Step | Hyp | Ref
| Expression |
1 | | pjf.k |
. . 3
⊢ 𝐾 = (proj‘𝑊) |
2 | | pjf.v |
. . 3
⊢ 𝑉 = (Base‘𝑊) |
3 | 1, 2 | pjf2 20058 |
. 2
⊢ ((𝑊 ∈ PreHil ∧ 𝑇 ∈ dom 𝐾) → (𝐾‘𝑇):𝑉⟶𝑇) |
4 | | frn 6053 |
. . . 4
⊢ ((𝐾‘𝑇):𝑉⟶𝑇 → ran (𝐾‘𝑇) ⊆ 𝑇) |
5 | 3, 4 | syl 17 |
. . 3
⊢ ((𝑊 ∈ PreHil ∧ 𝑇 ∈ dom 𝐾) → ran (𝐾‘𝑇) ⊆ 𝑇) |
6 | | eqid 2622 |
. . . . . . . . . 10
⊢
(ocv‘𝑊) =
(ocv‘𝑊) |
7 | | eqid 2622 |
. . . . . . . . . 10
⊢
(proj1‘𝑊) = (proj1‘𝑊) |
8 | 6, 7, 1 | pjval 20054 |
. . . . . . . . 9
⊢ (𝑇 ∈ dom 𝐾 → (𝐾‘𝑇) = (𝑇(proj1‘𝑊)((ocv‘𝑊)‘𝑇))) |
9 | 8 | ad2antlr 763 |
. . . . . . . 8
⊢ (((𝑊 ∈ PreHil ∧ 𝑇 ∈ dom 𝐾) ∧ 𝑥 ∈ 𝑇) → (𝐾‘𝑇) = (𝑇(proj1‘𝑊)((ocv‘𝑊)‘𝑇))) |
10 | 9 | fveq1d 6193 |
. . . . . . 7
⊢ (((𝑊 ∈ PreHil ∧ 𝑇 ∈ dom 𝐾) ∧ 𝑥 ∈ 𝑇) → ((𝐾‘𝑇)‘𝑥) = ((𝑇(proj1‘𝑊)((ocv‘𝑊)‘𝑇))‘𝑥)) |
11 | | eqid 2622 |
. . . . . . . 8
⊢
(+g‘𝑊) = (+g‘𝑊) |
12 | | eqid 2622 |
. . . . . . . 8
⊢
(LSSum‘𝑊) =
(LSSum‘𝑊) |
13 | | eqid 2622 |
. . . . . . . 8
⊢
(0g‘𝑊) = (0g‘𝑊) |
14 | | eqid 2622 |
. . . . . . . 8
⊢
(Cntz‘𝑊) =
(Cntz‘𝑊) |
15 | | phllmod 19975 |
. . . . . . . . . . 11
⊢ (𝑊 ∈ PreHil → 𝑊 ∈ LMod) |
16 | 15 | adantr 481 |
. . . . . . . . . 10
⊢ ((𝑊 ∈ PreHil ∧ 𝑇 ∈ dom 𝐾) → 𝑊 ∈ LMod) |
17 | | eqid 2622 |
. . . . . . . . . . 11
⊢
(LSubSp‘𝑊) =
(LSubSp‘𝑊) |
18 | 17 | lsssssubg 18958 |
. . . . . . . . . 10
⊢ (𝑊 ∈ LMod →
(LSubSp‘𝑊) ⊆
(SubGrp‘𝑊)) |
19 | 16, 18 | syl 17 |
. . . . . . . . 9
⊢ ((𝑊 ∈ PreHil ∧ 𝑇 ∈ dom 𝐾) → (LSubSp‘𝑊) ⊆ (SubGrp‘𝑊)) |
20 | 2, 17, 6, 12, 1 | pjdm2 20055 |
. . . . . . . . . 10
⊢ (𝑊 ∈ PreHil → (𝑇 ∈ dom 𝐾 ↔ (𝑇 ∈ (LSubSp‘𝑊) ∧ (𝑇(LSSum‘𝑊)((ocv‘𝑊)‘𝑇)) = 𝑉))) |
21 | 20 | simprbda 653 |
. . . . . . . . 9
⊢ ((𝑊 ∈ PreHil ∧ 𝑇 ∈ dom 𝐾) → 𝑇 ∈ (LSubSp‘𝑊)) |
22 | 19, 21 | sseldd 3604 |
. . . . . . . 8
⊢ ((𝑊 ∈ PreHil ∧ 𝑇 ∈ dom 𝐾) → 𝑇 ∈ (SubGrp‘𝑊)) |
23 | 2, 17 | lssss 18937 |
. . . . . . . . . . 11
⊢ (𝑇 ∈ (LSubSp‘𝑊) → 𝑇 ⊆ 𝑉) |
24 | 21, 23 | syl 17 |
. . . . . . . . . 10
⊢ ((𝑊 ∈ PreHil ∧ 𝑇 ∈ dom 𝐾) → 𝑇 ⊆ 𝑉) |
25 | 2, 6, 17 | ocvlss 20016 |
. . . . . . . . . 10
⊢ ((𝑊 ∈ PreHil ∧ 𝑇 ⊆ 𝑉) → ((ocv‘𝑊)‘𝑇) ∈ (LSubSp‘𝑊)) |
26 | 24, 25 | syldan 487 |
. . . . . . . . 9
⊢ ((𝑊 ∈ PreHil ∧ 𝑇 ∈ dom 𝐾) → ((ocv‘𝑊)‘𝑇) ∈ (LSubSp‘𝑊)) |
27 | 19, 26 | sseldd 3604 |
. . . . . . . 8
⊢ ((𝑊 ∈ PreHil ∧ 𝑇 ∈ dom 𝐾) → ((ocv‘𝑊)‘𝑇) ∈ (SubGrp‘𝑊)) |
28 | 6, 17, 13 | ocvin 20018 |
. . . . . . . . 9
⊢ ((𝑊 ∈ PreHil ∧ 𝑇 ∈ (LSubSp‘𝑊)) → (𝑇 ∩ ((ocv‘𝑊)‘𝑇)) = {(0g‘𝑊)}) |
29 | 21, 28 | syldan 487 |
. . . . . . . 8
⊢ ((𝑊 ∈ PreHil ∧ 𝑇 ∈ dom 𝐾) → (𝑇 ∩ ((ocv‘𝑊)‘𝑇)) = {(0g‘𝑊)}) |
30 | | lmodabl 18910 |
. . . . . . . . . 10
⊢ (𝑊 ∈ LMod → 𝑊 ∈ Abel) |
31 | 16, 30 | syl 17 |
. . . . . . . . 9
⊢ ((𝑊 ∈ PreHil ∧ 𝑇 ∈ dom 𝐾) → 𝑊 ∈ Abel) |
32 | 14, 31, 22, 27 | ablcntzd 18260 |
. . . . . . . 8
⊢ ((𝑊 ∈ PreHil ∧ 𝑇 ∈ dom 𝐾) → 𝑇 ⊆ ((Cntz‘𝑊)‘((ocv‘𝑊)‘𝑇))) |
33 | 11, 12, 13, 14, 22, 27, 29, 32, 7 | pj1lid 18114 |
. . . . . . 7
⊢ (((𝑊 ∈ PreHil ∧ 𝑇 ∈ dom 𝐾) ∧ 𝑥 ∈ 𝑇) → ((𝑇(proj1‘𝑊)((ocv‘𝑊)‘𝑇))‘𝑥) = 𝑥) |
34 | 10, 33 | eqtrd 2656 |
. . . . . 6
⊢ (((𝑊 ∈ PreHil ∧ 𝑇 ∈ dom 𝐾) ∧ 𝑥 ∈ 𝑇) → ((𝐾‘𝑇)‘𝑥) = 𝑥) |
35 | | ffn 6045 |
. . . . . . . . 9
⊢ ((𝐾‘𝑇):𝑉⟶𝑇 → (𝐾‘𝑇) Fn 𝑉) |
36 | 3, 35 | syl 17 |
. . . . . . . 8
⊢ ((𝑊 ∈ PreHil ∧ 𝑇 ∈ dom 𝐾) → (𝐾‘𝑇) Fn 𝑉) |
37 | 36 | adantr 481 |
. . . . . . 7
⊢ (((𝑊 ∈ PreHil ∧ 𝑇 ∈ dom 𝐾) ∧ 𝑥 ∈ 𝑇) → (𝐾‘𝑇) Fn 𝑉) |
38 | 24 | sselda 3603 |
. . . . . . 7
⊢ (((𝑊 ∈ PreHil ∧ 𝑇 ∈ dom 𝐾) ∧ 𝑥 ∈ 𝑇) → 𝑥 ∈ 𝑉) |
39 | | fnfvelrn 6356 |
. . . . . . 7
⊢ (((𝐾‘𝑇) Fn 𝑉 ∧ 𝑥 ∈ 𝑉) → ((𝐾‘𝑇)‘𝑥) ∈ ran (𝐾‘𝑇)) |
40 | 37, 38, 39 | syl2anc 693 |
. . . . . 6
⊢ (((𝑊 ∈ PreHil ∧ 𝑇 ∈ dom 𝐾) ∧ 𝑥 ∈ 𝑇) → ((𝐾‘𝑇)‘𝑥) ∈ ran (𝐾‘𝑇)) |
41 | 34, 40 | eqeltrrd 2702 |
. . . . 5
⊢ (((𝑊 ∈ PreHil ∧ 𝑇 ∈ dom 𝐾) ∧ 𝑥 ∈ 𝑇) → 𝑥 ∈ ran (𝐾‘𝑇)) |
42 | 41 | ex 450 |
. . . 4
⊢ ((𝑊 ∈ PreHil ∧ 𝑇 ∈ dom 𝐾) → (𝑥 ∈ 𝑇 → 𝑥 ∈ ran (𝐾‘𝑇))) |
43 | 42 | ssrdv 3609 |
. . 3
⊢ ((𝑊 ∈ PreHil ∧ 𝑇 ∈ dom 𝐾) → 𝑇 ⊆ ran (𝐾‘𝑇)) |
44 | 5, 43 | eqssd 3620 |
. 2
⊢ ((𝑊 ∈ PreHil ∧ 𝑇 ∈ dom 𝐾) → ran (𝐾‘𝑇) = 𝑇) |
45 | | dffo2 6119 |
. 2
⊢ ((𝐾‘𝑇):𝑉–onto→𝑇 ↔ ((𝐾‘𝑇):𝑉⟶𝑇 ∧ ran (𝐾‘𝑇) = 𝑇)) |
46 | 3, 44, 45 | sylanbrc 698 |
1
⊢ ((𝑊 ∈ PreHil ∧ 𝑇 ∈ dom 𝐾) → (𝐾‘𝑇):𝑉–onto→𝑇) |