Step | Hyp | Ref
| Expression |
1 | | kercvrlsm.f |
. . . . 5
⊢ (𝜑 → 𝐹 ∈ (𝑆 LMHom 𝑇)) |
2 | | lmhmlmod1 18854 |
. . . . 5
⊢ (𝐹 ∈ (𝑆 LMHom 𝑇) → 𝑆 ∈ LMod) |
3 | 1, 2 | syl 17 |
. . . 4
⊢ (𝜑 → 𝑆 ∈ LMod) |
4 | | kercvrlsm.k |
. . . . . 6
⊢ 𝐾 = (◡𝐹 “ { 0 }) |
5 | | kercvrlsm.z |
. . . . . 6
⊢ 0 =
(0g‘𝑇) |
6 | | kercvrlsm.u |
. . . . . 6
⊢ 𝑈 = (LSubSp‘𝑆) |
7 | 4, 5, 6 | lmhmkerlss 18872 |
. . . . 5
⊢ (𝐹 ∈ (𝑆 LMHom 𝑇) → 𝐾 ∈ 𝑈) |
8 | 1, 7 | syl 17 |
. . . 4
⊢ (𝜑 → 𝐾 ∈ 𝑈) |
9 | | kercvrlsm.d |
. . . 4
⊢ (𝜑 → 𝐷 ∈ 𝑈) |
10 | | kercvrlsm.p |
. . . . 5
⊢ ⊕ =
(LSSum‘𝑆) |
11 | 6, 10 | lsmcl 18904 |
. . . 4
⊢ ((𝑆 ∈ LMod ∧ 𝐾 ∈ 𝑈 ∧ 𝐷 ∈ 𝑈) → (𝐾 ⊕ 𝐷) ∈ 𝑈) |
12 | 3, 8, 9, 11 | syl3anc 1318 |
. . 3
⊢ (𝜑 → (𝐾 ⊕ 𝐷) ∈ 𝑈) |
13 | | kercvrlsm.b |
. . . 4
⊢ 𝐵 = (Base‘𝑆) |
14 | 13, 6 | lssss 18758 |
. . 3
⊢ ((𝐾 ⊕ 𝐷) ∈ 𝑈 → (𝐾 ⊕ 𝐷) ⊆ 𝐵) |
15 | 12, 14 | syl 17 |
. 2
⊢ (𝜑 → (𝐾 ⊕ 𝐷) ⊆ 𝐵) |
16 | | eqid 2610 |
. . . . . . . . . . 11
⊢
(Base‘𝑇) =
(Base‘𝑇) |
17 | 13, 16 | lmhmf 18855 |
. . . . . . . . . 10
⊢ (𝐹 ∈ (𝑆 LMHom 𝑇) → 𝐹:𝐵⟶(Base‘𝑇)) |
18 | 1, 17 | syl 17 |
. . . . . . . . 9
⊢ (𝜑 → 𝐹:𝐵⟶(Base‘𝑇)) |
19 | | ffn 5958 |
. . . . . . . . 9
⊢ (𝐹:𝐵⟶(Base‘𝑇) → 𝐹 Fn 𝐵) |
20 | 18, 19 | syl 17 |
. . . . . . . 8
⊢ (𝜑 → 𝐹 Fn 𝐵) |
21 | | fnfvelrn 6264 |
. . . . . . . 8
⊢ ((𝐹 Fn 𝐵 ∧ 𝑎 ∈ 𝐵) → (𝐹‘𝑎) ∈ ran 𝐹) |
22 | 20, 21 | sylan 487 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑎 ∈ 𝐵) → (𝐹‘𝑎) ∈ ran 𝐹) |
23 | | kercvrlsm.cv |
. . . . . . . 8
⊢ (𝜑 → (𝐹 “ 𝐷) = ran 𝐹) |
24 | 23 | adantr 480 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑎 ∈ 𝐵) → (𝐹 “ 𝐷) = ran 𝐹) |
25 | 22, 24 | eleqtrrd 2691 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑎 ∈ 𝐵) → (𝐹‘𝑎) ∈ (𝐹 “ 𝐷)) |
26 | 20 | adantr 480 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑎 ∈ 𝐵) → 𝐹 Fn 𝐵) |
27 | 13, 6 | lssss 18758 |
. . . . . . . . 9
⊢ (𝐷 ∈ 𝑈 → 𝐷 ⊆ 𝐵) |
28 | 9, 27 | syl 17 |
. . . . . . . 8
⊢ (𝜑 → 𝐷 ⊆ 𝐵) |
29 | 28 | adantr 480 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑎 ∈ 𝐵) → 𝐷 ⊆ 𝐵) |
30 | | fvelimab 6163 |
. . . . . . 7
⊢ ((𝐹 Fn 𝐵 ∧ 𝐷 ⊆ 𝐵) → ((𝐹‘𝑎) ∈ (𝐹 “ 𝐷) ↔ ∃𝑏 ∈ 𝐷 (𝐹‘𝑏) = (𝐹‘𝑎))) |
31 | 26, 29, 30 | syl2anc 691 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑎 ∈ 𝐵) → ((𝐹‘𝑎) ∈ (𝐹 “ 𝐷) ↔ ∃𝑏 ∈ 𝐷 (𝐹‘𝑏) = (𝐹‘𝑎))) |
32 | 25, 31 | mpbid 221 |
. . . . 5
⊢ ((𝜑 ∧ 𝑎 ∈ 𝐵) → ∃𝑏 ∈ 𝐷 (𝐹‘𝑏) = (𝐹‘𝑎)) |
33 | | lmodgrp 18693 |
. . . . . . . . . . . . 13
⊢ (𝑆 ∈ LMod → 𝑆 ∈ Grp) |
34 | 3, 33 | syl 17 |
. . . . . . . . . . . 12
⊢ (𝜑 → 𝑆 ∈ Grp) |
35 | 34 | adantr 480 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ (𝑎 ∈ 𝐵 ∧ 𝑏 ∈ 𝐷)) → 𝑆 ∈ Grp) |
36 | | simprl 790 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ (𝑎 ∈ 𝐵 ∧ 𝑏 ∈ 𝐷)) → 𝑎 ∈ 𝐵) |
37 | 28 | sselda 3568 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑏 ∈ 𝐷) → 𝑏 ∈ 𝐵) |
38 | 37 | adantrl 748 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ (𝑎 ∈ 𝐵 ∧ 𝑏 ∈ 𝐷)) → 𝑏 ∈ 𝐵) |
39 | | eqid 2610 |
. . . . . . . . . . . 12
⊢
(+g‘𝑆) = (+g‘𝑆) |
40 | | eqid 2610 |
. . . . . . . . . . . 12
⊢
(-g‘𝑆) = (-g‘𝑆) |
41 | 13, 39, 40 | grpnpcan 17330 |
. . . . . . . . . . 11
⊢ ((𝑆 ∈ Grp ∧ 𝑎 ∈ 𝐵 ∧ 𝑏 ∈ 𝐵) → ((𝑎(-g‘𝑆)𝑏)(+g‘𝑆)𝑏) = 𝑎) |
42 | 35, 36, 38, 41 | syl3anc 1318 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑎 ∈ 𝐵 ∧ 𝑏 ∈ 𝐷)) → ((𝑎(-g‘𝑆)𝑏)(+g‘𝑆)𝑏) = 𝑎) |
43 | 42 | adantr 480 |
. . . . . . . . 9
⊢ (((𝜑 ∧ (𝑎 ∈ 𝐵 ∧ 𝑏 ∈ 𝐷)) ∧ (𝐹‘𝑏) = (𝐹‘𝑎)) → ((𝑎(-g‘𝑆)𝑏)(+g‘𝑆)𝑏) = 𝑎) |
44 | 3 | ad2antrr 758 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ (𝑎 ∈ 𝐵 ∧ 𝑏 ∈ 𝐷)) ∧ (𝐹‘𝑏) = (𝐹‘𝑎)) → 𝑆 ∈ LMod) |
45 | 13, 6 | lssss 18758 |
. . . . . . . . . . . 12
⊢ (𝐾 ∈ 𝑈 → 𝐾 ⊆ 𝐵) |
46 | 8, 45 | syl 17 |
. . . . . . . . . . 11
⊢ (𝜑 → 𝐾 ⊆ 𝐵) |
47 | 46 | ad2antrr 758 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ (𝑎 ∈ 𝐵 ∧ 𝑏 ∈ 𝐷)) ∧ (𝐹‘𝑏) = (𝐹‘𝑎)) → 𝐾 ⊆ 𝐵) |
48 | 28 | ad2antrr 758 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ (𝑎 ∈ 𝐵 ∧ 𝑏 ∈ 𝐷)) ∧ (𝐹‘𝑏) = (𝐹‘𝑎)) → 𝐷 ⊆ 𝐵) |
49 | | eqcom 2617 |
. . . . . . . . . . . 12
⊢ ((𝐹‘𝑏) = (𝐹‘𝑎) ↔ (𝐹‘𝑎) = (𝐹‘𝑏)) |
50 | | lmghm 18852 |
. . . . . . . . . . . . . . 15
⊢ (𝐹 ∈ (𝑆 LMHom 𝑇) → 𝐹 ∈ (𝑆 GrpHom 𝑇)) |
51 | 1, 50 | syl 17 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → 𝐹 ∈ (𝑆 GrpHom 𝑇)) |
52 | 51 | adantr 480 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ (𝑎 ∈ 𝐵 ∧ 𝑏 ∈ 𝐷)) → 𝐹 ∈ (𝑆 GrpHom 𝑇)) |
53 | 13, 5, 4, 40 | ghmeqker 17510 |
. . . . . . . . . . . . 13
⊢ ((𝐹 ∈ (𝑆 GrpHom 𝑇) ∧ 𝑎 ∈ 𝐵 ∧ 𝑏 ∈ 𝐵) → ((𝐹‘𝑎) = (𝐹‘𝑏) ↔ (𝑎(-g‘𝑆)𝑏) ∈ 𝐾)) |
54 | 52, 36, 38, 53 | syl3anc 1318 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ (𝑎 ∈ 𝐵 ∧ 𝑏 ∈ 𝐷)) → ((𝐹‘𝑎) = (𝐹‘𝑏) ↔ (𝑎(-g‘𝑆)𝑏) ∈ 𝐾)) |
55 | 49, 54 | syl5bb 271 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ (𝑎 ∈ 𝐵 ∧ 𝑏 ∈ 𝐷)) → ((𝐹‘𝑏) = (𝐹‘𝑎) ↔ (𝑎(-g‘𝑆)𝑏) ∈ 𝐾)) |
56 | 55 | biimpa 500 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ (𝑎 ∈ 𝐵 ∧ 𝑏 ∈ 𝐷)) ∧ (𝐹‘𝑏) = (𝐹‘𝑎)) → (𝑎(-g‘𝑆)𝑏) ∈ 𝐾) |
57 | | simplrr 797 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ (𝑎 ∈ 𝐵 ∧ 𝑏 ∈ 𝐷)) ∧ (𝐹‘𝑏) = (𝐹‘𝑎)) → 𝑏 ∈ 𝐷) |
58 | 13, 39, 10 | lsmelvalix 17879 |
. . . . . . . . . 10
⊢ (((𝑆 ∈ LMod ∧ 𝐾 ⊆ 𝐵 ∧ 𝐷 ⊆ 𝐵) ∧ ((𝑎(-g‘𝑆)𝑏) ∈ 𝐾 ∧ 𝑏 ∈ 𝐷)) → ((𝑎(-g‘𝑆)𝑏)(+g‘𝑆)𝑏) ∈ (𝐾 ⊕ 𝐷)) |
59 | 44, 47, 48, 56, 57, 58 | syl32anc 1326 |
. . . . . . . . 9
⊢ (((𝜑 ∧ (𝑎 ∈ 𝐵 ∧ 𝑏 ∈ 𝐷)) ∧ (𝐹‘𝑏) = (𝐹‘𝑎)) → ((𝑎(-g‘𝑆)𝑏)(+g‘𝑆)𝑏) ∈ (𝐾 ⊕ 𝐷)) |
60 | 43, 59 | eqeltrrd 2689 |
. . . . . . . 8
⊢ (((𝜑 ∧ (𝑎 ∈ 𝐵 ∧ 𝑏 ∈ 𝐷)) ∧ (𝐹‘𝑏) = (𝐹‘𝑎)) → 𝑎 ∈ (𝐾 ⊕ 𝐷)) |
61 | 60 | ex 449 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑎 ∈ 𝐵 ∧ 𝑏 ∈ 𝐷)) → ((𝐹‘𝑏) = (𝐹‘𝑎) → 𝑎 ∈ (𝐾 ⊕ 𝐷))) |
62 | 61 | anassrs 678 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑎 ∈ 𝐵) ∧ 𝑏 ∈ 𝐷) → ((𝐹‘𝑏) = (𝐹‘𝑎) → 𝑎 ∈ (𝐾 ⊕ 𝐷))) |
63 | 62 | rexlimdva 3013 |
. . . . 5
⊢ ((𝜑 ∧ 𝑎 ∈ 𝐵) → (∃𝑏 ∈ 𝐷 (𝐹‘𝑏) = (𝐹‘𝑎) → 𝑎 ∈ (𝐾 ⊕ 𝐷))) |
64 | 32, 63 | mpd 15 |
. . . 4
⊢ ((𝜑 ∧ 𝑎 ∈ 𝐵) → 𝑎 ∈ (𝐾 ⊕ 𝐷)) |
65 | 64 | ex 449 |
. . 3
⊢ (𝜑 → (𝑎 ∈ 𝐵 → 𝑎 ∈ (𝐾 ⊕ 𝐷))) |
66 | 65 | ssrdv 3574 |
. 2
⊢ (𝜑 → 𝐵 ⊆ (𝐾 ⊕ 𝐷)) |
67 | 15, 66 | eqssd 3585 |
1
⊢ (𝜑 → (𝐾 ⊕ 𝐷) = 𝐵) |