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 ( 𝜑 → ( ( 𝑆 ‘ ( ( 𝑚 · 𝐸 ) + 𝑥 ) ) ‘ ( ( 𝑛 · 𝐸 ) + 𝑦 ) ) = ( ( 𝑛 × ( 𝐺𝑚 ) ) ( ( 𝑆𝑥 ) ‘ 𝑦 ) ) )