This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem lsmspsn

Description: Member of subspace sum of spans of singletons. (Contributed by NM, 8-Apr-2015)

Ref Expression
Hypotheses lsmspsn.v ⊢ 𝑉 = ( Base ‘ 𝑊 )
lsmspsn.a ⊢ + = ( +g ‘ 𝑊 )
lsmspsn.f ⊢ 𝐹 = ( Scalar ‘ 𝑊 )
lsmspsn.k ⊢ 𝐾 = ( Base ‘ 𝐹 )
lsmspsn.t ⊢ · = ( ·𝑠 ‘ 𝑊 )
lsmspsn.p ⊢ ⊕ = ( LSSum ‘ 𝑊 )
lsmspsn.n ⊢ 𝑁 = ( LSpan ‘ 𝑊 )
lsmspsn.w ⊢ ( 𝜑 → 𝑊 ∈ LMod )
lsmspsn.x ⊢ ( 𝜑 → 𝑋 ∈ 𝑉 )
lsmspsn.y ⊢ ( 𝜑 → 𝑌 ∈ 𝑉 )
Assertion lsmspsn ( 𝜑 → ( 𝑈 ∈ ( ( 𝑁 ‘ { 𝑋 } ) ⊕ ( 𝑁 ‘ { 𝑌 } ) ) ↔ ∃ 𝑗 ∈ 𝐾 ∃ 𝑘 ∈ 𝐾 𝑈 = ( ( 𝑗 · 𝑋 ) + ( 𝑘 · 𝑌 ) ) ) )

Proof

Step Hyp Ref Expression
1 lsmspsn.v ⊢ 𝑉 = ( Base ‘ 𝑊 )
2 lsmspsn.a ⊢ + = ( +g ‘ 𝑊 )
3 lsmspsn.f ⊢ 𝐹 = ( Scalar ‘ 𝑊 )
4 lsmspsn.k ⊢ 𝐾 = ( Base ‘ 𝐹 )
5 lsmspsn.t ⊢ · = ( ·𝑠 ‘ 𝑊 )
6 lsmspsn.p ⊢ ⊕ = ( LSSum ‘ 𝑊 )
7 lsmspsn.n ⊢ 𝑁 = ( LSpan ‘ 𝑊 )
8 lsmspsn.w ⊢ ( 𝜑 → 𝑊 ∈ LMod )
9 lsmspsn.x ⊢ ( 𝜑 → 𝑋 ∈ 𝑉 )
10 lsmspsn.y ⊢ ( 𝜑 → 𝑌 ∈ 𝑉 )
11 1 7 lspsnsubg ⊢ ( ( 𝑊 ∈ LMod ∧ 𝑋 ∈ 𝑉 ) → ( 𝑁 ‘ { 𝑋 } ) ∈ ( SubGrp ‘ 𝑊 ) )
12 8 9 11 syl2anc ⊢ ( 𝜑 → ( 𝑁 ‘ { 𝑋 } ) ∈ ( SubGrp ‘ 𝑊 ) )
13 1 7 lspsnsubg ⊢ ( ( 𝑊 ∈ LMod ∧ 𝑌 ∈ 𝑉 ) → ( 𝑁 ‘ { 𝑌 } ) ∈ ( SubGrp ‘ 𝑊 ) )
14 8 10 13 syl2anc ⊢ ( 𝜑 → ( 𝑁 ‘ { 𝑌 } ) ∈ ( SubGrp ‘ 𝑊 ) )
15 2 6 lsmelval ⊢ ( ( ( 𝑁 ‘ { 𝑋 } ) ∈ ( SubGrp ‘ 𝑊 ) ∧ ( 𝑁 ‘ { 𝑌 } ) ∈ ( SubGrp ‘ 𝑊 ) ) → ( 𝑈 ∈ ( ( 𝑁 ‘ { 𝑋 } ) ⊕ ( 𝑁 ‘ { 𝑌 } ) ) ↔ ∃ 𝑣 ∈ ( 𝑁 ‘ { 𝑋 } ) ∃ 𝑤 ∈ ( 𝑁 ‘ { 𝑌 } ) 𝑈 = ( 𝑣 + 𝑤 ) ) )
16 12 14 15 syl2anc ⊢ ( 𝜑 → ( 𝑈 ∈ ( ( 𝑁 ‘ { 𝑋 } ) ⊕ ( 𝑁 ‘ { 𝑌 } ) ) ↔ ∃ 𝑣 ∈ ( 𝑁 ‘ { 𝑋 } ) ∃ 𝑤 ∈ ( 𝑁 ‘ { 𝑌 } ) 𝑈 = ( 𝑣 + 𝑤 ) ) )
17 3 4 1 5 7 ellspsn ⊢ ( ( 𝑊 ∈ LMod ∧ 𝑋 ∈ 𝑉 ) → ( 𝑣 ∈ ( 𝑁 ‘ { 𝑋 } ) ↔ ∃ 𝑗 ∈ 𝐾 𝑣 = ( 𝑗 · 𝑋 ) ) )
18 8 9 17 syl2anc ⊢ ( 𝜑 → ( 𝑣 ∈ ( 𝑁 ‘ { 𝑋 } ) ↔ ∃ 𝑗 ∈ 𝐾 𝑣 = ( 𝑗 · 𝑋 ) ) )
19 3 4 1 5 7 ellspsn ⊢ ( ( 𝑊 ∈ LMod ∧ 𝑌 ∈ 𝑉 ) → ( 𝑤 ∈ ( 𝑁 ‘ { 𝑌 } ) ↔ ∃ 𝑘 ∈ 𝐾 𝑤 = ( 𝑘 · 𝑌 ) ) )
20 8 10 19 syl2anc ⊢ ( 𝜑 → ( 𝑤 ∈ ( 𝑁 ‘ { 𝑌 } ) ↔ ∃ 𝑘 ∈ 𝐾 𝑤 = ( 𝑘 · 𝑌 ) ) )
21 18 20 anbi12d ⊢ ( 𝜑 → ( ( 𝑣 ∈ ( 𝑁 ‘ { 𝑋 } ) ∧ 𝑤 ∈ ( 𝑁 ‘ { 𝑌 } ) ) ↔ ( ∃ 𝑗 ∈ 𝐾 𝑣 = ( 𝑗 · 𝑋 ) ∧ ∃ 𝑘 ∈ 𝐾 𝑤 = ( 𝑘 · 𝑌 ) ) ) )
22 21 biimpa ⊢ ( ( 𝜑 ∧ ( 𝑣 ∈ ( 𝑁 ‘ { 𝑋 } ) ∧ 𝑤 ∈ ( 𝑁 ‘ { 𝑌 } ) ) ) → ( ∃ 𝑗 ∈ 𝐾 𝑣 = ( 𝑗 · 𝑋 ) ∧ ∃ 𝑘 ∈ 𝐾 𝑤 = ( 𝑘 · 𝑌 ) ) )
23 22 biantrurd ⊢ ( ( 𝜑 ∧ ( 𝑣 ∈ ( 𝑁 ‘ { 𝑋 } ) ∧ 𝑤 ∈ ( 𝑁 ‘ { 𝑌 } ) ) ) → ( 𝑈 = ( 𝑣 + 𝑤 ) ↔ ( ( ∃ 𝑗 ∈ 𝐾 𝑣 = ( 𝑗 · 𝑋 ) ∧ ∃ 𝑘 ∈ 𝐾 𝑤 = ( 𝑘 · 𝑌 ) ) ∧ 𝑈 = ( 𝑣 + 𝑤 ) ) ) )
24 r19.41v ⊢ ( ∃ 𝑘 ∈ 𝐾 ( ( 𝑣 = ( 𝑗 · 𝑋 ) ∧ 𝑤 = ( 𝑘 · 𝑌 ) ) ∧ 𝑈 = ( 𝑣 + 𝑤 ) ) ↔ ( ∃ 𝑘 ∈ 𝐾 ( 𝑣 = ( 𝑗 · 𝑋 ) ∧ 𝑤 = ( 𝑘 · 𝑌 ) ) ∧ 𝑈 = ( 𝑣 + 𝑤 ) ) )
25 24 rexbii ⊢ ( ∃ 𝑗 ∈ 𝐾 ∃ 𝑘 ∈ 𝐾 ( ( 𝑣 = ( 𝑗 · 𝑋 ) ∧ 𝑤 = ( 𝑘 · 𝑌 ) ) ∧ 𝑈 = ( 𝑣 + 𝑤 ) ) ↔ ∃ 𝑗 ∈ 𝐾 ( ∃ 𝑘 ∈ 𝐾 ( 𝑣 = ( 𝑗 · 𝑋 ) ∧ 𝑤 = ( 𝑘 · 𝑌 ) ) ∧ 𝑈 = ( 𝑣 + 𝑤 ) ) )
26 r19.41v ⊢ ( ∃ 𝑗 ∈ 𝐾 ( ∃ 𝑘 ∈ 𝐾 ( 𝑣 = ( 𝑗 · 𝑋 ) ∧ 𝑤 = ( 𝑘 · 𝑌 ) ) ∧ 𝑈 = ( 𝑣 + 𝑤 ) ) ↔ ( ∃ 𝑗 ∈ 𝐾 ∃ 𝑘 ∈ 𝐾 ( 𝑣 = ( 𝑗 · 𝑋 ) ∧ 𝑤 = ( 𝑘 · 𝑌 ) ) ∧ 𝑈 = ( 𝑣 + 𝑤 ) ) )
27 reeanv ⊢ ( ∃ 𝑗 ∈ 𝐾 ∃ 𝑘 ∈ 𝐾 ( 𝑣 = ( 𝑗 · 𝑋 ) ∧ 𝑤 = ( 𝑘 · 𝑌 ) ) ↔ ( ∃ 𝑗 ∈ 𝐾 𝑣 = ( 𝑗 · 𝑋 ) ∧ ∃ 𝑘 ∈ 𝐾 𝑤 = ( 𝑘 · 𝑌 ) ) )
28 27 anbi1i ⊢ ( ( ∃ 𝑗 ∈ 𝐾 ∃ 𝑘 ∈ 𝐾 ( 𝑣 = ( 𝑗 · 𝑋 ) ∧ 𝑤 = ( 𝑘 · 𝑌 ) ) ∧ 𝑈 = ( 𝑣 + 𝑤 ) ) ↔ ( ( ∃ 𝑗 ∈ 𝐾 𝑣 = ( 𝑗 · 𝑋 ) ∧ ∃ 𝑘 ∈ 𝐾 𝑤 = ( 𝑘 · 𝑌 ) ) ∧ 𝑈 = ( 𝑣 + 𝑤 ) ) )
29 25 26 28 3bitrri ⊢ ( ( ( ∃ 𝑗 ∈ 𝐾 𝑣 = ( 𝑗 · 𝑋 ) ∧ ∃ 𝑘 ∈ 𝐾 𝑤 = ( 𝑘 · 𝑌 ) ) ∧ 𝑈 = ( 𝑣 + 𝑤 ) ) ↔ ∃ 𝑗 ∈ 𝐾 ∃ 𝑘 ∈ 𝐾 ( ( 𝑣 = ( 𝑗 · 𝑋 ) ∧ 𝑤 = ( 𝑘 · 𝑌 ) ) ∧ 𝑈 = ( 𝑣 + 𝑤 ) ) )
30 23 29 bitrdi ⊢ ( ( 𝜑 ∧ ( 𝑣 ∈ ( 𝑁 ‘ { 𝑋 } ) ∧ 𝑤 ∈ ( 𝑁 ‘ { 𝑌 } ) ) ) → ( 𝑈 = ( 𝑣 + 𝑤 ) ↔ ∃ 𝑗 ∈ 𝐾 ∃ 𝑘 ∈ 𝐾 ( ( 𝑣 = ( 𝑗 · 𝑋 ) ∧ 𝑤 = ( 𝑘 · 𝑌 ) ) ∧ 𝑈 = ( 𝑣 + 𝑤 ) ) ) )
31 30 2rexbidva ⊢ ( 𝜑 → ( ∃ 𝑣 ∈ ( 𝑁 ‘ { 𝑋 } ) ∃ 𝑤 ∈ ( 𝑁 ‘ { 𝑌 } ) 𝑈 = ( 𝑣 + 𝑤 ) ↔ ∃ 𝑣 ∈ ( 𝑁 ‘ { 𝑋 } ) ∃ 𝑤 ∈ ( 𝑁 ‘ { 𝑌 } ) ∃ 𝑗 ∈ 𝐾 ∃ 𝑘 ∈ 𝐾 ( ( 𝑣 = ( 𝑗 · 𝑋 ) ∧ 𝑤 = ( 𝑘 · 𝑌 ) ) ∧ 𝑈 = ( 𝑣 + 𝑤 ) ) ) )
32 rexrot4 ⊢ ( ∃ 𝑣 ∈ ( 𝑁 ‘ { 𝑋 } ) ∃ 𝑤 ∈ ( 𝑁 ‘ { 𝑌 } ) ∃ 𝑗 ∈ 𝐾 ∃ 𝑘 ∈ 𝐾 ( ( 𝑣 = ( 𝑗 · 𝑋 ) ∧ 𝑤 = ( 𝑘 · 𝑌 ) ) ∧ 𝑈 = ( 𝑣 + 𝑤 ) ) ↔ ∃ 𝑗 ∈ 𝐾 ∃ 𝑘 ∈ 𝐾 ∃ 𝑣 ∈ ( 𝑁 ‘ { 𝑋 } ) ∃ 𝑤 ∈ ( 𝑁 ‘ { 𝑌 } ) ( ( 𝑣 = ( 𝑗 · 𝑋 ) ∧ 𝑤 = ( 𝑘 · 𝑌 ) ) ∧ 𝑈 = ( 𝑣 + 𝑤 ) ) )
33 31 32 bitrdi ⊢ ( 𝜑 → ( ∃ 𝑣 ∈ ( 𝑁 ‘ { 𝑋 } ) ∃ 𝑤 ∈ ( 𝑁 ‘ { 𝑌 } ) 𝑈 = ( 𝑣 + 𝑤 ) ↔ ∃ 𝑗 ∈ 𝐾 ∃ 𝑘 ∈ 𝐾 ∃ 𝑣 ∈ ( 𝑁 ‘ { 𝑋 } ) ∃ 𝑤 ∈ ( 𝑁 ‘ { 𝑌 } ) ( ( 𝑣 = ( 𝑗 · 𝑋 ) ∧ 𝑤 = ( 𝑘 · 𝑌 ) ) ∧ 𝑈 = ( 𝑣 + 𝑤 ) ) ) )
34 8 adantr ⊢ ( ( 𝜑 ∧ ( 𝑗 ∈ 𝐾 ∧ 𝑘 ∈ 𝐾 ) ) → 𝑊 ∈ LMod )
35 simprl ⊢ ( ( 𝜑 ∧ ( 𝑗 ∈ 𝐾 ∧ 𝑘 ∈ 𝐾 ) ) → 𝑗 ∈ 𝐾 )
36 9 adantr ⊢ ( ( 𝜑 ∧ ( 𝑗 ∈ 𝐾 ∧ 𝑘 ∈ 𝐾 ) ) → 𝑋 ∈ 𝑉 )
37 1 5 3 4 7 34 35 36 ellspsni ⊢ ( ( 𝜑 ∧ ( 𝑗 ∈ 𝐾 ∧ 𝑘 ∈ 𝐾 ) ) → ( 𝑗 · 𝑋 ) ∈ ( 𝑁 ‘ { 𝑋 } ) )
38 simprr ⊢ ( ( 𝜑 ∧ ( 𝑗 ∈ 𝐾 ∧ 𝑘 ∈ 𝐾 ) ) → 𝑘 ∈ 𝐾 )
39 10 adantr ⊢ ( ( 𝜑 ∧ ( 𝑗 ∈ 𝐾 ∧ 𝑘 ∈ 𝐾 ) ) → 𝑌 ∈ 𝑉 )
40 1 5 3 4 7 34 38 39 ellspsni ⊢ ( ( 𝜑 ∧ ( 𝑗 ∈ 𝐾 ∧ 𝑘 ∈ 𝐾 ) ) → ( 𝑘 · 𝑌 ) ∈ ( 𝑁 ‘ { 𝑌 } ) )
41 oveq1 ⊢ ( 𝑣 = ( 𝑗 · 𝑋 ) → ( 𝑣 + 𝑤 ) = ( ( 𝑗 · 𝑋 ) + 𝑤 ) )
42 41 eqeq2d ⊢ ( 𝑣 = ( 𝑗 · 𝑋 ) → ( 𝑈 = ( 𝑣 + 𝑤 ) ↔ 𝑈 = ( ( 𝑗 · 𝑋 ) + 𝑤 ) ) )
43 oveq2 ⊢ ( 𝑤 = ( 𝑘 · 𝑌 ) → ( ( 𝑗 · 𝑋 ) + 𝑤 ) = ( ( 𝑗 · 𝑋 ) + ( 𝑘 · 𝑌 ) ) )
44 43 eqeq2d ⊢ ( 𝑤 = ( 𝑘 · 𝑌 ) → ( 𝑈 = ( ( 𝑗 · 𝑋 ) + 𝑤 ) ↔ 𝑈 = ( ( 𝑗 · 𝑋 ) + ( 𝑘 · 𝑌 ) ) ) )
45 42 44 ceqsrex2v ⊢ ( ( ( 𝑗 · 𝑋 ) ∈ ( 𝑁 ‘ { 𝑋 } ) ∧ ( 𝑘 · 𝑌 ) ∈ ( 𝑁 ‘ { 𝑌 } ) ) → ( ∃ 𝑣 ∈ ( 𝑁 ‘ { 𝑋 } ) ∃ 𝑤 ∈ ( 𝑁 ‘ { 𝑌 } ) ( ( 𝑣 = ( 𝑗 · 𝑋 ) ∧ 𝑤 = ( 𝑘 · 𝑌 ) ) ∧ 𝑈 = ( 𝑣 + 𝑤 ) ) ↔ 𝑈 = ( ( 𝑗 · 𝑋 ) + ( 𝑘 · 𝑌 ) ) ) )
46 37 40 45 syl2anc ⊢ ( ( 𝜑 ∧ ( 𝑗 ∈ 𝐾 ∧ 𝑘 ∈ 𝐾 ) ) → ( ∃ 𝑣 ∈ ( 𝑁 ‘ { 𝑋 } ) ∃ 𝑤 ∈ ( 𝑁 ‘ { 𝑌 } ) ( ( 𝑣 = ( 𝑗 · 𝑋 ) ∧ 𝑤 = ( 𝑘 · 𝑌 ) ) ∧ 𝑈 = ( 𝑣 + 𝑤 ) ) ↔ 𝑈 = ( ( 𝑗 · 𝑋 ) + ( 𝑘 · 𝑌 ) ) ) )
47 46 2rexbidva ⊢ ( 𝜑 → ( ∃ 𝑗 ∈ 𝐾 ∃ 𝑘 ∈ 𝐾 ∃ 𝑣 ∈ ( 𝑁 ‘ { 𝑋 } ) ∃ 𝑤 ∈ ( 𝑁 ‘ { 𝑌 } ) ( ( 𝑣 = ( 𝑗 · 𝑋 ) ∧ 𝑤 = ( 𝑘 · 𝑌 ) ) ∧ 𝑈 = ( 𝑣 + 𝑤 ) ) ↔ ∃ 𝑗 ∈ 𝐾 ∃ 𝑘 ∈ 𝐾 𝑈 = ( ( 𝑗 · 𝑋 ) + ( 𝑘 · 𝑌 ) ) ) )
48 16 33 47 3bitrd ⊢ ( 𝜑 → ( 𝑈 ∈ ( ( 𝑁 ‘ { 𝑋 } ) ⊕ ( 𝑁 ‘ { 𝑌 } ) ) ↔ ∃ 𝑗 ∈ 𝐾 ∃ 𝑘 ∈ 𝐾 𝑈 = ( ( 𝑗 · 𝑋 ) + ( 𝑘 · 𝑌 ) ) ) )