Metamath Proof Explorer

Theorem hdmapglem7b

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 ⊢ ( 𝜑 → 𝑋 ∈ 𝑉 )
hdmapglem7.t ⊢ × = ( .r ‘ 𝑅 )
hdmapglem7.z ⊢ 0 = ( 0g ‘ 𝑅 )
hdmapglem7.c ⊢ ✚ = ( +g ‘ 𝑅 )
hdmapglem7.s ⊢ 𝑆 = ( ( HDMap ‘ 𝐾 ) ‘ 𝑊 )
hdmapglem7.g ⊢ 𝐺 = ( ( HGMap ‘ 𝐾 ) ‘ 𝑊 )
hdmapglem7b.u ⊢ ( 𝜑 → 𝑥 ∈ ( 𝑂 ‘ { 𝐸 } ) )
hdmapglem7b.v ⊢ ( 𝜑 → 𝑦 ∈ ( 𝑂 ‘ { 𝐸 } ) )
hdmapglem7b.k ⊢ ( 𝜑 → 𝑚 ∈ 𝐵 )
hdmapglem7b.l ⊢ ( 𝜑 → 𝑛 ∈ 𝐵 )
Assertion hdmapglem7b ( 𝜑 → ( ( 𝑆 ‘ ( ( 𝑚 · 𝐸 ) + 𝑥 ) ) ‘ ( ( 𝑛 · 𝐸 ) + 𝑦 ) ) = ( ( 𝑛 × ( 𝐺 ‘ 𝑚 ) ) ✚ ( ( 𝑆 ‘ 𝑥 ) ‘ 𝑦 ) ) )

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 hdmapglem7.t ⊢ × = ( .r ‘ 𝑅 )
15 hdmapglem7.z ⊢ 0 = ( 0g ‘ 𝑅 )
16 hdmapglem7.c ⊢ ✚ = ( +g ‘ 𝑅 )
17 hdmapglem7.s ⊢ 𝑆 = ( ( HDMap ‘ 𝐾 ) ‘ 𝑊 )
18 hdmapglem7.g ⊢ 𝐺 = ( ( HGMap ‘ 𝐾 ) ‘ 𝑊 )
19 hdmapglem7b.u ⊢ ( 𝜑 → 𝑥 ∈ ( 𝑂 ‘ { 𝐸 } ) )
20 hdmapglem7b.v ⊢ ( 𝜑 → 𝑦 ∈ ( 𝑂 ‘ { 𝐸 } ) )
21 hdmapglem7b.k ⊢ ( 𝜑 → 𝑚 ∈ 𝐵 )
22 hdmapglem7b.l ⊢ ( 𝜑 → 𝑛 ∈ 𝐵 )
23 1 4 12 dvhlmod ⊢ ( 𝜑 → 𝑈 ∈ LMod )
24 eqid ⊢ ( Base ‘ 𝐾 ) = ( Base ‘ 𝐾 )
25 eqid ⊢ ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 ) = ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 )
26 eqid ⊢ ( 0g ‘ 𝑈 ) = ( 0g ‘ 𝑈 )
27 1 24 25 4 5 26 2 12 dvheveccl ⊢ ( 𝜑 → 𝐸 ∈ ( 𝑉 ∖ { ( 0g ‘ 𝑈 ) } ) )
28 27 eldifad ⊢ ( 𝜑 → 𝐸 ∈ 𝑉 )
29 5 8 7 9 lmodvscl ⊢ ( ( 𝑈 ∈ LMod ∧ 𝑛 ∈ 𝐵 ∧ 𝐸 ∈ 𝑉 ) → ( 𝑛 · 𝐸 ) ∈ 𝑉 )
30 23 22 28 29 syl3anc ⊢ ( 𝜑 → ( 𝑛 · 𝐸 ) ∈ 𝑉 )
31 28 snssd ⊢ ( 𝜑 → { 𝐸 } ⊆ 𝑉 )
32 1 4 5 3 dochssv ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ { 𝐸 } ⊆ 𝑉 ) → ( 𝑂 ‘ { 𝐸 } ) ⊆ 𝑉 )
33 12 31 32 syl2anc ⊢ ( 𝜑 → ( 𝑂 ‘ { 𝐸 } ) ⊆ 𝑉 )
34 33 20 sseldd ⊢ ( 𝜑 → 𝑦 ∈ 𝑉 )
35 5 6 lmodvacl ⊢ ( ( 𝑈 ∈ LMod ∧ ( 𝑛 · 𝐸 ) ∈ 𝑉 ∧ 𝑦 ∈ 𝑉 ) → ( ( 𝑛 · 𝐸 ) + 𝑦 ) ∈ 𝑉 )
36 23 30 34 35 syl3anc ⊢ ( 𝜑 → ( ( 𝑛 · 𝐸 ) + 𝑦 ) ∈ 𝑉 )
37 33 19 sseldd ⊢ ( 𝜑 → 𝑥 ∈ 𝑉 )
38 1 4 5 6 7 8 9 16 14 17 18 12 36 28 37 21 hdmapgln2 ⊢ ( 𝜑 → ( ( 𝑆 ‘ ( ( 𝑚 · 𝐸 ) + 𝑥 ) ) ‘ ( ( 𝑛 · 𝐸 ) + 𝑦 ) ) = ( ( ( ( 𝑆 ‘ 𝐸 ) ‘ ( ( 𝑛 · 𝐸 ) + 𝑦 ) ) × ( 𝐺 ‘ 𝑚 ) ) ✚ ( ( 𝑆 ‘ 𝑥 ) ‘ ( ( 𝑛 · 𝐸 ) + 𝑦 ) ) ) )
39 1 4 5 6 7 8 9 16 14 17 12 28 34 28 22 hdmapln1 ⊢ ( 𝜑 → ( ( 𝑆 ‘ 𝐸 ) ‘ ( ( 𝑛 · 𝐸 ) + 𝑦 ) ) = ( ( 𝑛 × ( ( 𝑆 ‘ 𝐸 ) ‘ 𝐸 ) ) ✚ ( ( 𝑆 ‘ 𝐸 ) ‘ 𝑦 ) ) )
40 eqid ⊢ ( ( HVMap ‘ 𝐾 ) ‘ 𝑊 ) = ( ( HVMap ‘ 𝐾 ) ‘ 𝑊 )
41 eqid ⊢ ( 1r ‘ 𝑅 ) = ( 1r ‘ 𝑅 )
42 1 2 40 17 12 4 8 41 hdmapevec2 ⊢ ( 𝜑 → ( ( 𝑆 ‘ 𝐸 ) ‘ 𝐸 ) = ( 1r ‘ 𝑅 ) )
43 42 oveq2d ⊢ ( 𝜑 → ( 𝑛 × ( ( 𝑆 ‘ 𝐸 ) ‘ 𝐸 ) ) = ( 𝑛 × ( 1r ‘ 𝑅 ) ) )
44 8 lmodring ⊢ ( 𝑈 ∈ LMod → 𝑅 ∈ Ring )
45 23 44 syl ⊢ ( 𝜑 → 𝑅 ∈ Ring )
46 9 14 41 ringridm ⊢ ( ( 𝑅 ∈ Ring ∧ 𝑛 ∈ 𝐵 ) → ( 𝑛 × ( 1r ‘ 𝑅 ) ) = 𝑛 )
47 45 22 46 syl2anc ⊢ ( 𝜑 → ( 𝑛 × ( 1r ‘ 𝑅 ) ) = 𝑛 )
48 43 47 eqtrd ⊢ ( 𝜑 → ( 𝑛 × ( ( 𝑆 ‘ 𝐸 ) ‘ 𝐸 ) ) = 𝑛 )
49 1 2 3 4 5 8 9 14 15 17 12 20 hdmapinvlem1 ⊢ ( 𝜑 → ( ( 𝑆 ‘ 𝐸 ) ‘ 𝑦 ) = 0 )
50 48 49 oveq12d ⊢ ( 𝜑 → ( ( 𝑛 × ( ( 𝑆 ‘ 𝐸 ) ‘ 𝐸 ) ) ✚ ( ( 𝑆 ‘ 𝐸 ) ‘ 𝑦 ) ) = ( 𝑛 ✚ 0 ) )
51 ringgrp ⊢ ( 𝑅 ∈ Ring → 𝑅 ∈ Grp )
52 45 51 syl ⊢ ( 𝜑 → 𝑅 ∈ Grp )
53 9 16 15 grprid ⊢ ( ( 𝑅 ∈ Grp ∧ 𝑛 ∈ 𝐵 ) → ( 𝑛 ✚ 0 ) = 𝑛 )
54 52 22 53 syl2anc ⊢ ( 𝜑 → ( 𝑛 ✚ 0 ) = 𝑛 )
55 39 50 54 3eqtrd ⊢ ( 𝜑 → ( ( 𝑆 ‘ 𝐸 ) ‘ ( ( 𝑛 · 𝐸 ) + 𝑦 ) ) = 𝑛 )
56 55 oveq1d ⊢ ( 𝜑 → ( ( ( 𝑆 ‘ 𝐸 ) ‘ ( ( 𝑛 · 𝐸 ) + 𝑦 ) ) × ( 𝐺 ‘ 𝑚 ) ) = ( 𝑛 × ( 𝐺 ‘ 𝑚 ) ) )
57 1 4 5 6 7 8 9 16 14 17 12 28 34 37 22 hdmapln1 ⊢ ( 𝜑 → ( ( 𝑆 ‘ 𝑥 ) ‘ ( ( 𝑛 · 𝐸 ) + 𝑦 ) ) = ( ( 𝑛 × ( ( 𝑆 ‘ 𝑥 ) ‘ 𝐸 ) ) ✚ ( ( 𝑆 ‘ 𝑥 ) ‘ 𝑦 ) ) )
58 1 2 3 4 5 8 9 14 15 17 12 19 hdmapinvlem2 ⊢ ( 𝜑 → ( ( 𝑆 ‘ 𝑥 ) ‘ 𝐸 ) = 0 )
59 58 oveq2d ⊢ ( 𝜑 → ( 𝑛 × ( ( 𝑆 ‘ 𝑥 ) ‘ 𝐸 ) ) = ( 𝑛 × 0 ) )
60 9 14 15 ringrz ⊢ ( ( 𝑅 ∈ Ring ∧ 𝑛 ∈ 𝐵 ) → ( 𝑛 × 0 ) = 0 )
61 45 22 60 syl2anc ⊢ ( 𝜑 → ( 𝑛 × 0 ) = 0 )
62 59 61 eqtrd ⊢ ( 𝜑 → ( 𝑛 × ( ( 𝑆 ‘ 𝑥 ) ‘ 𝐸 ) ) = 0 )
63 62 oveq1d ⊢ ( 𝜑 → ( ( 𝑛 × ( ( 𝑆 ‘ 𝑥 ) ‘ 𝐸 ) ) ✚ ( ( 𝑆 ‘ 𝑥 ) ‘ 𝑦 ) ) = ( 0 ✚ ( ( 𝑆 ‘ 𝑥 ) ‘ 𝑦 ) ) )
64 1 4 5 8 9 17 12 34 37 hdmapipcl ⊢ ( 𝜑 → ( ( 𝑆 ‘ 𝑥 ) ‘ 𝑦 ) ∈ 𝐵 )
65 9 16 15 grplid ⊢ ( ( 𝑅 ∈ Grp ∧ ( ( 𝑆 ‘ 𝑥 ) ‘ 𝑦 ) ∈ 𝐵 ) → ( 0 ✚ ( ( 𝑆 ‘ 𝑥 ) ‘ 𝑦 ) ) = ( ( 𝑆 ‘ 𝑥 ) ‘ 𝑦 ) )
66 52 64 65 syl2anc ⊢ ( 𝜑 → ( 0 ✚ ( ( 𝑆 ‘ 𝑥 ) ‘ 𝑦 ) ) = ( ( 𝑆 ‘ 𝑥 ) ‘ 𝑦 ) )
67 57 63 66 3eqtrd ⊢ ( 𝜑 → ( ( 𝑆 ‘ 𝑥 ) ‘ ( ( 𝑛 · 𝐸 ) + 𝑦 ) ) = ( ( 𝑆 ‘ 𝑥 ) ‘ 𝑦 ) )
68 56 67 oveq12d ⊢ ( 𝜑 → ( ( ( ( 𝑆 ‘ 𝐸 ) ‘ ( ( 𝑛 · 𝐸 ) + 𝑦 ) ) × ( 𝐺 ‘ 𝑚 ) ) ✚ ( ( 𝑆 ‘ 𝑥 ) ‘ ( ( 𝑛 · 𝐸 ) + 𝑦 ) ) ) = ( ( 𝑛 × ( 𝐺 ‘ 𝑚 ) ) ✚ ( ( 𝑆 ‘ 𝑥 ) ‘ 𝑦 ) ) )
69 38 68 eqtrd ⊢ ( 𝜑 → ( ( 𝑆 ‘ ( ( 𝑚 · 𝐸 ) + 𝑥 ) ) ‘ ( ( 𝑛 · 𝐸 ) + 𝑦 ) ) = ( ( 𝑛 × ( 𝐺 ‘ 𝑚 ) ) ✚ ( ( 𝑆 ‘ 𝑥 ) ‘ 𝑦 ) ) )