Metamath Proof Explorer

Theorem hdmapglem7a

Description: Lemma for hdmapg . (Contributed by NM, 14-Jun-2015)

Ref Expression
Hypotheses hdmapglem7.h ⊢ 𝐻 = ( LHyp ‘ 𝐾 )
hdmapglem7.e ⊢ 𝐸 = ⟨ ( I ↾ ( Base ‘ 𝐾 ) ) , ( I ↾ ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 ) ) ⟩
hdmapglem7.o ⊢ 𝑂 = ( ( ocH ‘ 𝐾 ) ‘ 𝑊 )
hdmapglem7.u ⊢ 𝑈 = ( ( DVecH ‘ 𝐾 ) ‘ 𝑊 )
hdmapglem7.v ⊢ 𝑉 = ( Base ‘ 𝑈 )
hdmapglem7.p ⊢ + = ( +g ‘ 𝑈 )
hdmapglem7.q ⊢ · = ( ·𝑠 ‘ 𝑈 )
hdmapglem7.r ⊢ 𝑅 = ( Scalar ‘ 𝑈 )
hdmapglem7.b ⊢ 𝐵 = ( Base ‘ 𝑅 )
hdmapglem7.a ⊢ ⊕ = ( LSSum ‘ 𝑈 )
hdmapglem7.n ⊢ 𝑁 = ( LSpan ‘ 𝑈 )
hdmapglem7.k ⊢ ( 𝜑 → ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) )
hdmapglem7.x ⊢ ( 𝜑 → 𝑋 ∈ 𝑉 )
Assertion hdmapglem7a ( 𝜑 → ∃ 𝑢 ∈ ( 𝑂 ‘ { 𝐸 } ) ∃ 𝑘 ∈ 𝐵 𝑋 = ( ( 𝑘 · 𝐸 ) + 𝑢 ) )

Proof

Step Hyp Ref Expression
1 hdmapglem7.h ⊢ 𝐻 = ( LHyp ‘ 𝐾 )
2 hdmapglem7.e ⊢ 𝐸 = ⟨ ( I ↾ ( Base ‘ 𝐾 ) ) , ( I ↾ ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 ) ) ⟩
3 hdmapglem7.o ⊢ 𝑂 = ( ( ocH ‘ 𝐾 ) ‘ 𝑊 )
4 hdmapglem7.u ⊢ 𝑈 = ( ( DVecH ‘ 𝐾 ) ‘ 𝑊 )
5 hdmapglem7.v ⊢ 𝑉 = ( Base ‘ 𝑈 )
6 hdmapglem7.p ⊢ + = ( +g ‘ 𝑈 )
7 hdmapglem7.q ⊢ · = ( ·𝑠 ‘ 𝑈 )
8 hdmapglem7.r ⊢ 𝑅 = ( Scalar ‘ 𝑈 )
9 hdmapglem7.b ⊢ 𝐵 = ( Base ‘ 𝑅 )
10 hdmapglem7.a ⊢ ⊕ = ( LSSum ‘ 𝑈 )
11 hdmapglem7.n ⊢ 𝑁 = ( LSpan ‘ 𝑈 )
12 hdmapglem7.k ⊢ ( 𝜑 → ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) )
13 hdmapglem7.x ⊢ ( 𝜑 → 𝑋 ∈ 𝑉 )
14 eqid ⊢ ( LSubSp ‘ 𝑈 ) = ( LSubSp ‘ 𝑈 )
15 1 4 12 dvhlmod ⊢ ( 𝜑 → 𝑈 ∈ LMod )
16 eqid ⊢ ( Base ‘ 𝐾 ) = ( Base ‘ 𝐾 )
17 eqid ⊢ ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 ) = ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 )
18 eqid ⊢ ( 0g ‘ 𝑈 ) = ( 0g ‘ 𝑈 )
19 1 16 17 4 5 18 2 12 dvheveccl ⊢ ( 𝜑 → 𝐸 ∈ ( 𝑉 ∖ { ( 0g ‘ 𝑈 ) } ) )
20 19 eldifad ⊢ ( 𝜑 → 𝐸 ∈ 𝑉 )
21 5 14 11 lspsncl ⊢ ( ( 𝑈 ∈ LMod ∧ 𝐸 ∈ 𝑉 ) → ( 𝑁 ‘ { 𝐸 } ) ∈ ( LSubSp ‘ 𝑈 ) )
22 15 20 21 syl2anc ⊢ ( 𝜑 → ( 𝑁 ‘ { 𝐸 } ) ∈ ( LSubSp ‘ 𝑈 ) )
23 20 snssd ⊢ ( 𝜑 → { 𝐸 } ⊆ 𝑉 )
24 1 4 3 5 11 12 23 dochocsp ⊢ ( 𝜑 → ( 𝑂 ‘ ( 𝑁 ‘ { 𝐸 } ) ) = ( 𝑂 ‘ { 𝐸 } ) )
25 24 fveq2d ⊢ ( 𝜑 → ( 𝑂 ‘ ( 𝑂 ‘ ( 𝑁 ‘ { 𝐸 } ) ) ) = ( 𝑂 ‘ ( 𝑂 ‘ { 𝐸 } ) ) )
26 1 4 3 5 11 12 20 dochocsn ⊢ ( 𝜑 → ( 𝑂 ‘ ( 𝑂 ‘ { 𝐸 } ) ) = ( 𝑁 ‘ { 𝐸 } ) )
27 25 26 eqtrd ⊢ ( 𝜑 → ( 𝑂 ‘ ( 𝑂 ‘ ( 𝑁 ‘ { 𝐸 } ) ) ) = ( 𝑁 ‘ { 𝐸 } ) )
28 1 3 4 5 14 10 12 22 27 dochexmid ⊢ ( 𝜑 → ( ( 𝑁 ‘ { 𝐸 } ) ⊕ ( 𝑂 ‘ ( 𝑁 ‘ { 𝐸 } ) ) ) = 𝑉 )
29 24 oveq2d ⊢ ( 𝜑 → ( ( 𝑁 ‘ { 𝐸 } ) ⊕ ( 𝑂 ‘ ( 𝑁 ‘ { 𝐸 } ) ) ) = ( ( 𝑁 ‘ { 𝐸 } ) ⊕ ( 𝑂 ‘ { 𝐸 } ) ) )
30 28 29 eqtr3d ⊢ ( 𝜑 → 𝑉 = ( ( 𝑁 ‘ { 𝐸 } ) ⊕ ( 𝑂 ‘ { 𝐸 } ) ) )
31 13 30 eleqtrd ⊢ ( 𝜑 → 𝑋 ∈ ( ( 𝑁 ‘ { 𝐸 } ) ⊕ ( 𝑂 ‘ { 𝐸 } ) ) )
32 14 lsssssubg ⊢ ( 𝑈 ∈ LMod → ( LSubSp ‘ 𝑈 ) ⊆ ( SubGrp ‘ 𝑈 ) )
33 15 32 syl ⊢ ( 𝜑 → ( LSubSp ‘ 𝑈 ) ⊆ ( SubGrp ‘ 𝑈 ) )
34 33 22 sseldd ⊢ ( 𝜑 → ( 𝑁 ‘ { 𝐸 } ) ∈ ( SubGrp ‘ 𝑈 ) )
35 1 4 5 14 3 dochlss ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ { 𝐸 } ⊆ 𝑉 ) → ( 𝑂 ‘ { 𝐸 } ) ∈ ( LSubSp ‘ 𝑈 ) )
36 12 23 35 syl2anc ⊢ ( 𝜑 → ( 𝑂 ‘ { 𝐸 } ) ∈ ( LSubSp ‘ 𝑈 ) )
37 33 36 sseldd ⊢ ( 𝜑 → ( 𝑂 ‘ { 𝐸 } ) ∈ ( SubGrp ‘ 𝑈 ) )
38 6 10 lsmelval ⊢ ( ( ( 𝑁 ‘ { 𝐸 } ) ∈ ( SubGrp ‘ 𝑈 ) ∧ ( 𝑂 ‘ { 𝐸 } ) ∈ ( SubGrp ‘ 𝑈 ) ) → ( 𝑋 ∈ ( ( 𝑁 ‘ { 𝐸 } ) ⊕ ( 𝑂 ‘ { 𝐸 } ) ) ↔ ∃ 𝑎 ∈ ( 𝑁 ‘ { 𝐸 } ) ∃ 𝑢 ∈ ( 𝑂 ‘ { 𝐸 } ) 𝑋 = ( 𝑎 + 𝑢 ) ) )
39 34 37 38 syl2anc ⊢ ( 𝜑 → ( 𝑋 ∈ ( ( 𝑁 ‘ { 𝐸 } ) ⊕ ( 𝑂 ‘ { 𝐸 } ) ) ↔ ∃ 𝑎 ∈ ( 𝑁 ‘ { 𝐸 } ) ∃ 𝑢 ∈ ( 𝑂 ‘ { 𝐸 } ) 𝑋 = ( 𝑎 + 𝑢 ) ) )
40 31 39 mpbid ⊢ ( 𝜑 → ∃ 𝑎 ∈ ( 𝑁 ‘ { 𝐸 } ) ∃ 𝑢 ∈ ( 𝑂 ‘ { 𝐸 } ) 𝑋 = ( 𝑎 + 𝑢 ) )
41 rexcom ⊢ ( ∃ 𝑎 ∈ ( 𝑁 ‘ { 𝐸 } ) ∃ 𝑢 ∈ ( 𝑂 ‘ { 𝐸 } ) 𝑋 = ( 𝑎 + 𝑢 ) ↔ ∃ 𝑢 ∈ ( 𝑂 ‘ { 𝐸 } ) ∃ 𝑎 ∈ ( 𝑁 ‘ { 𝐸 } ) 𝑋 = ( 𝑎 + 𝑢 ) )
42 df-rex ⊢ ( ∃ 𝑎 ∈ ( 𝑁 ‘ { 𝐸 } ) 𝑋 = ( 𝑎 + 𝑢 ) ↔ ∃ 𝑎 ( 𝑎 ∈ ( 𝑁 ‘ { 𝐸 } ) ∧ 𝑋 = ( 𝑎 + 𝑢 ) ) )
43 8 9 5 7 11 lspsnel ⊢ ( ( 𝑈 ∈ LMod ∧ 𝐸 ∈ 𝑉 ) → ( 𝑎 ∈ ( 𝑁 ‘ { 𝐸 } ) ↔ ∃ 𝑘 ∈ 𝐵 𝑎 = ( 𝑘 · 𝐸 ) ) )
44 15 20 43 syl2anc ⊢ ( 𝜑 → ( 𝑎 ∈ ( 𝑁 ‘ { 𝐸 } ) ↔ ∃ 𝑘 ∈ 𝐵 𝑎 = ( 𝑘 · 𝐸 ) ) )
45 44 anbi1d ⊢ ( 𝜑 → ( ( 𝑎 ∈ ( 𝑁 ‘ { 𝐸 } ) ∧ 𝑋 = ( 𝑎 + 𝑢 ) ) ↔ ( ∃ 𝑘 ∈ 𝐵 𝑎 = ( 𝑘 · 𝐸 ) ∧ 𝑋 = ( 𝑎 + 𝑢 ) ) ) )
46 r19.41v ⊢ ( ∃ 𝑘 ∈ 𝐵 ( 𝑎 = ( 𝑘 · 𝐸 ) ∧ 𝑋 = ( 𝑎 + 𝑢 ) ) ↔ ( ∃ 𝑘 ∈ 𝐵 𝑎 = ( 𝑘 · 𝐸 ) ∧ 𝑋 = ( 𝑎 + 𝑢 ) ) )
47 45 46 bitr4di ⊢ ( 𝜑 → ( ( 𝑎 ∈ ( 𝑁 ‘ { 𝐸 } ) ∧ 𝑋 = ( 𝑎 + 𝑢 ) ) ↔ ∃ 𝑘 ∈ 𝐵 ( 𝑎 = ( 𝑘 · 𝐸 ) ∧ 𝑋 = ( 𝑎 + 𝑢 ) ) ) )
48 47 exbidv ⊢ ( 𝜑 → ( ∃ 𝑎 ( 𝑎 ∈ ( 𝑁 ‘ { 𝐸 } ) ∧ 𝑋 = ( 𝑎 + 𝑢 ) ) ↔ ∃ 𝑎 ∃ 𝑘 ∈ 𝐵 ( 𝑎 = ( 𝑘 · 𝐸 ) ∧ 𝑋 = ( 𝑎 + 𝑢 ) ) ) )
49 rexcom4 ⊢ ( ∃ 𝑘 ∈ 𝐵 ∃ 𝑎 ( 𝑎 = ( 𝑘 · 𝐸 ) ∧ 𝑋 = ( 𝑎 + 𝑢 ) ) ↔ ∃ 𝑎 ∃ 𝑘 ∈ 𝐵 ( 𝑎 = ( 𝑘 · 𝐸 ) ∧ 𝑋 = ( 𝑎 + 𝑢 ) ) )
50 ovex ⊢ ( 𝑘 · 𝐸 ) ∈ V
51 oveq1 ⊢ ( 𝑎 = ( 𝑘 · 𝐸 ) → ( 𝑎 + 𝑢 ) = ( ( 𝑘 · 𝐸 ) + 𝑢 ) )
52 51 eqeq2d ⊢ ( 𝑎 = ( 𝑘 · 𝐸 ) → ( 𝑋 = ( 𝑎 + 𝑢 ) ↔ 𝑋 = ( ( 𝑘 · 𝐸 ) + 𝑢 ) ) )
53 50 52 ceqsexv ⊢ ( ∃ 𝑎 ( 𝑎 = ( 𝑘 · 𝐸 ) ∧ 𝑋 = ( 𝑎 + 𝑢 ) ) ↔ 𝑋 = ( ( 𝑘 · 𝐸 ) + 𝑢 ) )
54 53 rexbii ⊢ ( ∃ 𝑘 ∈ 𝐵 ∃ 𝑎 ( 𝑎 = ( 𝑘 · 𝐸 ) ∧ 𝑋 = ( 𝑎 + 𝑢 ) ) ↔ ∃ 𝑘 ∈ 𝐵 𝑋 = ( ( 𝑘 · 𝐸 ) + 𝑢 ) )
55 49 54 bitr3i ⊢ ( ∃ 𝑎 ∃ 𝑘 ∈ 𝐵 ( 𝑎 = ( 𝑘 · 𝐸 ) ∧ 𝑋 = ( 𝑎 + 𝑢 ) ) ↔ ∃ 𝑘 ∈ 𝐵 𝑋 = ( ( 𝑘 · 𝐸 ) + 𝑢 ) )
56 48 55 bitrdi ⊢ ( 𝜑 → ( ∃ 𝑎 ( 𝑎 ∈ ( 𝑁 ‘ { 𝐸 } ) ∧ 𝑋 = ( 𝑎 + 𝑢 ) ) ↔ ∃ 𝑘 ∈ 𝐵 𝑋 = ( ( 𝑘 · 𝐸 ) + 𝑢 ) ) )
57 42 56 syl5bb ⊢ ( 𝜑 → ( ∃ 𝑎 ∈ ( 𝑁 ‘ { 𝐸 } ) 𝑋 = ( 𝑎 + 𝑢 ) ↔ ∃ 𝑘 ∈ 𝐵 𝑋 = ( ( 𝑘 · 𝐸 ) + 𝑢 ) ) )
58 57 rexbidv ⊢ ( 𝜑 → ( ∃ 𝑢 ∈ ( 𝑂 ‘ { 𝐸 } ) ∃ 𝑎 ∈ ( 𝑁 ‘ { 𝐸 } ) 𝑋 = ( 𝑎 + 𝑢 ) ↔ ∃ 𝑢 ∈ ( 𝑂 ‘ { 𝐸 } ) ∃ 𝑘 ∈ 𝐵 𝑋 = ( ( 𝑘 · 𝐸 ) + 𝑢 ) ) )
59 41 58 syl5bb ⊢ ( 𝜑 → ( ∃ 𝑎 ∈ ( 𝑁 ‘ { 𝐸 } ) ∃ 𝑢 ∈ ( 𝑂 ‘ { 𝐸 } ) 𝑋 = ( 𝑎 + 𝑢 ) ↔ ∃ 𝑢 ∈ ( 𝑂 ‘ { 𝐸 } ) ∃ 𝑘 ∈ 𝐵 𝑋 = ( ( 𝑘 · 𝐸 ) + 𝑢 ) ) )
60 40 59 mpbid ⊢ ( 𝜑 → ∃ 𝑢 ∈ ( 𝑂 ‘ { 𝐸 } ) ∃ 𝑘 ∈ 𝐵 𝑋 = ( ( 𝑘 · 𝐸 ) + 𝑢 ) )