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 ( 𝜑 → ( 𝐺 ‘ ( 𝑋 · 𝑌 ) ) = ( ( 𝐺𝑌 ) · ( 𝐺𝑋 ) ) )