Metamath Proof Explorer

Theorem lsmelval2

Description: Subspace sum membership in terms of a sum of 1-dim subspaces (atoms), which can be useful for treating subspaces as projective lattice elements. (Contributed by NM, 9-Aug-2014)

Ref Expression
Hypotheses lsmelval2.v ⊢ 𝑉 = ( Base ‘ 𝑊 )
lsmelval2.s ⊢ 𝑆 = ( LSubSp ‘ 𝑊 )
lsmelval2.p ⊢ ⊕ = ( LSSum ‘ 𝑊 )
lsmelval2.n ⊢ 𝑁 = ( LSpan ‘ 𝑊 )
lsmelval2.w ⊢ ( 𝜑 → 𝑊 ∈ LMod )
lsmelval2.t ⊢ ( 𝜑 → 𝑇 ∈ 𝑆 )
lsmelval2.u ⊢ ( 𝜑 → 𝑈 ∈ 𝑆 )
Assertion lsmelval2 ( 𝜑 → ( 𝑋 ∈ ( 𝑇 ⊕ 𝑈 ) ↔ ( 𝑋 ∈ 𝑉 ∧ ∃ 𝑦 ∈ 𝑇 ∃ 𝑧 ∈ 𝑈 ( 𝑁 ‘ { 𝑋 } ) ⊆ ( ( 𝑁 ‘ { 𝑦 } ) ⊕ ( 𝑁 ‘ { 𝑧 } ) ) ) ) )

Proof

Step Hyp Ref Expression
1 lsmelval2.v ⊢ 𝑉 = ( Base ‘ 𝑊 )
2 lsmelval2.s ⊢ 𝑆 = ( LSubSp ‘ 𝑊 )
3 lsmelval2.p ⊢ ⊕ = ( LSSum ‘ 𝑊 )
4 lsmelval2.n ⊢ 𝑁 = ( LSpan ‘ 𝑊 )
5 lsmelval2.w ⊢ ( 𝜑 → 𝑊 ∈ LMod )
6 lsmelval2.t ⊢ ( 𝜑 → 𝑇 ∈ 𝑆 )
7 lsmelval2.u ⊢ ( 𝜑 → 𝑈 ∈ 𝑆 )
8 2 lsssubg ⊢ ( ( 𝑊 ∈ LMod ∧ 𝑇 ∈ 𝑆 ) → 𝑇 ∈ ( SubGrp ‘ 𝑊 ) )
9 5 6 8 syl2anc ⊢ ( 𝜑 → 𝑇 ∈ ( SubGrp ‘ 𝑊 ) )
10 2 lsssubg ⊢ ( ( 𝑊 ∈ LMod ∧ 𝑈 ∈ 𝑆 ) → 𝑈 ∈ ( SubGrp ‘ 𝑊 ) )
11 5 7 10 syl2anc ⊢ ( 𝜑 → 𝑈 ∈ ( SubGrp ‘ 𝑊 ) )
12 eqid ⊢ ( +g ‘ 𝑊 ) = ( +g ‘ 𝑊 )
13 12 3 lsmelval ⊢ ( ( 𝑇 ∈ ( SubGrp ‘ 𝑊 ) ∧ 𝑈 ∈ ( SubGrp ‘ 𝑊 ) ) → ( 𝑋 ∈ ( 𝑇 ⊕ 𝑈 ) ↔ ∃ 𝑦 ∈ 𝑇 ∃ 𝑧 ∈ 𝑈 𝑋 = ( 𝑦 ( +g ‘ 𝑊 ) 𝑧 ) ) )
14 9 11 13 syl2anc ⊢ ( 𝜑 → ( 𝑋 ∈ ( 𝑇 ⊕ 𝑈 ) ↔ ∃ 𝑦 ∈ 𝑇 ∃ 𝑧 ∈ 𝑈 𝑋 = ( 𝑦 ( +g ‘ 𝑊 ) 𝑧 ) ) )
15 5 adantr ⊢ ( ( 𝜑 ∧ ( 𝑦 ∈ 𝑇 ∧ 𝑧 ∈ 𝑈 ) ) → 𝑊 ∈ LMod )
16 6 adantr ⊢ ( ( 𝜑 ∧ ( 𝑦 ∈ 𝑇 ∧ 𝑧 ∈ 𝑈 ) ) → 𝑇 ∈ 𝑆 )
17 simprl ⊢ ( ( 𝜑 ∧ ( 𝑦 ∈ 𝑇 ∧ 𝑧 ∈ 𝑈 ) ) → 𝑦 ∈ 𝑇 )
18 1 2 lssel ⊢ ( ( 𝑇 ∈ 𝑆 ∧ 𝑦 ∈ 𝑇 ) → 𝑦 ∈ 𝑉 )
19 16 17 18 syl2anc ⊢ ( ( 𝜑 ∧ ( 𝑦 ∈ 𝑇 ∧ 𝑧 ∈ 𝑈 ) ) → 𝑦 ∈ 𝑉 )
20 1 2 4 lspsncl ⊢ ( ( 𝑊 ∈ LMod ∧ 𝑦 ∈ 𝑉 ) → ( 𝑁 ‘ { 𝑦 } ) ∈ 𝑆 )
21 15 19 20 syl2anc ⊢ ( ( 𝜑 ∧ ( 𝑦 ∈ 𝑇 ∧ 𝑧 ∈ 𝑈 ) ) → ( 𝑁 ‘ { 𝑦 } ) ∈ 𝑆 )
22 2 lsssubg ⊢ ( ( 𝑊 ∈ LMod ∧ ( 𝑁 ‘ { 𝑦 } ) ∈ 𝑆 ) → ( 𝑁 ‘ { 𝑦 } ) ∈ ( SubGrp ‘ 𝑊 ) )
23 15 21 22 syl2anc ⊢ ( ( 𝜑 ∧ ( 𝑦 ∈ 𝑇 ∧ 𝑧 ∈ 𝑈 ) ) → ( 𝑁 ‘ { 𝑦 } ) ∈ ( SubGrp ‘ 𝑊 ) )
24 7 adantr ⊢ ( ( 𝜑 ∧ ( 𝑦 ∈ 𝑇 ∧ 𝑧 ∈ 𝑈 ) ) → 𝑈 ∈ 𝑆 )
25 simprr ⊢ ( ( 𝜑 ∧ ( 𝑦 ∈ 𝑇 ∧ 𝑧 ∈ 𝑈 ) ) → 𝑧 ∈ 𝑈 )
26 1 2 lssel ⊢ ( ( 𝑈 ∈ 𝑆 ∧ 𝑧 ∈ 𝑈 ) → 𝑧 ∈ 𝑉 )
27 24 25 26 syl2anc ⊢ ( ( 𝜑 ∧ ( 𝑦 ∈ 𝑇 ∧ 𝑧 ∈ 𝑈 ) ) → 𝑧 ∈ 𝑉 )
28 1 2 4 lspsncl ⊢ ( ( 𝑊 ∈ LMod ∧ 𝑧 ∈ 𝑉 ) → ( 𝑁 ‘ { 𝑧 } ) ∈ 𝑆 )
29 15 27 28 syl2anc ⊢ ( ( 𝜑 ∧ ( 𝑦 ∈ 𝑇 ∧ 𝑧 ∈ 𝑈 ) ) → ( 𝑁 ‘ { 𝑧 } ) ∈ 𝑆 )
30 2 lsssubg ⊢ ( ( 𝑊 ∈ LMod ∧ ( 𝑁 ‘ { 𝑧 } ) ∈ 𝑆 ) → ( 𝑁 ‘ { 𝑧 } ) ∈ ( SubGrp ‘ 𝑊 ) )
31 15 29 30 syl2anc ⊢ ( ( 𝜑 ∧ ( 𝑦 ∈ 𝑇 ∧ 𝑧 ∈ 𝑈 ) ) → ( 𝑁 ‘ { 𝑧 } ) ∈ ( SubGrp ‘ 𝑊 ) )
32 1 4 lspsnid ⊢ ( ( 𝑊 ∈ LMod ∧ 𝑦 ∈ 𝑉 ) → 𝑦 ∈ ( 𝑁 ‘ { 𝑦 } ) )
33 15 19 32 syl2anc ⊢ ( ( 𝜑 ∧ ( 𝑦 ∈ 𝑇 ∧ 𝑧 ∈ 𝑈 ) ) → 𝑦 ∈ ( 𝑁 ‘ { 𝑦 } ) )
34 1 4 lspsnid ⊢ ( ( 𝑊 ∈ LMod ∧ 𝑧 ∈ 𝑉 ) → 𝑧 ∈ ( 𝑁 ‘ { 𝑧 } ) )
35 15 27 34 syl2anc ⊢ ( ( 𝜑 ∧ ( 𝑦 ∈ 𝑇 ∧ 𝑧 ∈ 𝑈 ) ) → 𝑧 ∈ ( 𝑁 ‘ { 𝑧 } ) )
36 12 3 lsmelvali ⊢ ( ( ( ( 𝑁 ‘ { 𝑦 } ) ∈ ( SubGrp ‘ 𝑊 ) ∧ ( 𝑁 ‘ { 𝑧 } ) ∈ ( SubGrp ‘ 𝑊 ) ) ∧ ( 𝑦 ∈ ( 𝑁 ‘ { 𝑦 } ) ∧ 𝑧 ∈ ( 𝑁 ‘ { 𝑧 } ) ) ) → ( 𝑦 ( +g ‘ 𝑊 ) 𝑧 ) ∈ ( ( 𝑁 ‘ { 𝑦 } ) ⊕ ( 𝑁 ‘ { 𝑧 } ) ) )
37 23 31 33 35 36 syl22anc ⊢ ( ( 𝜑 ∧ ( 𝑦 ∈ 𝑇 ∧ 𝑧 ∈ 𝑈 ) ) → ( 𝑦 ( +g ‘ 𝑊 ) 𝑧 ) ∈ ( ( 𝑁 ‘ { 𝑦 } ) ⊕ ( 𝑁 ‘ { 𝑧 } ) ) )
38 eleq1a ⊢ ( ( 𝑦 ( +g ‘ 𝑊 ) 𝑧 ) ∈ ( ( 𝑁 ‘ { 𝑦 } ) ⊕ ( 𝑁 ‘ { 𝑧 } ) ) → ( 𝑋 = ( 𝑦 ( +g ‘ 𝑊 ) 𝑧 ) → 𝑋 ∈ ( ( 𝑁 ‘ { 𝑦 } ) ⊕ ( 𝑁 ‘ { 𝑧 } ) ) ) )
39 37 38 syl ⊢ ( ( 𝜑 ∧ ( 𝑦 ∈ 𝑇 ∧ 𝑧 ∈ 𝑈 ) ) → ( 𝑋 = ( 𝑦 ( +g ‘ 𝑊 ) 𝑧 ) → 𝑋 ∈ ( ( 𝑁 ‘ { 𝑦 } ) ⊕ ( 𝑁 ‘ { 𝑧 } ) ) ) )
40 2 3 lsmcl ⊢ ( ( 𝑊 ∈ LMod ∧ ( 𝑁 ‘ { 𝑦 } ) ∈ 𝑆 ∧ ( 𝑁 ‘ { 𝑧 } ) ∈ 𝑆 ) → ( ( 𝑁 ‘ { 𝑦 } ) ⊕ ( 𝑁 ‘ { 𝑧 } ) ) ∈ 𝑆 )
41 15 21 29 40 syl3anc ⊢ ( ( 𝜑 ∧ ( 𝑦 ∈ 𝑇 ∧ 𝑧 ∈ 𝑈 ) ) → ( ( 𝑁 ‘ { 𝑦 } ) ⊕ ( 𝑁 ‘ { 𝑧 } ) ) ∈ 𝑆 )
42 1 2 4 15 41 ellspsn6 ⊢ ( ( 𝜑 ∧ ( 𝑦 ∈ 𝑇 ∧ 𝑧 ∈ 𝑈 ) ) → ( 𝑋 ∈ ( ( 𝑁 ‘ { 𝑦 } ) ⊕ ( 𝑁 ‘ { 𝑧 } ) ) ↔ ( 𝑋 ∈ 𝑉 ∧ ( 𝑁 ‘ { 𝑋 } ) ⊆ ( ( 𝑁 ‘ { 𝑦 } ) ⊕ ( 𝑁 ‘ { 𝑧 } ) ) ) ) )
43 39 42 sylibd ⊢ ( ( 𝜑 ∧ ( 𝑦 ∈ 𝑇 ∧ 𝑧 ∈ 𝑈 ) ) → ( 𝑋 = ( 𝑦 ( +g ‘ 𝑊 ) 𝑧 ) → ( 𝑋 ∈ 𝑉 ∧ ( 𝑁 ‘ { 𝑋 } ) ⊆ ( ( 𝑁 ‘ { 𝑦 } ) ⊕ ( 𝑁 ‘ { 𝑧 } ) ) ) ) )
44 43 reximdvva ⊢ ( 𝜑 → ( ∃ 𝑦 ∈ 𝑇 ∃ 𝑧 ∈ 𝑈 𝑋 = ( 𝑦 ( +g ‘ 𝑊 ) 𝑧 ) → ∃ 𝑦 ∈ 𝑇 ∃ 𝑧 ∈ 𝑈 ( 𝑋 ∈ 𝑉 ∧ ( 𝑁 ‘ { 𝑋 } ) ⊆ ( ( 𝑁 ‘ { 𝑦 } ) ⊕ ( 𝑁 ‘ { 𝑧 } ) ) ) ) )
45 14 44 sylbid ⊢ ( 𝜑 → ( 𝑋 ∈ ( 𝑇 ⊕ 𝑈 ) → ∃ 𝑦 ∈ 𝑇 ∃ 𝑧 ∈ 𝑈 ( 𝑋 ∈ 𝑉 ∧ ( 𝑁 ‘ { 𝑋 } ) ⊆ ( ( 𝑁 ‘ { 𝑦 } ) ⊕ ( 𝑁 ‘ { 𝑧 } ) ) ) ) )
46 9 adantr ⊢ ( ( 𝜑 ∧ ( 𝑦 ∈ 𝑇 ∧ 𝑧 ∈ 𝑈 ) ) → 𝑇 ∈ ( SubGrp ‘ 𝑊 ) )
47 2 4 15 16 17 ellspsn5 ⊢ ( ( 𝜑 ∧ ( 𝑦 ∈ 𝑇 ∧ 𝑧 ∈ 𝑈 ) ) → ( 𝑁 ‘ { 𝑦 } ) ⊆ 𝑇 )
48 3 lsmless1 ⊢ ( ( 𝑇 ∈ ( SubGrp ‘ 𝑊 ) ∧ ( 𝑁 ‘ { 𝑧 } ) ∈ ( SubGrp ‘ 𝑊 ) ∧ ( 𝑁 ‘ { 𝑦 } ) ⊆ 𝑇 ) → ( ( 𝑁 ‘ { 𝑦 } ) ⊕ ( 𝑁 ‘ { 𝑧 } ) ) ⊆ ( 𝑇 ⊕ ( 𝑁 ‘ { 𝑧 } ) ) )
49 46 31 47 48 syl3anc ⊢ ( ( 𝜑 ∧ ( 𝑦 ∈ 𝑇 ∧ 𝑧 ∈ 𝑈 ) ) → ( ( 𝑁 ‘ { 𝑦 } ) ⊕ ( 𝑁 ‘ { 𝑧 } ) ) ⊆ ( 𝑇 ⊕ ( 𝑁 ‘ { 𝑧 } ) ) )
50 11 adantr ⊢ ( ( 𝜑 ∧ ( 𝑦 ∈ 𝑇 ∧ 𝑧 ∈ 𝑈 ) ) → 𝑈 ∈ ( SubGrp ‘ 𝑊 ) )
51 2 4 15 24 25 ellspsn5 ⊢ ( ( 𝜑 ∧ ( 𝑦 ∈ 𝑇 ∧ 𝑧 ∈ 𝑈 ) ) → ( 𝑁 ‘ { 𝑧 } ) ⊆ 𝑈 )
52 3 lsmless2 ⊢ ( ( 𝑇 ∈ ( SubGrp ‘ 𝑊 ) ∧ 𝑈 ∈ ( SubGrp ‘ 𝑊 ) ∧ ( 𝑁 ‘ { 𝑧 } ) ⊆ 𝑈 ) → ( 𝑇 ⊕ ( 𝑁 ‘ { 𝑧 } ) ) ⊆ ( 𝑇 ⊕ 𝑈 ) )
53 46 50 51 52 syl3anc ⊢ ( ( 𝜑 ∧ ( 𝑦 ∈ 𝑇 ∧ 𝑧 ∈ 𝑈 ) ) → ( 𝑇 ⊕ ( 𝑁 ‘ { 𝑧 } ) ) ⊆ ( 𝑇 ⊕ 𝑈 ) )
54 49 53 sstrd ⊢ ( ( 𝜑 ∧ ( 𝑦 ∈ 𝑇 ∧ 𝑧 ∈ 𝑈 ) ) → ( ( 𝑁 ‘ { 𝑦 } ) ⊕ ( 𝑁 ‘ { 𝑧 } ) ) ⊆ ( 𝑇 ⊕ 𝑈 ) )
55 54 sseld ⊢ ( ( 𝜑 ∧ ( 𝑦 ∈ 𝑇 ∧ 𝑧 ∈ 𝑈 ) ) → ( 𝑋 ∈ ( ( 𝑁 ‘ { 𝑦 } ) ⊕ ( 𝑁 ‘ { 𝑧 } ) ) → 𝑋 ∈ ( 𝑇 ⊕ 𝑈 ) ) )
56 42 55 sylbird ⊢ ( ( 𝜑 ∧ ( 𝑦 ∈ 𝑇 ∧ 𝑧 ∈ 𝑈 ) ) → ( ( 𝑋 ∈ 𝑉 ∧ ( 𝑁 ‘ { 𝑋 } ) ⊆ ( ( 𝑁 ‘ { 𝑦 } ) ⊕ ( 𝑁 ‘ { 𝑧 } ) ) ) → 𝑋 ∈ ( 𝑇 ⊕ 𝑈 ) ) )
57 56 rexlimdvva ⊢ ( 𝜑 → ( ∃ 𝑦 ∈ 𝑇 ∃ 𝑧 ∈ 𝑈 ( 𝑋 ∈ 𝑉 ∧ ( 𝑁 ‘ { 𝑋 } ) ⊆ ( ( 𝑁 ‘ { 𝑦 } ) ⊕ ( 𝑁 ‘ { 𝑧 } ) ) ) → 𝑋 ∈ ( 𝑇 ⊕ 𝑈 ) ) )
58 45 57 impbid ⊢ ( 𝜑 → ( 𝑋 ∈ ( 𝑇 ⊕ 𝑈 ) ↔ ∃ 𝑦 ∈ 𝑇 ∃ 𝑧 ∈ 𝑈 ( 𝑋 ∈ 𝑉 ∧ ( 𝑁 ‘ { 𝑋 } ) ⊆ ( ( 𝑁 ‘ { 𝑦 } ) ⊕ ( 𝑁 ‘ { 𝑧 } ) ) ) ) )
59 r19.42v ⊢ ( ∃ 𝑧 ∈ 𝑈 ( 𝑋 ∈ 𝑉 ∧ ( 𝑁 ‘ { 𝑋 } ) ⊆ ( ( 𝑁 ‘ { 𝑦 } ) ⊕ ( 𝑁 ‘ { 𝑧 } ) ) ) ↔ ( 𝑋 ∈ 𝑉 ∧ ∃ 𝑧 ∈ 𝑈 ( 𝑁 ‘ { 𝑋 } ) ⊆ ( ( 𝑁 ‘ { 𝑦 } ) ⊕ ( 𝑁 ‘ { 𝑧 } ) ) ) )
60 59 rexbii ⊢ ( ∃ 𝑦 ∈ 𝑇 ∃ 𝑧 ∈ 𝑈 ( 𝑋 ∈ 𝑉 ∧ ( 𝑁 ‘ { 𝑋 } ) ⊆ ( ( 𝑁 ‘ { 𝑦 } ) ⊕ ( 𝑁 ‘ { 𝑧 } ) ) ) ↔ ∃ 𝑦 ∈ 𝑇 ( 𝑋 ∈ 𝑉 ∧ ∃ 𝑧 ∈ 𝑈 ( 𝑁 ‘ { 𝑋 } ) ⊆ ( ( 𝑁 ‘ { 𝑦 } ) ⊕ ( 𝑁 ‘ { 𝑧 } ) ) ) )
61 r19.42v ⊢ ( ∃ 𝑦 ∈ 𝑇 ( 𝑋 ∈ 𝑉 ∧ ∃ 𝑧 ∈ 𝑈 ( 𝑁 ‘ { 𝑋 } ) ⊆ ( ( 𝑁 ‘ { 𝑦 } ) ⊕ ( 𝑁 ‘ { 𝑧 } ) ) ) ↔ ( 𝑋 ∈ 𝑉 ∧ ∃ 𝑦 ∈ 𝑇 ∃ 𝑧 ∈ 𝑈 ( 𝑁 ‘ { 𝑋 } ) ⊆ ( ( 𝑁 ‘ { 𝑦 } ) ⊕ ( 𝑁 ‘ { 𝑧 } ) ) ) )
62 60 61 bitri ⊢ ( ∃ 𝑦 ∈ 𝑇 ∃ 𝑧 ∈ 𝑈 ( 𝑋 ∈ 𝑉 ∧ ( 𝑁 ‘ { 𝑋 } ) ⊆ ( ( 𝑁 ‘ { 𝑦 } ) ⊕ ( 𝑁 ‘ { 𝑧 } ) ) ) ↔ ( 𝑋 ∈ 𝑉 ∧ ∃ 𝑦 ∈ 𝑇 ∃ 𝑧 ∈ 𝑈 ( 𝑁 ‘ { 𝑋 } ) ⊆ ( ( 𝑁 ‘ { 𝑦 } ) ⊕ ( 𝑁 ‘ { 𝑧 } ) ) ) )
63 58 62 bitrdi ⊢ ( 𝜑 → ( 𝑋 ∈ ( 𝑇 ⊕ 𝑈 ) ↔ ( 𝑋 ∈ 𝑉 ∧ ∃ 𝑦 ∈ 𝑇 ∃ 𝑧 ∈ 𝑈 ( 𝑁 ‘ { 𝑋 } ) ⊆ ( ( 𝑁 ‘ { 𝑦 } ) ⊕ ( 𝑁 ‘ { 𝑧 } ) ) ) ) )