Metamath Proof Explorer

Theorem kercvrlsm

Description: The domain of a linear function is the subspace sum of the kernel and any subspace which covers the range. (Contributed by Stefan O'Rear, 24-Jan-2015) (Revised by Stefan O'Rear, 6-May-2015)

Ref Expression
Hypotheses kercvrlsm.u ⊢ 𝑈 = ( LSubSp ‘ 𝑆 )
kercvrlsm.p ⊢ ⊕ = ( LSSum ‘ 𝑆 )
kercvrlsm.z ⊢ 0 = ( 0g ‘ 𝑇 )
kercvrlsm.k ⊢ 𝐾 = ( ◡ 𝐹 “ { 0 } )
kercvrlsm.b ⊢ 𝐵 = ( Base ‘ 𝑆 )
kercvrlsm.f ⊢ ( 𝜑 → 𝐹 ∈ ( 𝑆 LMHom 𝑇 ) )
kercvrlsm.d ⊢ ( 𝜑 → 𝐷 ∈ 𝑈 )
kercvrlsm.cv ⊢ ( 𝜑 → ( 𝐹 “ 𝐷 ) = ran 𝐹 )
Assertion kercvrlsm ( 𝜑 → ( 𝐾 ⊕ 𝐷 ) = 𝐵 )

Proof

Step Hyp Ref Expression
1 kercvrlsm.u ⊢ 𝑈 = ( LSubSp ‘ 𝑆 )
2 kercvrlsm.p ⊢ ⊕ = ( LSSum ‘ 𝑆 )
3 kercvrlsm.z ⊢ 0 = ( 0g ‘ 𝑇 )
4 kercvrlsm.k ⊢ 𝐾 = ( ◡ 𝐹 “ { 0 } )
5 kercvrlsm.b ⊢ 𝐵 = ( Base ‘ 𝑆 )
6 kercvrlsm.f ⊢ ( 𝜑 → 𝐹 ∈ ( 𝑆 LMHom 𝑇 ) )
7 kercvrlsm.d ⊢ ( 𝜑 → 𝐷 ∈ 𝑈 )
8 kercvrlsm.cv ⊢ ( 𝜑 → ( 𝐹 “ 𝐷 ) = ran 𝐹 )
9 lmhmlmod1 ⊢ ( 𝐹 ∈ ( 𝑆 LMHom 𝑇 ) → 𝑆 ∈ LMod )
10 6 9 syl ⊢ ( 𝜑 → 𝑆 ∈ LMod )
11 4 3 1 lmhmkerlss ⊢ ( 𝐹 ∈ ( 𝑆 LMHom 𝑇 ) → 𝐾 ∈ 𝑈 )
12 6 11 syl ⊢ ( 𝜑 → 𝐾 ∈ 𝑈 )
13 1 2 lsmcl ⊢ ( ( 𝑆 ∈ LMod ∧ 𝐾 ∈ 𝑈 ∧ 𝐷 ∈ 𝑈 ) → ( 𝐾 ⊕ 𝐷 ) ∈ 𝑈 )
14 10 12 7 13 syl3anc ⊢ ( 𝜑 → ( 𝐾 ⊕ 𝐷 ) ∈ 𝑈 )
15 5 1 lssss ⊢ ( ( 𝐾 ⊕ 𝐷 ) ∈ 𝑈 → ( 𝐾 ⊕ 𝐷 ) ⊆ 𝐵 )
16 14 15 syl ⊢ ( 𝜑 → ( 𝐾 ⊕ 𝐷 ) ⊆ 𝐵 )
17 eqid ⊢ ( Base ‘ 𝑇 ) = ( Base ‘ 𝑇 )
18 5 17 lmhmf ⊢ ( 𝐹 ∈ ( 𝑆 LMHom 𝑇 ) → 𝐹 : 𝐵 ⟶ ( Base ‘ 𝑇 ) )
19 6 18 syl ⊢ ( 𝜑 → 𝐹 : 𝐵 ⟶ ( Base ‘ 𝑇 ) )
20 19 ffnd ⊢ ( 𝜑 → 𝐹 Fn 𝐵 )
21 fnfvelrn ⊢ ( ( 𝐹 Fn 𝐵 ∧ 𝑎 ∈ 𝐵 ) → ( 𝐹 ‘ 𝑎 ) ∈ ran 𝐹 )
22 20 21 sylan ⊢ ( ( 𝜑 ∧ 𝑎 ∈ 𝐵 ) → ( 𝐹 ‘ 𝑎 ) ∈ ran 𝐹 )
23 8 adantr ⊢ ( ( 𝜑 ∧ 𝑎 ∈ 𝐵 ) → ( 𝐹 “ 𝐷 ) = ran 𝐹 )
24 22 23 eleqtrrd ⊢ ( ( 𝜑 ∧ 𝑎 ∈ 𝐵 ) → ( 𝐹 ‘ 𝑎 ) ∈ ( 𝐹 “ 𝐷 ) )
25 20 adantr ⊢ ( ( 𝜑 ∧ 𝑎 ∈ 𝐵 ) → 𝐹 Fn 𝐵 )
26 5 1 lssss ⊢ ( 𝐷 ∈ 𝑈 → 𝐷 ⊆ 𝐵 )
27 7 26 syl ⊢ ( 𝜑 → 𝐷 ⊆ 𝐵 )
28 27 adantr ⊢ ( ( 𝜑 ∧ 𝑎 ∈ 𝐵 ) → 𝐷 ⊆ 𝐵 )
29 fvelimab ⊢ ( ( 𝐹 Fn 𝐵 ∧ 𝐷 ⊆ 𝐵 ) → ( ( 𝐹 ‘ 𝑎 ) ∈ ( 𝐹 “ 𝐷 ) ↔ ∃ 𝑏 ∈ 𝐷 ( 𝐹 ‘ 𝑏 ) = ( 𝐹 ‘ 𝑎 ) ) )
30 25 28 29 syl2anc ⊢ ( ( 𝜑 ∧ 𝑎 ∈ 𝐵 ) → ( ( 𝐹 ‘ 𝑎 ) ∈ ( 𝐹 “ 𝐷 ) ↔ ∃ 𝑏 ∈ 𝐷 ( 𝐹 ‘ 𝑏 ) = ( 𝐹 ‘ 𝑎 ) ) )
31 24 30 mpbid ⊢ ( ( 𝜑 ∧ 𝑎 ∈ 𝐵 ) → ∃ 𝑏 ∈ 𝐷 ( 𝐹 ‘ 𝑏 ) = ( 𝐹 ‘ 𝑎 ) )
32 lmodgrp ⊢ ( 𝑆 ∈ LMod → 𝑆 ∈ Grp )
33 10 32 syl ⊢ ( 𝜑 → 𝑆 ∈ Grp )
34 33 adantr ⊢ ( ( 𝜑 ∧ ( 𝑎 ∈ 𝐵 ∧ 𝑏 ∈ 𝐷 ) ) → 𝑆 ∈ Grp )
35 simprl ⊢ ( ( 𝜑 ∧ ( 𝑎 ∈ 𝐵 ∧ 𝑏 ∈ 𝐷 ) ) → 𝑎 ∈ 𝐵 )
36 27 sselda ⊢ ( ( 𝜑 ∧ 𝑏 ∈ 𝐷 ) → 𝑏 ∈ 𝐵 )
37 36 adantrl ⊢ ( ( 𝜑 ∧ ( 𝑎 ∈ 𝐵 ∧ 𝑏 ∈ 𝐷 ) ) → 𝑏 ∈ 𝐵 )
38 eqid ⊢ ( +g ‘ 𝑆 ) = ( +g ‘ 𝑆 )
39 eqid ⊢ ( -g ‘ 𝑆 ) = ( -g ‘ 𝑆 )
40 5 38 39 grpnpcan ⊢ ( ( 𝑆 ∈ Grp ∧ 𝑎 ∈ 𝐵 ∧ 𝑏 ∈ 𝐵 ) → ( ( 𝑎 ( -g ‘ 𝑆 ) 𝑏 ) ( +g ‘ 𝑆 ) 𝑏 ) = 𝑎 )
41 34 35 37 40 syl3anc ⊢ ( ( 𝜑 ∧ ( 𝑎 ∈ 𝐵 ∧ 𝑏 ∈ 𝐷 ) ) → ( ( 𝑎 ( -g ‘ 𝑆 ) 𝑏 ) ( +g ‘ 𝑆 ) 𝑏 ) = 𝑎 )
42 41 adantr ⊢ ( ( ( 𝜑 ∧ ( 𝑎 ∈ 𝐵 ∧ 𝑏 ∈ 𝐷 ) ) ∧ ( 𝐹 ‘ 𝑏 ) = ( 𝐹 ‘ 𝑎 ) ) → ( ( 𝑎 ( -g ‘ 𝑆 ) 𝑏 ) ( +g ‘ 𝑆 ) 𝑏 ) = 𝑎 )
43 10 ad2antrr ⊢ ( ( ( 𝜑 ∧ ( 𝑎 ∈ 𝐵 ∧ 𝑏 ∈ 𝐷 ) ) ∧ ( 𝐹 ‘ 𝑏 ) = ( 𝐹 ‘ 𝑎 ) ) → 𝑆 ∈ LMod )
44 5 1 lssss ⊢ ( 𝐾 ∈ 𝑈 → 𝐾 ⊆ 𝐵 )
45 12 44 syl ⊢ ( 𝜑 → 𝐾 ⊆ 𝐵 )
46 45 ad2antrr ⊢ ( ( ( 𝜑 ∧ ( 𝑎 ∈ 𝐵 ∧ 𝑏 ∈ 𝐷 ) ) ∧ ( 𝐹 ‘ 𝑏 ) = ( 𝐹 ‘ 𝑎 ) ) → 𝐾 ⊆ 𝐵 )
47 27 ad2antrr ⊢ ( ( ( 𝜑 ∧ ( 𝑎 ∈ 𝐵 ∧ 𝑏 ∈ 𝐷 ) ) ∧ ( 𝐹 ‘ 𝑏 ) = ( 𝐹 ‘ 𝑎 ) ) → 𝐷 ⊆ 𝐵 )
48 eqcom ⊢ ( ( 𝐹 ‘ 𝑏 ) = ( 𝐹 ‘ 𝑎 ) ↔ ( 𝐹 ‘ 𝑎 ) = ( 𝐹 ‘ 𝑏 ) )
49 lmghm ⊢ ( 𝐹 ∈ ( 𝑆 LMHom 𝑇 ) → 𝐹 ∈ ( 𝑆 GrpHom 𝑇 ) )
50 6 49 syl ⊢ ( 𝜑 → 𝐹 ∈ ( 𝑆 GrpHom 𝑇 ) )
51 50 adantr ⊢ ( ( 𝜑 ∧ ( 𝑎 ∈ 𝐵 ∧ 𝑏 ∈ 𝐷 ) ) → 𝐹 ∈ ( 𝑆 GrpHom 𝑇 ) )
52 5 3 4 39 ghmeqker ⊢ ( ( 𝐹 ∈ ( 𝑆 GrpHom 𝑇 ) ∧ 𝑎 ∈ 𝐵 ∧ 𝑏 ∈ 𝐵 ) → ( ( 𝐹 ‘ 𝑎 ) = ( 𝐹 ‘ 𝑏 ) ↔ ( 𝑎 ( -g ‘ 𝑆 ) 𝑏 ) ∈ 𝐾 ) )
53 51 35 37 52 syl3anc ⊢ ( ( 𝜑 ∧ ( 𝑎 ∈ 𝐵 ∧ 𝑏 ∈ 𝐷 ) ) → ( ( 𝐹 ‘ 𝑎 ) = ( 𝐹 ‘ 𝑏 ) ↔ ( 𝑎 ( -g ‘ 𝑆 ) 𝑏 ) ∈ 𝐾 ) )
54 48 53 syl5bb ⊢ ( ( 𝜑 ∧ ( 𝑎 ∈ 𝐵 ∧ 𝑏 ∈ 𝐷 ) ) → ( ( 𝐹 ‘ 𝑏 ) = ( 𝐹 ‘ 𝑎 ) ↔ ( 𝑎 ( -g ‘ 𝑆 ) 𝑏 ) ∈ 𝐾 ) )
55 54 biimpa ⊢ ( ( ( 𝜑 ∧ ( 𝑎 ∈ 𝐵 ∧ 𝑏 ∈ 𝐷 ) ) ∧ ( 𝐹 ‘ 𝑏 ) = ( 𝐹 ‘ 𝑎 ) ) → ( 𝑎 ( -g ‘ 𝑆 ) 𝑏 ) ∈ 𝐾 )
56 simplrr ⊢ ( ( ( 𝜑 ∧ ( 𝑎 ∈ 𝐵 ∧ 𝑏 ∈ 𝐷 ) ) ∧ ( 𝐹 ‘ 𝑏 ) = ( 𝐹 ‘ 𝑎 ) ) → 𝑏 ∈ 𝐷 )
57 5 38 2 lsmelvalix ⊢ ( ( ( 𝑆 ∈ LMod ∧ 𝐾 ⊆ 𝐵 ∧ 𝐷 ⊆ 𝐵 ) ∧ ( ( 𝑎 ( -g ‘ 𝑆 ) 𝑏 ) ∈ 𝐾 ∧ 𝑏 ∈ 𝐷 ) ) → ( ( 𝑎 ( -g ‘ 𝑆 ) 𝑏 ) ( +g ‘ 𝑆 ) 𝑏 ) ∈ ( 𝐾 ⊕ 𝐷 ) )
58 43 46 47 55 56 57 syl32anc ⊢ ( ( ( 𝜑 ∧ ( 𝑎 ∈ 𝐵 ∧ 𝑏 ∈ 𝐷 ) ) ∧ ( 𝐹 ‘ 𝑏 ) = ( 𝐹 ‘ 𝑎 ) ) → ( ( 𝑎 ( -g ‘ 𝑆 ) 𝑏 ) ( +g ‘ 𝑆 ) 𝑏 ) ∈ ( 𝐾 ⊕ 𝐷 ) )
59 42 58 eqeltrrd ⊢ ( ( ( 𝜑 ∧ ( 𝑎 ∈ 𝐵 ∧ 𝑏 ∈ 𝐷 ) ) ∧ ( 𝐹 ‘ 𝑏 ) = ( 𝐹 ‘ 𝑎 ) ) → 𝑎 ∈ ( 𝐾 ⊕ 𝐷 ) )
60 59 ex ⊢ ( ( 𝜑 ∧ ( 𝑎 ∈ 𝐵 ∧ 𝑏 ∈ 𝐷 ) ) → ( ( 𝐹 ‘ 𝑏 ) = ( 𝐹 ‘ 𝑎 ) → 𝑎 ∈ ( 𝐾 ⊕ 𝐷 ) ) )
61 60 anassrs ⊢ ( ( ( 𝜑 ∧ 𝑎 ∈ 𝐵 ) ∧ 𝑏 ∈ 𝐷 ) → ( ( 𝐹 ‘ 𝑏 ) = ( 𝐹 ‘ 𝑎 ) → 𝑎 ∈ ( 𝐾 ⊕ 𝐷 ) ) )
62 61 rexlimdva ⊢ ( ( 𝜑 ∧ 𝑎 ∈ 𝐵 ) → ( ∃ 𝑏 ∈ 𝐷 ( 𝐹 ‘ 𝑏 ) = ( 𝐹 ‘ 𝑎 ) → 𝑎 ∈ ( 𝐾 ⊕ 𝐷 ) ) )
63 31 62 mpd ⊢ ( ( 𝜑 ∧ 𝑎 ∈ 𝐵 ) → 𝑎 ∈ ( 𝐾 ⊕ 𝐷 ) )
64 16 63 eqelssd ⊢ ( 𝜑 → ( 𝐾 ⊕ 𝐷 ) = 𝐵 )