Metamath Proof Explorer

Theorem lsmsat

Description: Convert comparison of atom with sum of subspaces to a comparison to sum with atom. ( elpaddatiN analog.) TODO: any way to shorten this? (Contributed by NM, 15-Jan-2015)

Ref Expression
Hypotheses lsmsat.o ⊢ 0 = ( 0g ‘ 𝑊 )
lsmsat.s ⊢ 𝑆 = ( LSubSp ‘ 𝑊 )
lsmsat.p ⊢ ⊕ = ( LSSum ‘ 𝑊 )
lsmsat.a ⊢ 𝐴 = ( LSAtoms ‘ 𝑊 )
lsmsat.w ⊢ ( 𝜑 → 𝑊 ∈ LMod )
lsmsat.t ⊢ ( 𝜑 → 𝑇 ∈ 𝑆 )
lsmsat.u ⊢ ( 𝜑 → 𝑈 ∈ 𝑆 )
lsmsat.q ⊢ ( 𝜑 → 𝑄 ∈ 𝐴 )
lsmsat.n ⊢ ( 𝜑 → 𝑇 ≠ { 0 } )
lsmsat.l ⊢ ( 𝜑 → 𝑄 ⊆ ( 𝑇 ⊕ 𝑈 ) )
Assertion lsmsat ( 𝜑 → ∃ 𝑝 ∈ 𝐴 ( 𝑝 ⊆ 𝑇 ∧ 𝑄 ⊆ ( 𝑝 ⊕ 𝑈 ) ) )

Proof

Step Hyp Ref Expression
1 lsmsat.o ⊢ 0 = ( 0g ‘ 𝑊 )
2 lsmsat.s ⊢ 𝑆 = ( LSubSp ‘ 𝑊 )
3 lsmsat.p ⊢ ⊕ = ( LSSum ‘ 𝑊 )
4 lsmsat.a ⊢ 𝐴 = ( LSAtoms ‘ 𝑊 )
5 lsmsat.w ⊢ ( 𝜑 → 𝑊 ∈ LMod )
6 lsmsat.t ⊢ ( 𝜑 → 𝑇 ∈ 𝑆 )
7 lsmsat.u ⊢ ( 𝜑 → 𝑈 ∈ 𝑆 )
8 lsmsat.q ⊢ ( 𝜑 → 𝑄 ∈ 𝐴 )
9 lsmsat.n ⊢ ( 𝜑 → 𝑇 ≠ { 0 } )
10 lsmsat.l ⊢ ( 𝜑 → 𝑄 ⊆ ( 𝑇 ⊕ 𝑈 ) )
11 eqid ⊢ ( Base ‘ 𝑊 ) = ( Base ‘ 𝑊 )
12 eqid ⊢ ( LSpan ‘ 𝑊 ) = ( LSpan ‘ 𝑊 )
13 11 12 1 4 islsat ⊢ ( 𝑊 ∈ LMod → ( 𝑄 ∈ 𝐴 ↔ ∃ 𝑟 ∈ ( ( Base ‘ 𝑊 ) ∖ { 0 } ) 𝑄 = ( ( LSpan ‘ 𝑊 ) ‘ { 𝑟 } ) ) )
14 5 13 syl ⊢ ( 𝜑 → ( 𝑄 ∈ 𝐴 ↔ ∃ 𝑟 ∈ ( ( Base ‘ 𝑊 ) ∖ { 0 } ) 𝑄 = ( ( LSpan ‘ 𝑊 ) ‘ { 𝑟 } ) ) )
15 8 14 mpbid ⊢ ( 𝜑 → ∃ 𝑟 ∈ ( ( Base ‘ 𝑊 ) ∖ { 0 } ) 𝑄 = ( ( LSpan ‘ 𝑊 ) ‘ { 𝑟 } ) )
16 simp3 ⊢ ( ( 𝜑 ∧ 𝑟 ∈ ( ( Base ‘ 𝑊 ) ∖ { 0 } ) ∧ 𝑄 = ( ( LSpan ‘ 𝑊 ) ‘ { 𝑟 } ) ) → 𝑄 = ( ( LSpan ‘ 𝑊 ) ‘ { 𝑟 } ) )
17 10 3ad2ant1 ⊢ ( ( 𝜑 ∧ 𝑟 ∈ ( ( Base ‘ 𝑊 ) ∖ { 0 } ) ∧ 𝑄 = ( ( LSpan ‘ 𝑊 ) ‘ { 𝑟 } ) ) → 𝑄 ⊆ ( 𝑇 ⊕ 𝑈 ) )
18 16 17 eqsstrrd ⊢ ( ( 𝜑 ∧ 𝑟 ∈ ( ( Base ‘ 𝑊 ) ∖ { 0 } ) ∧ 𝑄 = ( ( LSpan ‘ 𝑊 ) ‘ { 𝑟 } ) ) → ( ( LSpan ‘ 𝑊 ) ‘ { 𝑟 } ) ⊆ ( 𝑇 ⊕ 𝑈 ) )
19 5 3ad2ant1 ⊢ ( ( 𝜑 ∧ 𝑟 ∈ ( ( Base ‘ 𝑊 ) ∖ { 0 } ) ∧ 𝑄 = ( ( LSpan ‘ 𝑊 ) ‘ { 𝑟 } ) ) → 𝑊 ∈ LMod )
20 2 3 lsmcl ⊢ ( ( 𝑊 ∈ LMod ∧ 𝑇 ∈ 𝑆 ∧ 𝑈 ∈ 𝑆 ) → ( 𝑇 ⊕ 𝑈 ) ∈ 𝑆 )
21 5 6 7 20 syl3anc ⊢ ( 𝜑 → ( 𝑇 ⊕ 𝑈 ) ∈ 𝑆 )
22 21 3ad2ant1 ⊢ ( ( 𝜑 ∧ 𝑟 ∈ ( ( Base ‘ 𝑊 ) ∖ { 0 } ) ∧ 𝑄 = ( ( LSpan ‘ 𝑊 ) ‘ { 𝑟 } ) ) → ( 𝑇 ⊕ 𝑈 ) ∈ 𝑆 )
23 eldifi ⊢ ( 𝑟 ∈ ( ( Base ‘ 𝑊 ) ∖ { 0 } ) → 𝑟 ∈ ( Base ‘ 𝑊 ) )
24 23 3ad2ant2 ⊢ ( ( 𝜑 ∧ 𝑟 ∈ ( ( Base ‘ 𝑊 ) ∖ { 0 } ) ∧ 𝑄 = ( ( LSpan ‘ 𝑊 ) ‘ { 𝑟 } ) ) → 𝑟 ∈ ( Base ‘ 𝑊 ) )
25 11 2 12 19 22 24 ellspsn5b ⊢ ( ( 𝜑 ∧ 𝑟 ∈ ( ( Base ‘ 𝑊 ) ∖ { 0 } ) ∧ 𝑄 = ( ( LSpan ‘ 𝑊 ) ‘ { 𝑟 } ) ) → ( 𝑟 ∈ ( 𝑇 ⊕ 𝑈 ) ↔ ( ( LSpan ‘ 𝑊 ) ‘ { 𝑟 } ) ⊆ ( 𝑇 ⊕ 𝑈 ) ) )
26 18 25 mpbird ⊢ ( ( 𝜑 ∧ 𝑟 ∈ ( ( Base ‘ 𝑊 ) ∖ { 0 } ) ∧ 𝑄 = ( ( LSpan ‘ 𝑊 ) ‘ { 𝑟 } ) ) → 𝑟 ∈ ( 𝑇 ⊕ 𝑈 ) )
27 2 lsssssubg ⊢ ( 𝑊 ∈ LMod → 𝑆 ⊆ ( SubGrp ‘ 𝑊 ) )
28 19 27 syl ⊢ ( ( 𝜑 ∧ 𝑟 ∈ ( ( Base ‘ 𝑊 ) ∖ { 0 } ) ∧ 𝑄 = ( ( LSpan ‘ 𝑊 ) ‘ { 𝑟 } ) ) → 𝑆 ⊆ ( SubGrp ‘ 𝑊 ) )
29 6 3ad2ant1 ⊢ ( ( 𝜑 ∧ 𝑟 ∈ ( ( Base ‘ 𝑊 ) ∖ { 0 } ) ∧ 𝑄 = ( ( LSpan ‘ 𝑊 ) ‘ { 𝑟 } ) ) → 𝑇 ∈ 𝑆 )
30 28 29 sseldd ⊢ ( ( 𝜑 ∧ 𝑟 ∈ ( ( Base ‘ 𝑊 ) ∖ { 0 } ) ∧ 𝑄 = ( ( LSpan ‘ 𝑊 ) ‘ { 𝑟 } ) ) → 𝑇 ∈ ( SubGrp ‘ 𝑊 ) )
31 7 3ad2ant1 ⊢ ( ( 𝜑 ∧ 𝑟 ∈ ( ( Base ‘ 𝑊 ) ∖ { 0 } ) ∧ 𝑄 = ( ( LSpan ‘ 𝑊 ) ‘ { 𝑟 } ) ) → 𝑈 ∈ 𝑆 )
32 28 31 sseldd ⊢ ( ( 𝜑 ∧ 𝑟 ∈ ( ( Base ‘ 𝑊 ) ∖ { 0 } ) ∧ 𝑄 = ( ( LSpan ‘ 𝑊 ) ‘ { 𝑟 } ) ) → 𝑈 ∈ ( SubGrp ‘ 𝑊 ) )
33 eqid ⊢ ( +g ‘ 𝑊 ) = ( +g ‘ 𝑊 )
34 33 3 lsmelval ⊢ ( ( 𝑇 ∈ ( SubGrp ‘ 𝑊 ) ∧ 𝑈 ∈ ( SubGrp ‘ 𝑊 ) ) → ( 𝑟 ∈ ( 𝑇 ⊕ 𝑈 ) ↔ ∃ 𝑦 ∈ 𝑇 ∃ 𝑧 ∈ 𝑈 𝑟 = ( 𝑦 ( +g ‘ 𝑊 ) 𝑧 ) ) )
35 30 32 34 syl2anc ⊢ ( ( 𝜑 ∧ 𝑟 ∈ ( ( Base ‘ 𝑊 ) ∖ { 0 } ) ∧ 𝑄 = ( ( LSpan ‘ 𝑊 ) ‘ { 𝑟 } ) ) → ( 𝑟 ∈ ( 𝑇 ⊕ 𝑈 ) ↔ ∃ 𝑦 ∈ 𝑇 ∃ 𝑧 ∈ 𝑈 𝑟 = ( 𝑦 ( +g ‘ 𝑊 ) 𝑧 ) ) )
36 26 35 mpbid ⊢ ( ( 𝜑 ∧ 𝑟 ∈ ( ( Base ‘ 𝑊 ) ∖ { 0 } ) ∧ 𝑄 = ( ( LSpan ‘ 𝑊 ) ‘ { 𝑟 } ) ) → ∃ 𝑦 ∈ 𝑇 ∃ 𝑧 ∈ 𝑈 𝑟 = ( 𝑦 ( +g ‘ 𝑊 ) 𝑧 ) )
37 1 2 lssne0 ⊢ ( 𝑇 ∈ 𝑆 → ( 𝑇 ≠ { 0 } ↔ ∃ 𝑞 ∈ 𝑇 𝑞 ≠ 0 ) )
38 6 37 syl ⊢ ( 𝜑 → ( 𝑇 ≠ { 0 } ↔ ∃ 𝑞 ∈ 𝑇 𝑞 ≠ 0 ) )
39 9 38 mpbid ⊢ ( 𝜑 → ∃ 𝑞 ∈ 𝑇 𝑞 ≠ 0 )
40 39 adantr ⊢ ( ( 𝜑 ∧ 𝑟 ∈ ( ( Base ‘ 𝑊 ) ∖ { 0 } ) ) → ∃ 𝑞 ∈ 𝑇 𝑞 ≠ 0 )
41 40 3ad2ant1 ⊢ ( ( ( 𝜑 ∧ 𝑟 ∈ ( ( Base ‘ 𝑊 ) ∖ { 0 } ) ) ∧ ( 𝑦 ∈ 𝑇 ∧ 𝑧 ∈ 𝑈 ) ∧ 𝑟 = ( 𝑦 ( +g ‘ 𝑊 ) 𝑧 ) ) → ∃ 𝑞 ∈ 𝑇 𝑞 ≠ 0 )
42 41 adantr ⊢ ( ( ( ( 𝜑 ∧ 𝑟 ∈ ( ( Base ‘ 𝑊 ) ∖ { 0 } ) ) ∧ ( 𝑦 ∈ 𝑇 ∧ 𝑧 ∈ 𝑈 ) ∧ 𝑟 = ( 𝑦 ( +g ‘ 𝑊 ) 𝑧 ) ) ∧ 𝑦 = 0 ) → ∃ 𝑞 ∈ 𝑇 𝑞 ≠ 0 )
43 5 adantr ⊢ ( ( 𝜑 ∧ 𝑟 ∈ ( ( Base ‘ 𝑊 ) ∖ { 0 } ) ) → 𝑊 ∈ LMod )
44 43 3ad2ant1 ⊢ ( ( ( 𝜑 ∧ 𝑟 ∈ ( ( Base ‘ 𝑊 ) ∖ { 0 } ) ) ∧ ( 𝑦 ∈ 𝑇 ∧ 𝑧 ∈ 𝑈 ) ∧ 𝑟 = ( 𝑦 ( +g ‘ 𝑊 ) 𝑧 ) ) → 𝑊 ∈ LMod )
45 44 adantr ⊢ ( ( ( ( 𝜑 ∧ 𝑟 ∈ ( ( Base ‘ 𝑊 ) ∖ { 0 } ) ) ∧ ( 𝑦 ∈ 𝑇 ∧ 𝑧 ∈ 𝑈 ) ∧ 𝑟 = ( 𝑦 ( +g ‘ 𝑊 ) 𝑧 ) ) ∧ ( 𝑦 = 0 ∧ 𝑞 ∈ 𝑇 ∧ 𝑞 ≠ 0 ) ) → 𝑊 ∈ LMod )
46 6 adantr ⊢ ( ( 𝜑 ∧ 𝑟 ∈ ( ( Base ‘ 𝑊 ) ∖ { 0 } ) ) → 𝑇 ∈ 𝑆 )
47 46 3ad2ant1 ⊢ ( ( ( 𝜑 ∧ 𝑟 ∈ ( ( Base ‘ 𝑊 ) ∖ { 0 } ) ) ∧ ( 𝑦 ∈ 𝑇 ∧ 𝑧 ∈ 𝑈 ) ∧ 𝑟 = ( 𝑦 ( +g ‘ 𝑊 ) 𝑧 ) ) → 𝑇 ∈ 𝑆 )
48 47 adantr ⊢ ( ( ( ( 𝜑 ∧ 𝑟 ∈ ( ( Base ‘ 𝑊 ) ∖ { 0 } ) ) ∧ ( 𝑦 ∈ 𝑇 ∧ 𝑧 ∈ 𝑈 ) ∧ 𝑟 = ( 𝑦 ( +g ‘ 𝑊 ) 𝑧 ) ) ∧ ( 𝑦 = 0 ∧ 𝑞 ∈ 𝑇 ∧ 𝑞 ≠ 0 ) ) → 𝑇 ∈ 𝑆 )
49 simpr2 ⊢ ( ( ( ( 𝜑 ∧ 𝑟 ∈ ( ( Base ‘ 𝑊 ) ∖ { 0 } ) ) ∧ ( 𝑦 ∈ 𝑇 ∧ 𝑧 ∈ 𝑈 ) ∧ 𝑟 = ( 𝑦 ( +g ‘ 𝑊 ) 𝑧 ) ) ∧ ( 𝑦 = 0 ∧ 𝑞 ∈ 𝑇 ∧ 𝑞 ≠ 0 ) ) → 𝑞 ∈ 𝑇 )
50 11 2 lssel ⊢ ( ( 𝑇 ∈ 𝑆 ∧ 𝑞 ∈ 𝑇 ) → 𝑞 ∈ ( Base ‘ 𝑊 ) )
51 48 49 50 syl2anc ⊢ ( ( ( ( 𝜑 ∧ 𝑟 ∈ ( ( Base ‘ 𝑊 ) ∖ { 0 } ) ) ∧ ( 𝑦 ∈ 𝑇 ∧ 𝑧 ∈ 𝑈 ) ∧ 𝑟 = ( 𝑦 ( +g ‘ 𝑊 ) 𝑧 ) ) ∧ ( 𝑦 = 0 ∧ 𝑞 ∈ 𝑇 ∧ 𝑞 ≠ 0 ) ) → 𝑞 ∈ ( Base ‘ 𝑊 ) )
52 simpr3 ⊢ ( ( ( ( 𝜑 ∧ 𝑟 ∈ ( ( Base ‘ 𝑊 ) ∖ { 0 } ) ) ∧ ( 𝑦 ∈ 𝑇 ∧ 𝑧 ∈ 𝑈 ) ∧ 𝑟 = ( 𝑦 ( +g ‘ 𝑊 ) 𝑧 ) ) ∧ ( 𝑦 = 0 ∧ 𝑞 ∈ 𝑇 ∧ 𝑞 ≠ 0 ) ) → 𝑞 ≠ 0 )
53 11 12 1 4 lsatlspsn2 ⊢ ( ( 𝑊 ∈ LMod ∧ 𝑞 ∈ ( Base ‘ 𝑊 ) ∧ 𝑞 ≠ 0 ) → ( ( LSpan ‘ 𝑊 ) ‘ { 𝑞 } ) ∈ 𝐴 )
54 45 51 52 53 syl3anc ⊢ ( ( ( ( 𝜑 ∧ 𝑟 ∈ ( ( Base ‘ 𝑊 ) ∖ { 0 } ) ) ∧ ( 𝑦 ∈ 𝑇 ∧ 𝑧 ∈ 𝑈 ) ∧ 𝑟 = ( 𝑦 ( +g ‘ 𝑊 ) 𝑧 ) ) ∧ ( 𝑦 = 0 ∧ 𝑞 ∈ 𝑇 ∧ 𝑞 ≠ 0 ) ) → ( ( LSpan ‘ 𝑊 ) ‘ { 𝑞 } ) ∈ 𝐴 )
55 2 12 45 48 49 ellspsn5 ⊢ ( ( ( ( 𝜑 ∧ 𝑟 ∈ ( ( Base ‘ 𝑊 ) ∖ { 0 } ) ) ∧ ( 𝑦 ∈ 𝑇 ∧ 𝑧 ∈ 𝑈 ) ∧ 𝑟 = ( 𝑦 ( +g ‘ 𝑊 ) 𝑧 ) ) ∧ ( 𝑦 = 0 ∧ 𝑞 ∈ 𝑇 ∧ 𝑞 ≠ 0 ) ) → ( ( LSpan ‘ 𝑊 ) ‘ { 𝑞 } ) ⊆ 𝑇 )
56 simpl3 ⊢ ( ( ( ( 𝜑 ∧ 𝑟 ∈ ( ( Base ‘ 𝑊 ) ∖ { 0 } ) ) ∧ ( 𝑦 ∈ 𝑇 ∧ 𝑧 ∈ 𝑈 ) ∧ 𝑟 = ( 𝑦 ( +g ‘ 𝑊 ) 𝑧 ) ) ∧ ( 𝑦 = 0 ∧ 𝑞 ∈ 𝑇 ∧ 𝑞 ≠ 0 ) ) → 𝑟 = ( 𝑦 ( +g ‘ 𝑊 ) 𝑧 ) )
57 simpr1 ⊢ ( ( ( ( 𝜑 ∧ 𝑟 ∈ ( ( Base ‘ 𝑊 ) ∖ { 0 } ) ) ∧ ( 𝑦 ∈ 𝑇 ∧ 𝑧 ∈ 𝑈 ) ∧ 𝑟 = ( 𝑦 ( +g ‘ 𝑊 ) 𝑧 ) ) ∧ ( 𝑦 = 0 ∧ 𝑞 ∈ 𝑇 ∧ 𝑞 ≠ 0 ) ) → 𝑦 = 0 )
58 57 oveq1d ⊢ ( ( ( ( 𝜑 ∧ 𝑟 ∈ ( ( Base ‘ 𝑊 ) ∖ { 0 } ) ) ∧ ( 𝑦 ∈ 𝑇 ∧ 𝑧 ∈ 𝑈 ) ∧ 𝑟 = ( 𝑦 ( +g ‘ 𝑊 ) 𝑧 ) ) ∧ ( 𝑦 = 0 ∧ 𝑞 ∈ 𝑇 ∧ 𝑞 ≠ 0 ) ) → ( 𝑦 ( +g ‘ 𝑊 ) 𝑧 ) = ( 0 ( +g ‘ 𝑊 ) 𝑧 ) )
59 7 adantr ⊢ ( ( 𝜑 ∧ 𝑟 ∈ ( ( Base ‘ 𝑊 ) ∖ { 0 } ) ) → 𝑈 ∈ 𝑆 )
60 59 3ad2ant1 ⊢ ( ( ( 𝜑 ∧ 𝑟 ∈ ( ( Base ‘ 𝑊 ) ∖ { 0 } ) ) ∧ ( 𝑦 ∈ 𝑇 ∧ 𝑧 ∈ 𝑈 ) ∧ 𝑟 = ( 𝑦 ( +g ‘ 𝑊 ) 𝑧 ) ) → 𝑈 ∈ 𝑆 )
61 simp2r ⊢ ( ( ( 𝜑 ∧ 𝑟 ∈ ( ( Base ‘ 𝑊 ) ∖ { 0 } ) ) ∧ ( 𝑦 ∈ 𝑇 ∧ 𝑧 ∈ 𝑈 ) ∧ 𝑟 = ( 𝑦 ( +g ‘ 𝑊 ) 𝑧 ) ) → 𝑧 ∈ 𝑈 )
62 11 2 lssel ⊢ ( ( 𝑈 ∈ 𝑆 ∧ 𝑧 ∈ 𝑈 ) → 𝑧 ∈ ( Base ‘ 𝑊 ) )
63 60 61 62 syl2anc ⊢ ( ( ( 𝜑 ∧ 𝑟 ∈ ( ( Base ‘ 𝑊 ) ∖ { 0 } ) ) ∧ ( 𝑦 ∈ 𝑇 ∧ 𝑧 ∈ 𝑈 ) ∧ 𝑟 = ( 𝑦 ( +g ‘ 𝑊 ) 𝑧 ) ) → 𝑧 ∈ ( Base ‘ 𝑊 ) )
64 63 adantr ⊢ ( ( ( ( 𝜑 ∧ 𝑟 ∈ ( ( Base ‘ 𝑊 ) ∖ { 0 } ) ) ∧ ( 𝑦 ∈ 𝑇 ∧ 𝑧 ∈ 𝑈 ) ∧ 𝑟 = ( 𝑦 ( +g ‘ 𝑊 ) 𝑧 ) ) ∧ ( 𝑦 = 0 ∧ 𝑞 ∈ 𝑇 ∧ 𝑞 ≠ 0 ) ) → 𝑧 ∈ ( Base ‘ 𝑊 ) )
65 11 33 1 lmod0vlid ⊢ ( ( 𝑊 ∈ LMod ∧ 𝑧 ∈ ( Base ‘ 𝑊 ) ) → ( 0 ( +g ‘ 𝑊 ) 𝑧 ) = 𝑧 )
66 45 64 65 syl2anc ⊢ ( ( ( ( 𝜑 ∧ 𝑟 ∈ ( ( Base ‘ 𝑊 ) ∖ { 0 } ) ) ∧ ( 𝑦 ∈ 𝑇 ∧ 𝑧 ∈ 𝑈 ) ∧ 𝑟 = ( 𝑦 ( +g ‘ 𝑊 ) 𝑧 ) ) ∧ ( 𝑦 = 0 ∧ 𝑞 ∈ 𝑇 ∧ 𝑞 ≠ 0 ) ) → ( 0 ( +g ‘ 𝑊 ) 𝑧 ) = 𝑧 )
67 56 58 66 3eqtrd ⊢ ( ( ( ( 𝜑 ∧ 𝑟 ∈ ( ( Base ‘ 𝑊 ) ∖ { 0 } ) ) ∧ ( 𝑦 ∈ 𝑇 ∧ 𝑧 ∈ 𝑈 ) ∧ 𝑟 = ( 𝑦 ( +g ‘ 𝑊 ) 𝑧 ) ) ∧ ( 𝑦 = 0 ∧ 𝑞 ∈ 𝑇 ∧ 𝑞 ≠ 0 ) ) → 𝑟 = 𝑧 )
68 67 sneqd ⊢ ( ( ( ( 𝜑 ∧ 𝑟 ∈ ( ( Base ‘ 𝑊 ) ∖ { 0 } ) ) ∧ ( 𝑦 ∈ 𝑇 ∧ 𝑧 ∈ 𝑈 ) ∧ 𝑟 = ( 𝑦 ( +g ‘ 𝑊 ) 𝑧 ) ) ∧ ( 𝑦 = 0 ∧ 𝑞 ∈ 𝑇 ∧ 𝑞 ≠ 0 ) ) → { 𝑟 } = { 𝑧 } )
69 68 fveq2d ⊢ ( ( ( ( 𝜑 ∧ 𝑟 ∈ ( ( Base ‘ 𝑊 ) ∖ { 0 } ) ) ∧ ( 𝑦 ∈ 𝑇 ∧ 𝑧 ∈ 𝑈 ) ∧ 𝑟 = ( 𝑦 ( +g ‘ 𝑊 ) 𝑧 ) ) ∧ ( 𝑦 = 0 ∧ 𝑞 ∈ 𝑇 ∧ 𝑞 ≠ 0 ) ) → ( ( LSpan ‘ 𝑊 ) ‘ { 𝑟 } ) = ( ( LSpan ‘ 𝑊 ) ‘ { 𝑧 } ) )
70 2 12 44 60 61 ellspsn5 ⊢ ( ( ( 𝜑 ∧ 𝑟 ∈ ( ( Base ‘ 𝑊 ) ∖ { 0 } ) ) ∧ ( 𝑦 ∈ 𝑇 ∧ 𝑧 ∈ 𝑈 ) ∧ 𝑟 = ( 𝑦 ( +g ‘ 𝑊 ) 𝑧 ) ) → ( ( LSpan ‘ 𝑊 ) ‘ { 𝑧 } ) ⊆ 𝑈 )
71 70 adantr ⊢ ( ( ( ( 𝜑 ∧ 𝑟 ∈ ( ( Base ‘ 𝑊 ) ∖ { 0 } ) ) ∧ ( 𝑦 ∈ 𝑇 ∧ 𝑧 ∈ 𝑈 ) ∧ 𝑟 = ( 𝑦 ( +g ‘ 𝑊 ) 𝑧 ) ) ∧ ( 𝑦 = 0 ∧ 𝑞 ∈ 𝑇 ∧ 𝑞 ≠ 0 ) ) → ( ( LSpan ‘ 𝑊 ) ‘ { 𝑧 } ) ⊆ 𝑈 )
72 69 71 eqsstrd ⊢ ( ( ( ( 𝜑 ∧ 𝑟 ∈ ( ( Base ‘ 𝑊 ) ∖ { 0 } ) ) ∧ ( 𝑦 ∈ 𝑇 ∧ 𝑧 ∈ 𝑈 ) ∧ 𝑟 = ( 𝑦 ( +g ‘ 𝑊 ) 𝑧 ) ) ∧ ( 𝑦 = 0 ∧ 𝑞 ∈ 𝑇 ∧ 𝑞 ≠ 0 ) ) → ( ( LSpan ‘ 𝑊 ) ‘ { 𝑟 } ) ⊆ 𝑈 )
73 11 12 lspsnsubg ⊢ ( ( 𝑊 ∈ LMod ∧ 𝑞 ∈ ( Base ‘ 𝑊 ) ) → ( ( LSpan ‘ 𝑊 ) ‘ { 𝑞 } ) ∈ ( SubGrp ‘ 𝑊 ) )
74 45 51 73 syl2anc ⊢ ( ( ( ( 𝜑 ∧ 𝑟 ∈ ( ( Base ‘ 𝑊 ) ∖ { 0 } ) ) ∧ ( 𝑦 ∈ 𝑇 ∧ 𝑧 ∈ 𝑈 ) ∧ 𝑟 = ( 𝑦 ( +g ‘ 𝑊 ) 𝑧 ) ) ∧ ( 𝑦 = 0 ∧ 𝑞 ∈ 𝑇 ∧ 𝑞 ≠ 0 ) ) → ( ( LSpan ‘ 𝑊 ) ‘ { 𝑞 } ) ∈ ( SubGrp ‘ 𝑊 ) )
75 45 27 syl ⊢ ( ( ( ( 𝜑 ∧ 𝑟 ∈ ( ( Base ‘ 𝑊 ) ∖ { 0 } ) ) ∧ ( 𝑦 ∈ 𝑇 ∧ 𝑧 ∈ 𝑈 ) ∧ 𝑟 = ( 𝑦 ( +g ‘ 𝑊 ) 𝑧 ) ) ∧ ( 𝑦 = 0 ∧ 𝑞 ∈ 𝑇 ∧ 𝑞 ≠ 0 ) ) → 𝑆 ⊆ ( SubGrp ‘ 𝑊 ) )
76 60 adantr ⊢ ( ( ( ( 𝜑 ∧ 𝑟 ∈ ( ( Base ‘ 𝑊 ) ∖ { 0 } ) ) ∧ ( 𝑦 ∈ 𝑇 ∧ 𝑧 ∈ 𝑈 ) ∧ 𝑟 = ( 𝑦 ( +g ‘ 𝑊 ) 𝑧 ) ) ∧ ( 𝑦 = 0 ∧ 𝑞 ∈ 𝑇 ∧ 𝑞 ≠ 0 ) ) → 𝑈 ∈ 𝑆 )
77 75 76 sseldd ⊢ ( ( ( ( 𝜑 ∧ 𝑟 ∈ ( ( Base ‘ 𝑊 ) ∖ { 0 } ) ) ∧ ( 𝑦 ∈ 𝑇 ∧ 𝑧 ∈ 𝑈 ) ∧ 𝑟 = ( 𝑦 ( +g ‘ 𝑊 ) 𝑧 ) ) ∧ ( 𝑦 = 0 ∧ 𝑞 ∈ 𝑇 ∧ 𝑞 ≠ 0 ) ) → 𝑈 ∈ ( SubGrp ‘ 𝑊 ) )
78 3 lsmub2 ⊢ ( ( ( ( LSpan ‘ 𝑊 ) ‘ { 𝑞 } ) ∈ ( SubGrp ‘ 𝑊 ) ∧ 𝑈 ∈ ( SubGrp ‘ 𝑊 ) ) → 𝑈 ⊆ ( ( ( LSpan ‘ 𝑊 ) ‘ { 𝑞 } ) ⊕ 𝑈 ) )
79 74 77 78 syl2anc ⊢ ( ( ( ( 𝜑 ∧ 𝑟 ∈ ( ( Base ‘ 𝑊 ) ∖ { 0 } ) ) ∧ ( 𝑦 ∈ 𝑇 ∧ 𝑧 ∈ 𝑈 ) ∧ 𝑟 = ( 𝑦 ( +g ‘ 𝑊 ) 𝑧 ) ) ∧ ( 𝑦 = 0 ∧ 𝑞 ∈ 𝑇 ∧ 𝑞 ≠ 0 ) ) → 𝑈 ⊆ ( ( ( LSpan ‘ 𝑊 ) ‘ { 𝑞 } ) ⊕ 𝑈 ) )
80 72 79 sstrd ⊢ ( ( ( ( 𝜑 ∧ 𝑟 ∈ ( ( Base ‘ 𝑊 ) ∖ { 0 } ) ) ∧ ( 𝑦 ∈ 𝑇 ∧ 𝑧 ∈ 𝑈 ) ∧ 𝑟 = ( 𝑦 ( +g ‘ 𝑊 ) 𝑧 ) ) ∧ ( 𝑦 = 0 ∧ 𝑞 ∈ 𝑇 ∧ 𝑞 ≠ 0 ) ) → ( ( LSpan ‘ 𝑊 ) ‘ { 𝑟 } ) ⊆ ( ( ( LSpan ‘ 𝑊 ) ‘ { 𝑞 } ) ⊕ 𝑈 ) )
81 sseq1 ⊢ ( 𝑝 = ( ( LSpan ‘ 𝑊 ) ‘ { 𝑞 } ) → ( 𝑝 ⊆ 𝑇 ↔ ( ( LSpan ‘ 𝑊 ) ‘ { 𝑞 } ) ⊆ 𝑇 ) )
82 oveq1 ⊢ ( 𝑝 = ( ( LSpan ‘ 𝑊 ) ‘ { 𝑞 } ) → ( 𝑝 ⊕ 𝑈 ) = ( ( ( LSpan ‘ 𝑊 ) ‘ { 𝑞 } ) ⊕ 𝑈 ) )
83 82 sseq2d ⊢ ( 𝑝 = ( ( LSpan ‘ 𝑊 ) ‘ { 𝑞 } ) → ( ( ( LSpan ‘ 𝑊 ) ‘ { 𝑟 } ) ⊆ ( 𝑝 ⊕ 𝑈 ) ↔ ( ( LSpan ‘ 𝑊 ) ‘ { 𝑟 } ) ⊆ ( ( ( LSpan ‘ 𝑊 ) ‘ { 𝑞 } ) ⊕ 𝑈 ) ) )
84 81 83 anbi12d ⊢ ( 𝑝 = ( ( LSpan ‘ 𝑊 ) ‘ { 𝑞 } ) → ( ( 𝑝 ⊆ 𝑇 ∧ ( ( LSpan ‘ 𝑊 ) ‘ { 𝑟 } ) ⊆ ( 𝑝 ⊕ 𝑈 ) ) ↔ ( ( ( LSpan ‘ 𝑊 ) ‘ { 𝑞 } ) ⊆ 𝑇 ∧ ( ( LSpan ‘ 𝑊 ) ‘ { 𝑟 } ) ⊆ ( ( ( LSpan ‘ 𝑊 ) ‘ { 𝑞 } ) ⊕ 𝑈 ) ) ) )
85 84 rspcev ⊢ ( ( ( ( LSpan ‘ 𝑊 ) ‘ { 𝑞 } ) ∈ 𝐴 ∧ ( ( ( LSpan ‘ 𝑊 ) ‘ { 𝑞 } ) ⊆ 𝑇 ∧ ( ( LSpan ‘ 𝑊 ) ‘ { 𝑟 } ) ⊆ ( ( ( LSpan ‘ 𝑊 ) ‘ { 𝑞 } ) ⊕ 𝑈 ) ) ) → ∃ 𝑝 ∈ 𝐴 ( 𝑝 ⊆ 𝑇 ∧ ( ( LSpan ‘ 𝑊 ) ‘ { 𝑟 } ) ⊆ ( 𝑝 ⊕ 𝑈 ) ) )
86 54 55 80 85 syl12anc ⊢ ( ( ( ( 𝜑 ∧ 𝑟 ∈ ( ( Base ‘ 𝑊 ) ∖ { 0 } ) ) ∧ ( 𝑦 ∈ 𝑇 ∧ 𝑧 ∈ 𝑈 ) ∧ 𝑟 = ( 𝑦 ( +g ‘ 𝑊 ) 𝑧 ) ) ∧ ( 𝑦 = 0 ∧ 𝑞 ∈ 𝑇 ∧ 𝑞 ≠ 0 ) ) → ∃ 𝑝 ∈ 𝐴 ( 𝑝 ⊆ 𝑇 ∧ ( ( LSpan ‘ 𝑊 ) ‘ { 𝑟 } ) ⊆ ( 𝑝 ⊕ 𝑈 ) ) )
87 86 3exp2 ⊢ ( ( ( 𝜑 ∧ 𝑟 ∈ ( ( Base ‘ 𝑊 ) ∖ { 0 } ) ) ∧ ( 𝑦 ∈ 𝑇 ∧ 𝑧 ∈ 𝑈 ) ∧ 𝑟 = ( 𝑦 ( +g ‘ 𝑊 ) 𝑧 ) ) → ( 𝑦 = 0 → ( 𝑞 ∈ 𝑇 → ( 𝑞 ≠ 0 → ∃ 𝑝 ∈ 𝐴 ( 𝑝 ⊆ 𝑇 ∧ ( ( LSpan ‘ 𝑊 ) ‘ { 𝑟 } ) ⊆ ( 𝑝 ⊕ 𝑈 ) ) ) ) ) )
88 87 imp ⊢ ( ( ( ( 𝜑 ∧ 𝑟 ∈ ( ( Base ‘ 𝑊 ) ∖ { 0 } ) ) ∧ ( 𝑦 ∈ 𝑇 ∧ 𝑧 ∈ 𝑈 ) ∧ 𝑟 = ( 𝑦 ( +g ‘ 𝑊 ) 𝑧 ) ) ∧ 𝑦 = 0 ) → ( 𝑞 ∈ 𝑇 → ( 𝑞 ≠ 0 → ∃ 𝑝 ∈ 𝐴 ( 𝑝 ⊆ 𝑇 ∧ ( ( LSpan ‘ 𝑊 ) ‘ { 𝑟 } ) ⊆ ( 𝑝 ⊕ 𝑈 ) ) ) ) )
89 88 rexlimdv ⊢ ( ( ( ( 𝜑 ∧ 𝑟 ∈ ( ( Base ‘ 𝑊 ) ∖ { 0 } ) ) ∧ ( 𝑦 ∈ 𝑇 ∧ 𝑧 ∈ 𝑈 ) ∧ 𝑟 = ( 𝑦 ( +g ‘ 𝑊 ) 𝑧 ) ) ∧ 𝑦 = 0 ) → ( ∃ 𝑞 ∈ 𝑇 𝑞 ≠ 0 → ∃ 𝑝 ∈ 𝐴 ( 𝑝 ⊆ 𝑇 ∧ ( ( LSpan ‘ 𝑊 ) ‘ { 𝑟 } ) ⊆ ( 𝑝 ⊕ 𝑈 ) ) ) )
90 42 89 mpd ⊢ ( ( ( ( 𝜑 ∧ 𝑟 ∈ ( ( Base ‘ 𝑊 ) ∖ { 0 } ) ) ∧ ( 𝑦 ∈ 𝑇 ∧ 𝑧 ∈ 𝑈 ) ∧ 𝑟 = ( 𝑦 ( +g ‘ 𝑊 ) 𝑧 ) ) ∧ 𝑦 = 0 ) → ∃ 𝑝 ∈ 𝐴 ( 𝑝 ⊆ 𝑇 ∧ ( ( LSpan ‘ 𝑊 ) ‘ { 𝑟 } ) ⊆ ( 𝑝 ⊕ 𝑈 ) ) )
91 44 adantr ⊢ ( ( ( ( 𝜑 ∧ 𝑟 ∈ ( ( Base ‘ 𝑊 ) ∖ { 0 } ) ) ∧ ( 𝑦 ∈ 𝑇 ∧ 𝑧 ∈ 𝑈 ) ∧ 𝑟 = ( 𝑦 ( +g ‘ 𝑊 ) 𝑧 ) ) ∧ 𝑦 ≠ 0 ) → 𝑊 ∈ LMod )
92 simp2l ⊢ ( ( ( 𝜑 ∧ 𝑟 ∈ ( ( Base ‘ 𝑊 ) ∖ { 0 } ) ) ∧ ( 𝑦 ∈ 𝑇 ∧ 𝑧 ∈ 𝑈 ) ∧ 𝑟 = ( 𝑦 ( +g ‘ 𝑊 ) 𝑧 ) ) → 𝑦 ∈ 𝑇 )
93 11 2 lssel ⊢ ( ( 𝑇 ∈ 𝑆 ∧ 𝑦 ∈ 𝑇 ) → 𝑦 ∈ ( Base ‘ 𝑊 ) )
94 47 92 93 syl2anc ⊢ ( ( ( 𝜑 ∧ 𝑟 ∈ ( ( Base ‘ 𝑊 ) ∖ { 0 } ) ) ∧ ( 𝑦 ∈ 𝑇 ∧ 𝑧 ∈ 𝑈 ) ∧ 𝑟 = ( 𝑦 ( +g ‘ 𝑊 ) 𝑧 ) ) → 𝑦 ∈ ( Base ‘ 𝑊 ) )
95 94 adantr ⊢ ( ( ( ( 𝜑 ∧ 𝑟 ∈ ( ( Base ‘ 𝑊 ) ∖ { 0 } ) ) ∧ ( 𝑦 ∈ 𝑇 ∧ 𝑧 ∈ 𝑈 ) ∧ 𝑟 = ( 𝑦 ( +g ‘ 𝑊 ) 𝑧 ) ) ∧ 𝑦 ≠ 0 ) → 𝑦 ∈ ( Base ‘ 𝑊 ) )
96 simpr ⊢ ( ( ( ( 𝜑 ∧ 𝑟 ∈ ( ( Base ‘ 𝑊 ) ∖ { 0 } ) ) ∧ ( 𝑦 ∈ 𝑇 ∧ 𝑧 ∈ 𝑈 ) ∧ 𝑟 = ( 𝑦 ( +g ‘ 𝑊 ) 𝑧 ) ) ∧ 𝑦 ≠ 0 ) → 𝑦 ≠ 0 )
97 11 12 1 4 lsatlspsn2 ⊢ ( ( 𝑊 ∈ LMod ∧ 𝑦 ∈ ( Base ‘ 𝑊 ) ∧ 𝑦 ≠ 0 ) → ( ( LSpan ‘ 𝑊 ) ‘ { 𝑦 } ) ∈ 𝐴 )
98 91 95 96 97 syl3anc ⊢ ( ( ( ( 𝜑 ∧ 𝑟 ∈ ( ( Base ‘ 𝑊 ) ∖ { 0 } ) ) ∧ ( 𝑦 ∈ 𝑇 ∧ 𝑧 ∈ 𝑈 ) ∧ 𝑟 = ( 𝑦 ( +g ‘ 𝑊 ) 𝑧 ) ) ∧ 𝑦 ≠ 0 ) → ( ( LSpan ‘ 𝑊 ) ‘ { 𝑦 } ) ∈ 𝐴 )
99 2 12 44 47 92 ellspsn5 ⊢ ( ( ( 𝜑 ∧ 𝑟 ∈ ( ( Base ‘ 𝑊 ) ∖ { 0 } ) ) ∧ ( 𝑦 ∈ 𝑇 ∧ 𝑧 ∈ 𝑈 ) ∧ 𝑟 = ( 𝑦 ( +g ‘ 𝑊 ) 𝑧 ) ) → ( ( LSpan ‘ 𝑊 ) ‘ { 𝑦 } ) ⊆ 𝑇 )
100 99 adantr ⊢ ( ( ( ( 𝜑 ∧ 𝑟 ∈ ( ( Base ‘ 𝑊 ) ∖ { 0 } ) ) ∧ ( 𝑦 ∈ 𝑇 ∧ 𝑧 ∈ 𝑈 ) ∧ 𝑟 = ( 𝑦 ( +g ‘ 𝑊 ) 𝑧 ) ) ∧ 𝑦 ≠ 0 ) → ( ( LSpan ‘ 𝑊 ) ‘ { 𝑦 } ) ⊆ 𝑇 )
101 simp3 ⊢ ( ( ( 𝜑 ∧ 𝑟 ∈ ( ( Base ‘ 𝑊 ) ∖ { 0 } ) ) ∧ ( 𝑦 ∈ 𝑇 ∧ 𝑧 ∈ 𝑈 ) ∧ 𝑟 = ( 𝑦 ( +g ‘ 𝑊 ) 𝑧 ) ) → 𝑟 = ( 𝑦 ( +g ‘ 𝑊 ) 𝑧 ) )
102 101 sneqd ⊢ ( ( ( 𝜑 ∧ 𝑟 ∈ ( ( Base ‘ 𝑊 ) ∖ { 0 } ) ) ∧ ( 𝑦 ∈ 𝑇 ∧ 𝑧 ∈ 𝑈 ) ∧ 𝑟 = ( 𝑦 ( +g ‘ 𝑊 ) 𝑧 ) ) → { 𝑟 } = { ( 𝑦 ( +g ‘ 𝑊 ) 𝑧 ) } )
103 102 fveq2d ⊢ ( ( ( 𝜑 ∧ 𝑟 ∈ ( ( Base ‘ 𝑊 ) ∖ { 0 } ) ) ∧ ( 𝑦 ∈ 𝑇 ∧ 𝑧 ∈ 𝑈 ) ∧ 𝑟 = ( 𝑦 ( +g ‘ 𝑊 ) 𝑧 ) ) → ( ( LSpan ‘ 𝑊 ) ‘ { 𝑟 } ) = ( ( LSpan ‘ 𝑊 ) ‘ { ( 𝑦 ( +g ‘ 𝑊 ) 𝑧 ) } ) )
104 11 33 12 lspvadd ⊢ ( ( 𝑊 ∈ LMod ∧ 𝑦 ∈ ( Base ‘ 𝑊 ) ∧ 𝑧 ∈ ( Base ‘ 𝑊 ) ) → ( ( LSpan ‘ 𝑊 ) ‘ { ( 𝑦 ( +g ‘ 𝑊 ) 𝑧 ) } ) ⊆ ( ( LSpan ‘ 𝑊 ) ‘ { 𝑦 , 𝑧 } ) )
105 44 94 63 104 syl3anc ⊢ ( ( ( 𝜑 ∧ 𝑟 ∈ ( ( Base ‘ 𝑊 ) ∖ { 0 } ) ) ∧ ( 𝑦 ∈ 𝑇 ∧ 𝑧 ∈ 𝑈 ) ∧ 𝑟 = ( 𝑦 ( +g ‘ 𝑊 ) 𝑧 ) ) → ( ( LSpan ‘ 𝑊 ) ‘ { ( 𝑦 ( +g ‘ 𝑊 ) 𝑧 ) } ) ⊆ ( ( LSpan ‘ 𝑊 ) ‘ { 𝑦 , 𝑧 } ) )
106 103 105 eqsstrd ⊢ ( ( ( 𝜑 ∧ 𝑟 ∈ ( ( Base ‘ 𝑊 ) ∖ { 0 } ) ) ∧ ( 𝑦 ∈ 𝑇 ∧ 𝑧 ∈ 𝑈 ) ∧ 𝑟 = ( 𝑦 ( +g ‘ 𝑊 ) 𝑧 ) ) → ( ( LSpan ‘ 𝑊 ) ‘ { 𝑟 } ) ⊆ ( ( LSpan ‘ 𝑊 ) ‘ { 𝑦 , 𝑧 } ) )
107 11 12 3 44 94 63 lsmpr ⊢ ( ( ( 𝜑 ∧ 𝑟 ∈ ( ( Base ‘ 𝑊 ) ∖ { 0 } ) ) ∧ ( 𝑦 ∈ 𝑇 ∧ 𝑧 ∈ 𝑈 ) ∧ 𝑟 = ( 𝑦 ( +g ‘ 𝑊 ) 𝑧 ) ) → ( ( LSpan ‘ 𝑊 ) ‘ { 𝑦 , 𝑧 } ) = ( ( ( LSpan ‘ 𝑊 ) ‘ { 𝑦 } ) ⊕ ( ( LSpan ‘ 𝑊 ) ‘ { 𝑧 } ) ) )
108 106 107 sseqtrd ⊢ ( ( ( 𝜑 ∧ 𝑟 ∈ ( ( Base ‘ 𝑊 ) ∖ { 0 } ) ) ∧ ( 𝑦 ∈ 𝑇 ∧ 𝑧 ∈ 𝑈 ) ∧ 𝑟 = ( 𝑦 ( +g ‘ 𝑊 ) 𝑧 ) ) → ( ( LSpan ‘ 𝑊 ) ‘ { 𝑟 } ) ⊆ ( ( ( LSpan ‘ 𝑊 ) ‘ { 𝑦 } ) ⊕ ( ( LSpan ‘ 𝑊 ) ‘ { 𝑧 } ) ) )
109 44 27 syl ⊢ ( ( ( 𝜑 ∧ 𝑟 ∈ ( ( Base ‘ 𝑊 ) ∖ { 0 } ) ) ∧ ( 𝑦 ∈ 𝑇 ∧ 𝑧 ∈ 𝑈 ) ∧ 𝑟 = ( 𝑦 ( +g ‘ 𝑊 ) 𝑧 ) ) → 𝑆 ⊆ ( SubGrp ‘ 𝑊 ) )
110 11 2 12 lspsncl ⊢ ( ( 𝑊 ∈ LMod ∧ 𝑦 ∈ ( Base ‘ 𝑊 ) ) → ( ( LSpan ‘ 𝑊 ) ‘ { 𝑦 } ) ∈ 𝑆 )
111 44 94 110 syl2anc ⊢ ( ( ( 𝜑 ∧ 𝑟 ∈ ( ( Base ‘ 𝑊 ) ∖ { 0 } ) ) ∧ ( 𝑦 ∈ 𝑇 ∧ 𝑧 ∈ 𝑈 ) ∧ 𝑟 = ( 𝑦 ( +g ‘ 𝑊 ) 𝑧 ) ) → ( ( LSpan ‘ 𝑊 ) ‘ { 𝑦 } ) ∈ 𝑆 )
112 109 111 sseldd ⊢ ( ( ( 𝜑 ∧ 𝑟 ∈ ( ( Base ‘ 𝑊 ) ∖ { 0 } ) ) ∧ ( 𝑦 ∈ 𝑇 ∧ 𝑧 ∈ 𝑈 ) ∧ 𝑟 = ( 𝑦 ( +g ‘ 𝑊 ) 𝑧 ) ) → ( ( LSpan ‘ 𝑊 ) ‘ { 𝑦 } ) ∈ ( SubGrp ‘ 𝑊 ) )
113 109 60 sseldd ⊢ ( ( ( 𝜑 ∧ 𝑟 ∈ ( ( Base ‘ 𝑊 ) ∖ { 0 } ) ) ∧ ( 𝑦 ∈ 𝑇 ∧ 𝑧 ∈ 𝑈 ) ∧ 𝑟 = ( 𝑦 ( +g ‘ 𝑊 ) 𝑧 ) ) → 𝑈 ∈ ( SubGrp ‘ 𝑊 ) )
114 3 lsmless2 ⊢ ( ( ( ( LSpan ‘ 𝑊 ) ‘ { 𝑦 } ) ∈ ( SubGrp ‘ 𝑊 ) ∧ 𝑈 ∈ ( SubGrp ‘ 𝑊 ) ∧ ( ( LSpan ‘ 𝑊 ) ‘ { 𝑧 } ) ⊆ 𝑈 ) → ( ( ( LSpan ‘ 𝑊 ) ‘ { 𝑦 } ) ⊕ ( ( LSpan ‘ 𝑊 ) ‘ { 𝑧 } ) ) ⊆ ( ( ( LSpan ‘ 𝑊 ) ‘ { 𝑦 } ) ⊕ 𝑈 ) )
115 112 113 70 114 syl3anc ⊢ ( ( ( 𝜑 ∧ 𝑟 ∈ ( ( Base ‘ 𝑊 ) ∖ { 0 } ) ) ∧ ( 𝑦 ∈ 𝑇 ∧ 𝑧 ∈ 𝑈 ) ∧ 𝑟 = ( 𝑦 ( +g ‘ 𝑊 ) 𝑧 ) ) → ( ( ( LSpan ‘ 𝑊 ) ‘ { 𝑦 } ) ⊕ ( ( LSpan ‘ 𝑊 ) ‘ { 𝑧 } ) ) ⊆ ( ( ( LSpan ‘ 𝑊 ) ‘ { 𝑦 } ) ⊕ 𝑈 ) )
116 108 115 sstrd ⊢ ( ( ( 𝜑 ∧ 𝑟 ∈ ( ( Base ‘ 𝑊 ) ∖ { 0 } ) ) ∧ ( 𝑦 ∈ 𝑇 ∧ 𝑧 ∈ 𝑈 ) ∧ 𝑟 = ( 𝑦 ( +g ‘ 𝑊 ) 𝑧 ) ) → ( ( LSpan ‘ 𝑊 ) ‘ { 𝑟 } ) ⊆ ( ( ( LSpan ‘ 𝑊 ) ‘ { 𝑦 } ) ⊕ 𝑈 ) )
117 116 adantr ⊢ ( ( ( ( 𝜑 ∧ 𝑟 ∈ ( ( Base ‘ 𝑊 ) ∖ { 0 } ) ) ∧ ( 𝑦 ∈ 𝑇 ∧ 𝑧 ∈ 𝑈 ) ∧ 𝑟 = ( 𝑦 ( +g ‘ 𝑊 ) 𝑧 ) ) ∧ 𝑦 ≠ 0 ) → ( ( LSpan ‘ 𝑊 ) ‘ { 𝑟 } ) ⊆ ( ( ( LSpan ‘ 𝑊 ) ‘ { 𝑦 } ) ⊕ 𝑈 ) )
118 sseq1 ⊢ ( 𝑝 = ( ( LSpan ‘ 𝑊 ) ‘ { 𝑦 } ) → ( 𝑝 ⊆ 𝑇 ↔ ( ( LSpan ‘ 𝑊 ) ‘ { 𝑦 } ) ⊆ 𝑇 ) )
119 oveq1 ⊢ ( 𝑝 = ( ( LSpan ‘ 𝑊 ) ‘ { 𝑦 } ) → ( 𝑝 ⊕ 𝑈 ) = ( ( ( LSpan ‘ 𝑊 ) ‘ { 𝑦 } ) ⊕ 𝑈 ) )
120 119 sseq2d ⊢ ( 𝑝 = ( ( LSpan ‘ 𝑊 ) ‘ { 𝑦 } ) → ( ( ( LSpan ‘ 𝑊 ) ‘ { 𝑟 } ) ⊆ ( 𝑝 ⊕ 𝑈 ) ↔ ( ( LSpan ‘ 𝑊 ) ‘ { 𝑟 } ) ⊆ ( ( ( LSpan ‘ 𝑊 ) ‘ { 𝑦 } ) ⊕ 𝑈 ) ) )
121 118 120 anbi12d ⊢ ( 𝑝 = ( ( LSpan ‘ 𝑊 ) ‘ { 𝑦 } ) → ( ( 𝑝 ⊆ 𝑇 ∧ ( ( LSpan ‘ 𝑊 ) ‘ { 𝑟 } ) ⊆ ( 𝑝 ⊕ 𝑈 ) ) ↔ ( ( ( LSpan ‘ 𝑊 ) ‘ { 𝑦 } ) ⊆ 𝑇 ∧ ( ( LSpan ‘ 𝑊 ) ‘ { 𝑟 } ) ⊆ ( ( ( LSpan ‘ 𝑊 ) ‘ { 𝑦 } ) ⊕ 𝑈 ) ) ) )
122 121 rspcev ⊢ ( ( ( ( LSpan ‘ 𝑊 ) ‘ { 𝑦 } ) ∈ 𝐴 ∧ ( ( ( LSpan ‘ 𝑊 ) ‘ { 𝑦 } ) ⊆ 𝑇 ∧ ( ( LSpan ‘ 𝑊 ) ‘ { 𝑟 } ) ⊆ ( ( ( LSpan ‘ 𝑊 ) ‘ { 𝑦 } ) ⊕ 𝑈 ) ) ) → ∃ 𝑝 ∈ 𝐴 ( 𝑝 ⊆ 𝑇 ∧ ( ( LSpan ‘ 𝑊 ) ‘ { 𝑟 } ) ⊆ ( 𝑝 ⊕ 𝑈 ) ) )
123 98 100 117 122 syl12anc ⊢ ( ( ( ( 𝜑 ∧ 𝑟 ∈ ( ( Base ‘ 𝑊 ) ∖ { 0 } ) ) ∧ ( 𝑦 ∈ 𝑇 ∧ 𝑧 ∈ 𝑈 ) ∧ 𝑟 = ( 𝑦 ( +g ‘ 𝑊 ) 𝑧 ) ) ∧ 𝑦 ≠ 0 ) → ∃ 𝑝 ∈ 𝐴 ( 𝑝 ⊆ 𝑇 ∧ ( ( LSpan ‘ 𝑊 ) ‘ { 𝑟 } ) ⊆ ( 𝑝 ⊕ 𝑈 ) ) )
124 90 123 pm2.61dane ⊢ ( ( ( 𝜑 ∧ 𝑟 ∈ ( ( Base ‘ 𝑊 ) ∖ { 0 } ) ) ∧ ( 𝑦 ∈ 𝑇 ∧ 𝑧 ∈ 𝑈 ) ∧ 𝑟 = ( 𝑦 ( +g ‘ 𝑊 ) 𝑧 ) ) → ∃ 𝑝 ∈ 𝐴 ( 𝑝 ⊆ 𝑇 ∧ ( ( LSpan ‘ 𝑊 ) ‘ { 𝑟 } ) ⊆ ( 𝑝 ⊕ 𝑈 ) ) )
125 124 3exp ⊢ ( ( 𝜑 ∧ 𝑟 ∈ ( ( Base ‘ 𝑊 ) ∖ { 0 } ) ) → ( ( 𝑦 ∈ 𝑇 ∧ 𝑧 ∈ 𝑈 ) → ( 𝑟 = ( 𝑦 ( +g ‘ 𝑊 ) 𝑧 ) → ∃ 𝑝 ∈ 𝐴 ( 𝑝 ⊆ 𝑇 ∧ ( ( LSpan ‘ 𝑊 ) ‘ { 𝑟 } ) ⊆ ( 𝑝 ⊕ 𝑈 ) ) ) ) )
126 125 rexlimdvv ⊢ ( ( 𝜑 ∧ 𝑟 ∈ ( ( Base ‘ 𝑊 ) ∖ { 0 } ) ) → ( ∃ 𝑦 ∈ 𝑇 ∃ 𝑧 ∈ 𝑈 𝑟 = ( 𝑦 ( +g ‘ 𝑊 ) 𝑧 ) → ∃ 𝑝 ∈ 𝐴 ( 𝑝 ⊆ 𝑇 ∧ ( ( LSpan ‘ 𝑊 ) ‘ { 𝑟 } ) ⊆ ( 𝑝 ⊕ 𝑈 ) ) ) )
127 126 3adant3 ⊢ ( ( 𝜑 ∧ 𝑟 ∈ ( ( Base ‘ 𝑊 ) ∖ { 0 } ) ∧ 𝑄 = ( ( LSpan ‘ 𝑊 ) ‘ { 𝑟 } ) ) → ( ∃ 𝑦 ∈ 𝑇 ∃ 𝑧 ∈ 𝑈 𝑟 = ( 𝑦 ( +g ‘ 𝑊 ) 𝑧 ) → ∃ 𝑝 ∈ 𝐴 ( 𝑝 ⊆ 𝑇 ∧ ( ( LSpan ‘ 𝑊 ) ‘ { 𝑟 } ) ⊆ ( 𝑝 ⊕ 𝑈 ) ) ) )
128 36 127 mpd ⊢ ( ( 𝜑 ∧ 𝑟 ∈ ( ( Base ‘ 𝑊 ) ∖ { 0 } ) ∧ 𝑄 = ( ( LSpan ‘ 𝑊 ) ‘ { 𝑟 } ) ) → ∃ 𝑝 ∈ 𝐴 ( 𝑝 ⊆ 𝑇 ∧ ( ( LSpan ‘ 𝑊 ) ‘ { 𝑟 } ) ⊆ ( 𝑝 ⊕ 𝑈 ) ) )
129 sseq1 ⊢ ( 𝑄 = ( ( LSpan ‘ 𝑊 ) ‘ { 𝑟 } ) → ( 𝑄 ⊆ ( 𝑝 ⊕ 𝑈 ) ↔ ( ( LSpan ‘ 𝑊 ) ‘ { 𝑟 } ) ⊆ ( 𝑝 ⊕ 𝑈 ) ) )
130 129 anbi2d ⊢ ( 𝑄 = ( ( LSpan ‘ 𝑊 ) ‘ { 𝑟 } ) → ( ( 𝑝 ⊆ 𝑇 ∧ 𝑄 ⊆ ( 𝑝 ⊕ 𝑈 ) ) ↔ ( 𝑝 ⊆ 𝑇 ∧ ( ( LSpan ‘ 𝑊 ) ‘ { 𝑟 } ) ⊆ ( 𝑝 ⊕ 𝑈 ) ) ) )
131 130 rexbidv ⊢ ( 𝑄 = ( ( LSpan ‘ 𝑊 ) ‘ { 𝑟 } ) → ( ∃ 𝑝 ∈ 𝐴 ( 𝑝 ⊆ 𝑇 ∧ 𝑄 ⊆ ( 𝑝 ⊕ 𝑈 ) ) ↔ ∃ 𝑝 ∈ 𝐴 ( 𝑝 ⊆ 𝑇 ∧ ( ( LSpan ‘ 𝑊 ) ‘ { 𝑟 } ) ⊆ ( 𝑝 ⊕ 𝑈 ) ) ) )
132 131 3ad2ant3 ⊢ ( ( 𝜑 ∧ 𝑟 ∈ ( ( Base ‘ 𝑊 ) ∖ { 0 } ) ∧ 𝑄 = ( ( LSpan ‘ 𝑊 ) ‘ { 𝑟 } ) ) → ( ∃ 𝑝 ∈ 𝐴 ( 𝑝 ⊆ 𝑇 ∧ 𝑄 ⊆ ( 𝑝 ⊕ 𝑈 ) ) ↔ ∃ 𝑝 ∈ 𝐴 ( 𝑝 ⊆ 𝑇 ∧ ( ( LSpan ‘ 𝑊 ) ‘ { 𝑟 } ) ⊆ ( 𝑝 ⊕ 𝑈 ) ) ) )
133 128 132 mpbird ⊢ ( ( 𝜑 ∧ 𝑟 ∈ ( ( Base ‘ 𝑊 ) ∖ { 0 } ) ∧ 𝑄 = ( ( LSpan ‘ 𝑊 ) ‘ { 𝑟 } ) ) → ∃ 𝑝 ∈ 𝐴 ( 𝑝 ⊆ 𝑇 ∧ 𝑄 ⊆ ( 𝑝 ⊕ 𝑈 ) ) )
134 133 3exp ⊢ ( 𝜑 → ( 𝑟 ∈ ( ( Base ‘ 𝑊 ) ∖ { 0 } ) → ( 𝑄 = ( ( LSpan ‘ 𝑊 ) ‘ { 𝑟 } ) → ∃ 𝑝 ∈ 𝐴 ( 𝑝 ⊆ 𝑇 ∧ 𝑄 ⊆ ( 𝑝 ⊕ 𝑈 ) ) ) ) )
135 134 rexlimdv ⊢ ( 𝜑 → ( ∃ 𝑟 ∈ ( ( Base ‘ 𝑊 ) ∖ { 0 } ) 𝑄 = ( ( LSpan ‘ 𝑊 ) ‘ { 𝑟 } ) → ∃ 𝑝 ∈ 𝐴 ( 𝑝 ⊆ 𝑇 ∧ 𝑄 ⊆ ( 𝑝 ⊕ 𝑈 ) ) ) )
136 15 135 mpd ⊢ ( 𝜑 → ∃ 𝑝 ∈ 𝐴 ( 𝑝 ⊆ 𝑇 ∧ 𝑄 ⊆ ( 𝑝 ⊕ 𝑈 ) ) )