Metamath Proof Explorer

Theorem hdmapglem5

Description: Part 1.2 in Baer p. 110 line 34, f(u,v) alpha = f(v,u). (Contributed by NM, 12-Jun-2015)

Ref Expression
Hypotheses hdmapglem5.h ⊢ 𝐻 = ( LHyp ‘ 𝐾 )
hdmapglem5.e ⊢ 𝐸 = ⟨ ( I ↾ ( Base ‘ 𝐾 ) ) , ( I ↾ ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 ) ) ⟩
hdmapglem5.o ⊢ 𝑂 = ( ( ocH ‘ 𝐾 ) ‘ 𝑊 )
hdmapglem5.u ⊢ 𝑈 = ( ( DVecH ‘ 𝐾 ) ‘ 𝑊 )
hdmapglem5.v ⊢ 𝑉 = ( Base ‘ 𝑈 )
hdmapglem5.p ⊢ + = ( +g ‘ 𝑈 )
hdmapglem5.m ⊢ − = ( -g ‘ 𝑈 )
hdmapglem5.q ⊢ · = ( ·𝑠 ‘ 𝑈 )
hdmapglem5.r ⊢ 𝑅 = ( Scalar ‘ 𝑈 )
hdmapglem5.b ⊢ 𝐵 = ( Base ‘ 𝑅 )
hdmapglem5.t ⊢ × = ( .r ‘ 𝑅 )
hdmapglem5.z ⊢ 0 = ( 0g ‘ 𝑅 )
hdmapglem5.s ⊢ 𝑆 = ( ( HDMap ‘ 𝐾 ) ‘ 𝑊 )
hdmapglem5.g ⊢ 𝐺 = ( ( HGMap ‘ 𝐾 ) ‘ 𝑊 )
hdmapglem5.k ⊢ ( 𝜑 → ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) )
hdmapglem5.c ⊢ ( 𝜑 → 𝐶 ∈ ( 𝑂 ‘ { 𝐸 } ) )
hdmapglem5.d ⊢ ( 𝜑 → 𝐷 ∈ ( 𝑂 ‘ { 𝐸 } ) )
hdmapglem5.i ⊢ ( 𝜑 → 𝐼 ∈ 𝐵 )
hdmapglem5.j ⊢ ( 𝜑 → 𝐽 ∈ 𝐵 )
Assertion hdmapglem5 ( 𝜑 → ( 𝐺 ‘ ( ( 𝑆 ‘ 𝐷 ) ‘ 𝐶 ) ) = ( ( 𝑆 ‘ 𝐶 ) ‘ 𝐷 ) )

Proof

Step Hyp Ref Expression
1 hdmapglem5.h ⊢ 𝐻 = ( LHyp ‘ 𝐾 )
2 hdmapglem5.e ⊢ 𝐸 = ⟨ ( I ↾ ( Base ‘ 𝐾 ) ) , ( I ↾ ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 ) ) ⟩
3 hdmapglem5.o ⊢ 𝑂 = ( ( ocH ‘ 𝐾 ) ‘ 𝑊 )
4 hdmapglem5.u ⊢ 𝑈 = ( ( DVecH ‘ 𝐾 ) ‘ 𝑊 )
5 hdmapglem5.v ⊢ 𝑉 = ( Base ‘ 𝑈 )
6 hdmapglem5.p ⊢ + = ( +g ‘ 𝑈 )
7 hdmapglem5.m ⊢ − = ( -g ‘ 𝑈 )
8 hdmapglem5.q ⊢ · = ( ·𝑠 ‘ 𝑈 )
9 hdmapglem5.r ⊢ 𝑅 = ( Scalar ‘ 𝑈 )
10 hdmapglem5.b ⊢ 𝐵 = ( Base ‘ 𝑅 )
11 hdmapglem5.t ⊢ × = ( .r ‘ 𝑅 )
12 hdmapglem5.z ⊢ 0 = ( 0g ‘ 𝑅 )
13 hdmapglem5.s ⊢ 𝑆 = ( ( HDMap ‘ 𝐾 ) ‘ 𝑊 )
14 hdmapglem5.g ⊢ 𝐺 = ( ( HGMap ‘ 𝐾 ) ‘ 𝑊 )
15 hdmapglem5.k ⊢ ( 𝜑 → ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) )
16 hdmapglem5.c ⊢ ( 𝜑 → 𝐶 ∈ ( 𝑂 ‘ { 𝐸 } ) )
17 hdmapglem5.d ⊢ ( 𝜑 → 𝐷 ∈ ( 𝑂 ‘ { 𝐸 } ) )
18 hdmapglem5.i ⊢ ( 𝜑 → 𝐼 ∈ 𝐵 )
19 hdmapglem5.j ⊢ ( 𝜑 → 𝐽 ∈ 𝐵 )
20 1 4 15 dvhlmod ⊢ ( 𝜑 → 𝑈 ∈ LMod )
21 9 lmodring ⊢ ( 𝑈 ∈ LMod → 𝑅 ∈ Ring )
22 20 21 syl ⊢ ( 𝜑 → 𝑅 ∈ Ring )
23 eqid ⊢ ( Base ‘ 𝐾 ) = ( Base ‘ 𝐾 )
24 eqid ⊢ ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 ) = ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 )
25 eqid ⊢ ( 0g ‘ 𝑈 ) = ( 0g ‘ 𝑈 )
26 1 23 24 4 5 25 2 15 dvheveccl ⊢ ( 𝜑 → 𝐸 ∈ ( 𝑉 ∖ { ( 0g ‘ 𝑈 ) } ) )
27 26 eldifad ⊢ ( 𝜑 → 𝐸 ∈ 𝑉 )
28 27 snssd ⊢ ( 𝜑 → { 𝐸 } ⊆ 𝑉 )
29 1 4 5 3 dochssv ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ { 𝐸 } ⊆ 𝑉 ) → ( 𝑂 ‘ { 𝐸 } ) ⊆ 𝑉 )
30 15 28 29 syl2anc ⊢ ( 𝜑 → ( 𝑂 ‘ { 𝐸 } ) ⊆ 𝑉 )
31 30 16 sseldd ⊢ ( 𝜑 → 𝐶 ∈ 𝑉 )
32 30 17 sseldd ⊢ ( 𝜑 → 𝐷 ∈ 𝑉 )
33 1 4 5 9 10 13 15 31 32 hdmapipcl ⊢ ( 𝜑 → ( ( 𝑆 ‘ 𝐷 ) ‘ 𝐶 ) ∈ 𝐵 )
34 1 4 9 10 14 15 33 hgmapcl ⊢ ( 𝜑 → ( 𝐺 ‘ ( ( 𝑆 ‘ 𝐷 ) ‘ 𝐶 ) ) ∈ 𝐵 )
35 eqid ⊢ ( 1r ‘ 𝑅 ) = ( 1r ‘ 𝑅 )
36 10 11 35 ringlidm ⊢ ( ( 𝑅 ∈ Ring ∧ ( 𝐺 ‘ ( ( 𝑆 ‘ 𝐷 ) ‘ 𝐶 ) ) ∈ 𝐵 ) → ( ( 1r ‘ 𝑅 ) × ( 𝐺 ‘ ( ( 𝑆 ‘ 𝐷 ) ‘ 𝐶 ) ) ) = ( 𝐺 ‘ ( ( 𝑆 ‘ 𝐷 ) ‘ 𝐶 ) ) )
37 22 34 36 syl2anc ⊢ ( 𝜑 → ( ( 1r ‘ 𝑅 ) × ( 𝐺 ‘ ( ( 𝑆 ‘ 𝐷 ) ‘ 𝐶 ) ) ) = ( 𝐺 ‘ ( ( 𝑆 ‘ 𝐷 ) ‘ 𝐶 ) ) )
38 10 35 ringidcl ⊢ ( 𝑅 ∈ Ring → ( 1r ‘ 𝑅 ) ∈ 𝐵 )
39 22 38 syl ⊢ ( 𝜑 → ( 1r ‘ 𝑅 ) ∈ 𝐵 )
40 1 4 9 35 14 15 hgmapval1 ⊢ ( 𝜑 → ( 𝐺 ‘ ( 1r ‘ 𝑅 ) ) = ( 1r ‘ 𝑅 ) )
41 40 oveq2d ⊢ ( 𝜑 → ( ( ( 𝑆 ‘ 𝐷 ) ‘ 𝐶 ) × ( 𝐺 ‘ ( 1r ‘ 𝑅 ) ) ) = ( ( ( 𝑆 ‘ 𝐷 ) ‘ 𝐶 ) × ( 1r ‘ 𝑅 ) ) )
42 10 11 35 ringridm ⊢ ( ( 𝑅 ∈ Ring ∧ ( ( 𝑆 ‘ 𝐷 ) ‘ 𝐶 ) ∈ 𝐵 ) → ( ( ( 𝑆 ‘ 𝐷 ) ‘ 𝐶 ) × ( 1r ‘ 𝑅 ) ) = ( ( 𝑆 ‘ 𝐷 ) ‘ 𝐶 ) )
43 22 33 42 syl2anc ⊢ ( 𝜑 → ( ( ( 𝑆 ‘ 𝐷 ) ‘ 𝐶 ) × ( 1r ‘ 𝑅 ) ) = ( ( 𝑆 ‘ 𝐷 ) ‘ 𝐶 ) )
44 41 43 eqtrd ⊢ ( 𝜑 → ( ( ( 𝑆 ‘ 𝐷 ) ‘ 𝐶 ) × ( 𝐺 ‘ ( 1r ‘ 𝑅 ) ) ) = ( ( 𝑆 ‘ 𝐷 ) ‘ 𝐶 ) )
45 1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 33 39 44 hdmapinvlem4 ⊢ ( 𝜑 → ( ( 1r ‘ 𝑅 ) × ( 𝐺 ‘ ( ( 𝑆 ‘ 𝐷 ) ‘ 𝐶 ) ) ) = ( ( 𝑆 ‘ 𝐶 ) ‘ 𝐷 ) )
46 37 45 eqtr3d ⊢ ( 𝜑 → ( 𝐺 ‘ ( ( 𝑆 ‘ 𝐷 ) ‘ 𝐶 ) ) = ( ( 𝑆 ‘ 𝐶 ) ‘ 𝐷 ) )