Metamath Proof Explorer

Theorem hgmapmul

Description: Part 15 of Baer p. 50 line 16. The multiplication is reversed after converting to the dual space scalar to the vector space scalar. (Contributed by NM, 7-Jun-2015)

Ref Expression
Hypotheses hgmapmul.h ⊢ 𝐻 = ( LHyp ‘ 𝐾 )
hgmapmul.u ⊢ 𝑈 = ( ( DVecH ‘ 𝐾 ) ‘ 𝑊 )
hgmapmul.r ⊢ 𝑅 = ( Scalar ‘ 𝑈 )
hgmapmul.b ⊢ 𝐵 = ( Base ‘ 𝑅 )
hgmapmul.t ⊢ · = ( .r ‘ 𝑅 )
hgmapmul.g ⊢ 𝐺 = ( ( HGMap ‘ 𝐾 ) ‘ 𝑊 )
hgmapmul.k ⊢ ( 𝜑 → ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) )
hgmapmul.x ⊢ ( 𝜑 → 𝑋 ∈ 𝐵 )
hgmapmul.y ⊢ ( 𝜑 → 𝑌 ∈ 𝐵 )
Assertion hgmapmul ( 𝜑 → ( 𝐺 ‘ ( 𝑋 · 𝑌 ) ) = ( ( 𝐺 ‘ 𝑌 ) · ( 𝐺 ‘ 𝑋 ) ) )

Proof

Step Hyp Ref Expression
1 hgmapmul.h ⊢ 𝐻 = ( LHyp ‘ 𝐾 )
2 hgmapmul.u ⊢ 𝑈 = ( ( DVecH ‘ 𝐾 ) ‘ 𝑊 )
3 hgmapmul.r ⊢ 𝑅 = ( Scalar ‘ 𝑈 )
4 hgmapmul.b ⊢ 𝐵 = ( Base ‘ 𝑅 )
5 hgmapmul.t ⊢ · = ( .r ‘ 𝑅 )
6 hgmapmul.g ⊢ 𝐺 = ( ( HGMap ‘ 𝐾 ) ‘ 𝑊 )
7 hgmapmul.k ⊢ ( 𝜑 → ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) )
8 hgmapmul.x ⊢ ( 𝜑 → 𝑋 ∈ 𝐵 )
9 hgmapmul.y ⊢ ( 𝜑 → 𝑌 ∈ 𝐵 )
10 eqid ⊢ ( Base ‘ 𝑈 ) = ( Base ‘ 𝑈 )
11 eqid ⊢ ( 0g ‘ 𝑈 ) = ( 0g ‘ 𝑈 )
12 1 2 10 11 7 dvh1dim ⊢ ( 𝜑 → ∃ 𝑡 ∈ ( Base ‘ 𝑈 ) 𝑡 ≠ ( 0g ‘ 𝑈 ) )
13 eqid ⊢ ( ( LCDual ‘ 𝐾 ) ‘ 𝑊 ) = ( ( LCDual ‘ 𝐾 ) ‘ 𝑊 )
14 1 13 7 lcdlmod ⊢ ( 𝜑 → ( ( LCDual ‘ 𝐾 ) ‘ 𝑊 ) ∈ LMod )
15 14 3ad2ant1 ⊢ ( ( 𝜑 ∧ 𝑡 ∈ ( Base ‘ 𝑈 ) ∧ 𝑡 ≠ ( 0g ‘ 𝑈 ) ) → ( ( LCDual ‘ 𝐾 ) ‘ 𝑊 ) ∈ LMod )
16 eqid ⊢ ( Scalar ‘ ( ( LCDual ‘ 𝐾 ) ‘ 𝑊 ) ) = ( Scalar ‘ ( ( LCDual ‘ 𝐾 ) ‘ 𝑊 ) )
17 eqid ⊢ ( Base ‘ ( Scalar ‘ ( ( LCDual ‘ 𝐾 ) ‘ 𝑊 ) ) ) = ( Base ‘ ( Scalar ‘ ( ( LCDual ‘ 𝐾 ) ‘ 𝑊 ) ) )
18 1 2 3 4 13 16 17 6 7 8 hgmapdcl ⊢ ( 𝜑 → ( 𝐺 ‘ 𝑋 ) ∈ ( Base ‘ ( Scalar ‘ ( ( LCDual ‘ 𝐾 ) ‘ 𝑊 ) ) ) )
19 18 3ad2ant1 ⊢ ( ( 𝜑 ∧ 𝑡 ∈ ( Base ‘ 𝑈 ) ∧ 𝑡 ≠ ( 0g ‘ 𝑈 ) ) → ( 𝐺 ‘ 𝑋 ) ∈ ( Base ‘ ( Scalar ‘ ( ( LCDual ‘ 𝐾 ) ‘ 𝑊 ) ) ) )
20 1 2 3 4 13 16 17 6 7 9 hgmapdcl ⊢ ( 𝜑 → ( 𝐺 ‘ 𝑌 ) ∈ ( Base ‘ ( Scalar ‘ ( ( LCDual ‘ 𝐾 ) ‘ 𝑊 ) ) ) )
21 20 3ad2ant1 ⊢ ( ( 𝜑 ∧ 𝑡 ∈ ( Base ‘ 𝑈 ) ∧ 𝑡 ≠ ( 0g ‘ 𝑈 ) ) → ( 𝐺 ‘ 𝑌 ) ∈ ( Base ‘ ( Scalar ‘ ( ( LCDual ‘ 𝐾 ) ‘ 𝑊 ) ) ) )
22 eqid ⊢ ( Base ‘ ( ( LCDual ‘ 𝐾 ) ‘ 𝑊 ) ) = ( Base ‘ ( ( LCDual ‘ 𝐾 ) ‘ 𝑊 ) )
23 eqid ⊢ ( ( HDMap ‘ 𝐾 ) ‘ 𝑊 ) = ( ( HDMap ‘ 𝐾 ) ‘ 𝑊 )
24 7 3ad2ant1 ⊢ ( ( 𝜑 ∧ 𝑡 ∈ ( Base ‘ 𝑈 ) ∧ 𝑡 ≠ ( 0g ‘ 𝑈 ) ) → ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) )
25 simp2 ⊢ ( ( 𝜑 ∧ 𝑡 ∈ ( Base ‘ 𝑈 ) ∧ 𝑡 ≠ ( 0g ‘ 𝑈 ) ) → 𝑡 ∈ ( Base ‘ 𝑈 ) )
26 1 2 10 13 22 23 24 25 hdmapcl ⊢ ( ( 𝜑 ∧ 𝑡 ∈ ( Base ‘ 𝑈 ) ∧ 𝑡 ≠ ( 0g ‘ 𝑈 ) ) → ( ( ( HDMap ‘ 𝐾 ) ‘ 𝑊 ) ‘ 𝑡 ) ∈ ( Base ‘ ( ( LCDual ‘ 𝐾 ) ‘ 𝑊 ) ) )
27 eqid ⊢ ( ·𝑠 ‘ ( ( LCDual ‘ 𝐾 ) ‘ 𝑊 ) ) = ( ·𝑠 ‘ ( ( LCDual ‘ 𝐾 ) ‘ 𝑊 ) )
28 eqid ⊢ ( .r ‘ ( Scalar ‘ ( ( LCDual ‘ 𝐾 ) ‘ 𝑊 ) ) ) = ( .r ‘ ( Scalar ‘ ( ( LCDual ‘ 𝐾 ) ‘ 𝑊 ) ) )
29 22 16 27 17 28 lmodvsass ⊢ ( ( ( ( LCDual ‘ 𝐾 ) ‘ 𝑊 ) ∈ LMod ∧ ( ( 𝐺 ‘ 𝑋 ) ∈ ( Base ‘ ( Scalar ‘ ( ( LCDual ‘ 𝐾 ) ‘ 𝑊 ) ) ) ∧ ( 𝐺 ‘ 𝑌 ) ∈ ( Base ‘ ( Scalar ‘ ( ( LCDual ‘ 𝐾 ) ‘ 𝑊 ) ) ) ∧ ( ( ( HDMap ‘ 𝐾 ) ‘ 𝑊 ) ‘ 𝑡 ) ∈ ( Base ‘ ( ( LCDual ‘ 𝐾 ) ‘ 𝑊 ) ) ) ) → ( ( ( 𝐺 ‘ 𝑋 ) ( .r ‘ ( Scalar ‘ ( ( LCDual ‘ 𝐾 ) ‘ 𝑊 ) ) ) ( 𝐺 ‘ 𝑌 ) ) ( ·𝑠 ‘ ( ( LCDual ‘ 𝐾 ) ‘ 𝑊 ) ) ( ( ( HDMap ‘ 𝐾 ) ‘ 𝑊 ) ‘ 𝑡 ) ) = ( ( 𝐺 ‘ 𝑋 ) ( ·𝑠 ‘ ( ( LCDual ‘ 𝐾 ) ‘ 𝑊 ) ) ( ( 𝐺 ‘ 𝑌 ) ( ·𝑠 ‘ ( ( LCDual ‘ 𝐾 ) ‘ 𝑊 ) ) ( ( ( HDMap ‘ 𝐾 ) ‘ 𝑊 ) ‘ 𝑡 ) ) ) )
30 15 19 21 26 29 syl13anc ⊢ ( ( 𝜑 ∧ 𝑡 ∈ ( Base ‘ 𝑈 ) ∧ 𝑡 ≠ ( 0g ‘ 𝑈 ) ) → ( ( ( 𝐺 ‘ 𝑋 ) ( .r ‘ ( Scalar ‘ ( ( LCDual ‘ 𝐾 ) ‘ 𝑊 ) ) ) ( 𝐺 ‘ 𝑌 ) ) ( ·𝑠 ‘ ( ( LCDual ‘ 𝐾 ) ‘ 𝑊 ) ) ( ( ( HDMap ‘ 𝐾 ) ‘ 𝑊 ) ‘ 𝑡 ) ) = ( ( 𝐺 ‘ 𝑋 ) ( ·𝑠 ‘ ( ( LCDual ‘ 𝐾 ) ‘ 𝑊 ) ) ( ( 𝐺 ‘ 𝑌 ) ( ·𝑠 ‘ ( ( LCDual ‘ 𝐾 ) ‘ 𝑊 ) ) ( ( ( HDMap ‘ 𝐾 ) ‘ 𝑊 ) ‘ 𝑡 ) ) ) )
31 1 2 7 dvhlmod ⊢ ( 𝜑 → 𝑈 ∈ LMod )
32 31 3ad2ant1 ⊢ ( ( 𝜑 ∧ 𝑡 ∈ ( Base ‘ 𝑈 ) ∧ 𝑡 ≠ ( 0g ‘ 𝑈 ) ) → 𝑈 ∈ LMod )
33 8 3ad2ant1 ⊢ ( ( 𝜑 ∧ 𝑡 ∈ ( Base ‘ 𝑈 ) ∧ 𝑡 ≠ ( 0g ‘ 𝑈 ) ) → 𝑋 ∈ 𝐵 )
34 9 3ad2ant1 ⊢ ( ( 𝜑 ∧ 𝑡 ∈ ( Base ‘ 𝑈 ) ∧ 𝑡 ≠ ( 0g ‘ 𝑈 ) ) → 𝑌 ∈ 𝐵 )
35 eqid ⊢ ( ·𝑠 ‘ 𝑈 ) = ( ·𝑠 ‘ 𝑈 )
36 10 3 35 4 5 lmodvsass ⊢ ( ( 𝑈 ∈ LMod ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑡 ∈ ( Base ‘ 𝑈 ) ) ) → ( ( 𝑋 · 𝑌 ) ( ·𝑠 ‘ 𝑈 ) 𝑡 ) = ( 𝑋 ( ·𝑠 ‘ 𝑈 ) ( 𝑌 ( ·𝑠 ‘ 𝑈 ) 𝑡 ) ) )
37 32 33 34 25 36 syl13anc ⊢ ( ( 𝜑 ∧ 𝑡 ∈ ( Base ‘ 𝑈 ) ∧ 𝑡 ≠ ( 0g ‘ 𝑈 ) ) → ( ( 𝑋 · 𝑌 ) ( ·𝑠 ‘ 𝑈 ) 𝑡 ) = ( 𝑋 ( ·𝑠 ‘ 𝑈 ) ( 𝑌 ( ·𝑠 ‘ 𝑈 ) 𝑡 ) ) )
38 37 fveq2d ⊢ ( ( 𝜑 ∧ 𝑡 ∈ ( Base ‘ 𝑈 ) ∧ 𝑡 ≠ ( 0g ‘ 𝑈 ) ) → ( ( ( HDMap ‘ 𝐾 ) ‘ 𝑊 ) ‘ ( ( 𝑋 · 𝑌 ) ( ·𝑠 ‘ 𝑈 ) 𝑡 ) ) = ( ( ( HDMap ‘ 𝐾 ) ‘ 𝑊 ) ‘ ( 𝑋 ( ·𝑠 ‘ 𝑈 ) ( 𝑌 ( ·𝑠 ‘ 𝑈 ) 𝑡 ) ) ) )
39 10 3 35 4 lmodvscl ⊢ ( ( 𝑈 ∈ LMod ∧ 𝑌 ∈ 𝐵 ∧ 𝑡 ∈ ( Base ‘ 𝑈 ) ) → ( 𝑌 ( ·𝑠 ‘ 𝑈 ) 𝑡 ) ∈ ( Base ‘ 𝑈 ) )
40 32 34 25 39 syl3anc ⊢ ( ( 𝜑 ∧ 𝑡 ∈ ( Base ‘ 𝑈 ) ∧ 𝑡 ≠ ( 0g ‘ 𝑈 ) ) → ( 𝑌 ( ·𝑠 ‘ 𝑈 ) 𝑡 ) ∈ ( Base ‘ 𝑈 ) )
41 1 2 10 35 3 4 13 27 23 6 24 40 33 hgmapvs ⊢ ( ( 𝜑 ∧ 𝑡 ∈ ( Base ‘ 𝑈 ) ∧ 𝑡 ≠ ( 0g ‘ 𝑈 ) ) → ( ( ( HDMap ‘ 𝐾 ) ‘ 𝑊 ) ‘ ( 𝑋 ( ·𝑠 ‘ 𝑈 ) ( 𝑌 ( ·𝑠 ‘ 𝑈 ) 𝑡 ) ) ) = ( ( 𝐺 ‘ 𝑋 ) ( ·𝑠 ‘ ( ( LCDual ‘ 𝐾 ) ‘ 𝑊 ) ) ( ( ( HDMap ‘ 𝐾 ) ‘ 𝑊 ) ‘ ( 𝑌 ( ·𝑠 ‘ 𝑈 ) 𝑡 ) ) ) )
42 1 2 10 35 3 4 13 27 23 6 24 25 34 hgmapvs ⊢ ( ( 𝜑 ∧ 𝑡 ∈ ( Base ‘ 𝑈 ) ∧ 𝑡 ≠ ( 0g ‘ 𝑈 ) ) → ( ( ( HDMap ‘ 𝐾 ) ‘ 𝑊 ) ‘ ( 𝑌 ( ·𝑠 ‘ 𝑈 ) 𝑡 ) ) = ( ( 𝐺 ‘ 𝑌 ) ( ·𝑠 ‘ ( ( LCDual ‘ 𝐾 ) ‘ 𝑊 ) ) ( ( ( HDMap ‘ 𝐾 ) ‘ 𝑊 ) ‘ 𝑡 ) ) )
43 42 oveq2d ⊢ ( ( 𝜑 ∧ 𝑡 ∈ ( Base ‘ 𝑈 ) ∧ 𝑡 ≠ ( 0g ‘ 𝑈 ) ) → ( ( 𝐺 ‘ 𝑋 ) ( ·𝑠 ‘ ( ( LCDual ‘ 𝐾 ) ‘ 𝑊 ) ) ( ( ( HDMap ‘ 𝐾 ) ‘ 𝑊 ) ‘ ( 𝑌 ( ·𝑠 ‘ 𝑈 ) 𝑡 ) ) ) = ( ( 𝐺 ‘ 𝑋 ) ( ·𝑠 ‘ ( ( LCDual ‘ 𝐾 ) ‘ 𝑊 ) ) ( ( 𝐺 ‘ 𝑌 ) ( ·𝑠 ‘ ( ( LCDual ‘ 𝐾 ) ‘ 𝑊 ) ) ( ( ( HDMap ‘ 𝐾 ) ‘ 𝑊 ) ‘ 𝑡 ) ) ) )
44 38 41 43 3eqtrd ⊢ ( ( 𝜑 ∧ 𝑡 ∈ ( Base ‘ 𝑈 ) ∧ 𝑡 ≠ ( 0g ‘ 𝑈 ) ) → ( ( ( HDMap ‘ 𝐾 ) ‘ 𝑊 ) ‘ ( ( 𝑋 · 𝑌 ) ( ·𝑠 ‘ 𝑈 ) 𝑡 ) ) = ( ( 𝐺 ‘ 𝑋 ) ( ·𝑠 ‘ ( ( LCDual ‘ 𝐾 ) ‘ 𝑊 ) ) ( ( 𝐺 ‘ 𝑌 ) ( ·𝑠 ‘ ( ( LCDual ‘ 𝐾 ) ‘ 𝑊 ) ) ( ( ( HDMap ‘ 𝐾 ) ‘ 𝑊 ) ‘ 𝑡 ) ) ) )
45 3 4 5 lmodmcl ⊢ ( ( 𝑈 ∈ LMod ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) → ( 𝑋 · 𝑌 ) ∈ 𝐵 )
46 31 8 9 45 syl3anc ⊢ ( 𝜑 → ( 𝑋 · 𝑌 ) ∈ 𝐵 )
47 46 3ad2ant1 ⊢ ( ( 𝜑 ∧ 𝑡 ∈ ( Base ‘ 𝑈 ) ∧ 𝑡 ≠ ( 0g ‘ 𝑈 ) ) → ( 𝑋 · 𝑌 ) ∈ 𝐵 )
48 1 2 10 35 3 4 13 27 23 6 24 25 47 hgmapvs ⊢ ( ( 𝜑 ∧ 𝑡 ∈ ( Base ‘ 𝑈 ) ∧ 𝑡 ≠ ( 0g ‘ 𝑈 ) ) → ( ( ( HDMap ‘ 𝐾 ) ‘ 𝑊 ) ‘ ( ( 𝑋 · 𝑌 ) ( ·𝑠 ‘ 𝑈 ) 𝑡 ) ) = ( ( 𝐺 ‘ ( 𝑋 · 𝑌 ) ) ( ·𝑠 ‘ ( ( LCDual ‘ 𝐾 ) ‘ 𝑊 ) ) ( ( ( HDMap ‘ 𝐾 ) ‘ 𝑊 ) ‘ 𝑡 ) ) )
49 30 44 48 3eqtr2rd ⊢ ( ( 𝜑 ∧ 𝑡 ∈ ( Base ‘ 𝑈 ) ∧ 𝑡 ≠ ( 0g ‘ 𝑈 ) ) → ( ( 𝐺 ‘ ( 𝑋 · 𝑌 ) ) ( ·𝑠 ‘ ( ( LCDual ‘ 𝐾 ) ‘ 𝑊 ) ) ( ( ( HDMap ‘ 𝐾 ) ‘ 𝑊 ) ‘ 𝑡 ) ) = ( ( ( 𝐺 ‘ 𝑋 ) ( .r ‘ ( Scalar ‘ ( ( LCDual ‘ 𝐾 ) ‘ 𝑊 ) ) ) ( 𝐺 ‘ 𝑌 ) ) ( ·𝑠 ‘ ( ( LCDual ‘ 𝐾 ) ‘ 𝑊 ) ) ( ( ( HDMap ‘ 𝐾 ) ‘ 𝑊 ) ‘ 𝑡 ) ) )
50 eqid ⊢ ( 0g ‘ ( ( LCDual ‘ 𝐾 ) ‘ 𝑊 ) ) = ( 0g ‘ ( ( LCDual ‘ 𝐾 ) ‘ 𝑊 ) )
51 1 13 7 lcdlvec ⊢ ( 𝜑 → ( ( LCDual ‘ 𝐾 ) ‘ 𝑊 ) ∈ LVec )
52 51 3ad2ant1 ⊢ ( ( 𝜑 ∧ 𝑡 ∈ ( Base ‘ 𝑈 ) ∧ 𝑡 ≠ ( 0g ‘ 𝑈 ) ) → ( ( LCDual ‘ 𝐾 ) ‘ 𝑊 ) ∈ LVec )
53 1 2 3 4 13 16 17 6 7 46 hgmapdcl ⊢ ( 𝜑 → ( 𝐺 ‘ ( 𝑋 · 𝑌 ) ) ∈ ( Base ‘ ( Scalar ‘ ( ( LCDual ‘ 𝐾 ) ‘ 𝑊 ) ) ) )
54 53 3ad2ant1 ⊢ ( ( 𝜑 ∧ 𝑡 ∈ ( Base ‘ 𝑈 ) ∧ 𝑡 ≠ ( 0g ‘ 𝑈 ) ) → ( 𝐺 ‘ ( 𝑋 · 𝑌 ) ) ∈ ( Base ‘ ( Scalar ‘ ( ( LCDual ‘ 𝐾 ) ‘ 𝑊 ) ) ) )
55 16 17 28 lmodmcl ⊢ ( ( ( ( LCDual ‘ 𝐾 ) ‘ 𝑊 ) ∈ LMod ∧ ( 𝐺 ‘ 𝑋 ) ∈ ( Base ‘ ( Scalar ‘ ( ( LCDual ‘ 𝐾 ) ‘ 𝑊 ) ) ) ∧ ( 𝐺 ‘ 𝑌 ) ∈ ( Base ‘ ( Scalar ‘ ( ( LCDual ‘ 𝐾 ) ‘ 𝑊 ) ) ) ) → ( ( 𝐺 ‘ 𝑋 ) ( .r ‘ ( Scalar ‘ ( ( LCDual ‘ 𝐾 ) ‘ 𝑊 ) ) ) ( 𝐺 ‘ 𝑌 ) ) ∈ ( Base ‘ ( Scalar ‘ ( ( LCDual ‘ 𝐾 ) ‘ 𝑊 ) ) ) )
56 14 18 20 55 syl3anc ⊢ ( 𝜑 → ( ( 𝐺 ‘ 𝑋 ) ( .r ‘ ( Scalar ‘ ( ( LCDual ‘ 𝐾 ) ‘ 𝑊 ) ) ) ( 𝐺 ‘ 𝑌 ) ) ∈ ( Base ‘ ( Scalar ‘ ( ( LCDual ‘ 𝐾 ) ‘ 𝑊 ) ) ) )
57 56 3ad2ant1 ⊢ ( ( 𝜑 ∧ 𝑡 ∈ ( Base ‘ 𝑈 ) ∧ 𝑡 ≠ ( 0g ‘ 𝑈 ) ) → ( ( 𝐺 ‘ 𝑋 ) ( .r ‘ ( Scalar ‘ ( ( LCDual ‘ 𝐾 ) ‘ 𝑊 ) ) ) ( 𝐺 ‘ 𝑌 ) ) ∈ ( Base ‘ ( Scalar ‘ ( ( LCDual ‘ 𝐾 ) ‘ 𝑊 ) ) ) )
58 simp3 ⊢ ( ( 𝜑 ∧ 𝑡 ∈ ( Base ‘ 𝑈 ) ∧ 𝑡 ≠ ( 0g ‘ 𝑈 ) ) → 𝑡 ≠ ( 0g ‘ 𝑈 ) )
59 1 2 10 11 13 50 23 24 25 hdmapeq0 ⊢ ( ( 𝜑 ∧ 𝑡 ∈ ( Base ‘ 𝑈 ) ∧ 𝑡 ≠ ( 0g ‘ 𝑈 ) ) → ( ( ( ( HDMap ‘ 𝐾 ) ‘ 𝑊 ) ‘ 𝑡 ) = ( 0g ‘ ( ( LCDual ‘ 𝐾 ) ‘ 𝑊 ) ) ↔ 𝑡 = ( 0g ‘ 𝑈 ) ) )
60 59 necon3bid ⊢ ( ( 𝜑 ∧ 𝑡 ∈ ( Base ‘ 𝑈 ) ∧ 𝑡 ≠ ( 0g ‘ 𝑈 ) ) → ( ( ( ( HDMap ‘ 𝐾 ) ‘ 𝑊 ) ‘ 𝑡 ) ≠ ( 0g ‘ ( ( LCDual ‘ 𝐾 ) ‘ 𝑊 ) ) ↔ 𝑡 ≠ ( 0g ‘ 𝑈 ) ) )
61 58 60 mpbird ⊢ ( ( 𝜑 ∧ 𝑡 ∈ ( Base ‘ 𝑈 ) ∧ 𝑡 ≠ ( 0g ‘ 𝑈 ) ) → ( ( ( HDMap ‘ 𝐾 ) ‘ 𝑊 ) ‘ 𝑡 ) ≠ ( 0g ‘ ( ( LCDual ‘ 𝐾 ) ‘ 𝑊 ) ) )
62 22 27 16 17 50 52 54 57 26 61 lvecvscan2 ⊢ ( ( 𝜑 ∧ 𝑡 ∈ ( Base ‘ 𝑈 ) ∧ 𝑡 ≠ ( 0g ‘ 𝑈 ) ) → ( ( ( 𝐺 ‘ ( 𝑋 · 𝑌 ) ) ( ·𝑠 ‘ ( ( LCDual ‘ 𝐾 ) ‘ 𝑊 ) ) ( ( ( HDMap ‘ 𝐾 ) ‘ 𝑊 ) ‘ 𝑡 ) ) = ( ( ( 𝐺 ‘ 𝑋 ) ( .r ‘ ( Scalar ‘ ( ( LCDual ‘ 𝐾 ) ‘ 𝑊 ) ) ) ( 𝐺 ‘ 𝑌 ) ) ( ·𝑠 ‘ ( ( LCDual ‘ 𝐾 ) ‘ 𝑊 ) ) ( ( ( HDMap ‘ 𝐾 ) ‘ 𝑊 ) ‘ 𝑡 ) ) ↔ ( 𝐺 ‘ ( 𝑋 · 𝑌 ) ) = ( ( 𝐺 ‘ 𝑋 ) ( .r ‘ ( Scalar ‘ ( ( LCDual ‘ 𝐾 ) ‘ 𝑊 ) ) ) ( 𝐺 ‘ 𝑌 ) ) ) )
63 49 62 mpbid ⊢ ( ( 𝜑 ∧ 𝑡 ∈ ( Base ‘ 𝑈 ) ∧ 𝑡 ≠ ( 0g ‘ 𝑈 ) ) → ( 𝐺 ‘ ( 𝑋 · 𝑌 ) ) = ( ( 𝐺 ‘ 𝑋 ) ( .r ‘ ( Scalar ‘ ( ( LCDual ‘ 𝐾 ) ‘ 𝑊 ) ) ) ( 𝐺 ‘ 𝑌 ) ) )
64 63 rexlimdv3a ⊢ ( 𝜑 → ( ∃ 𝑡 ∈ ( Base ‘ 𝑈 ) 𝑡 ≠ ( 0g ‘ 𝑈 ) → ( 𝐺 ‘ ( 𝑋 · 𝑌 ) ) = ( ( 𝐺 ‘ 𝑋 ) ( .r ‘ ( Scalar ‘ ( ( LCDual ‘ 𝐾 ) ‘ 𝑊 ) ) ) ( 𝐺 ‘ 𝑌 ) ) ) )
65 12 64 mpd ⊢ ( 𝜑 → ( 𝐺 ‘ ( 𝑋 · 𝑌 ) ) = ( ( 𝐺 ‘ 𝑋 ) ( .r ‘ ( Scalar ‘ ( ( LCDual ‘ 𝐾 ) ‘ 𝑊 ) ) ) ( 𝐺 ‘ 𝑌 ) ) )
66 1 2 3 4 6 7 8 hgmapcl ⊢ ( 𝜑 → ( 𝐺 ‘ 𝑋 ) ∈ 𝐵 )
67 1 2 3 4 6 7 9 hgmapcl ⊢ ( 𝜑 → ( 𝐺 ‘ 𝑌 ) ∈ 𝐵 )
68 1 2 3 4 5 13 16 28 7 66 67 lcdsmul ⊢ ( 𝜑 → ( ( 𝐺 ‘ 𝑋 ) ( .r ‘ ( Scalar ‘ ( ( LCDual ‘ 𝐾 ) ‘ 𝑊 ) ) ) ( 𝐺 ‘ 𝑌 ) ) = ( ( 𝐺 ‘ 𝑌 ) · ( 𝐺 ‘ 𝑋 ) ) )
69 65 68 eqtrd ⊢ ( 𝜑 → ( 𝐺 ‘ ( 𝑋 · 𝑌 ) ) = ( ( 𝐺 ‘ 𝑌 ) · ( 𝐺 ‘ 𝑋 ) ) )