Metamath Proof Explorer

Theorem hgmapvvlem2

Description: Lemma for hgmapvv . Eliminate Y (Baer's s). (Contributed by NM, 13-Jun-2015)

Ref Expression
Hypotheses hdmapglem6.h ⊢ 𝐻 = ( LHyp ‘ 𝐾 )
hdmapglem6.e ⊢ 𝐸 = ⟨ ( I ↾ ( Base ‘ 𝐾 ) ) , ( I ↾ ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 ) ) ⟩
hdmapglem6.o ⊢ 𝑂 = ( ( ocH ‘ 𝐾 ) ‘ 𝑊 )
hdmapglem6.u ⊢ 𝑈 = ( ( DVecH ‘ 𝐾 ) ‘ 𝑊 )
hdmapglem6.v ⊢ 𝑉 = ( Base ‘ 𝑈 )
hdmapglem6.q ⊢ · = ( ·𝑠 ‘ 𝑈 )
hdmapglem6.r ⊢ 𝑅 = ( Scalar ‘ 𝑈 )
hdmapglem6.b ⊢ 𝐵 = ( Base ‘ 𝑅 )
hdmapglem6.t ⊢ × = ( .r ‘ 𝑅 )
hdmapglem6.z ⊢ 0 = ( 0g ‘ 𝑅 )
hdmapglem6.i ⊢ 1 = ( 1r ‘ 𝑅 )
hdmapglem6.n ⊢ 𝑁 = ( invr ‘ 𝑅 )
hdmapglem6.s ⊢ 𝑆 = ( ( HDMap ‘ 𝐾 ) ‘ 𝑊 )
hdmapglem6.g ⊢ 𝐺 = ( ( HGMap ‘ 𝐾 ) ‘ 𝑊 )
hdmapglem6.k ⊢ ( 𝜑 → ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) )
hdmapglem6.x ⊢ ( 𝜑 → 𝑋 ∈ ( 𝐵 ∖ { 0 } ) )
hdmapglem6.c ⊢ ( 𝜑 → 𝐶 ∈ ( 𝑂 ‘ { 𝐸 } ) )
hdmapglem6.d ⊢ ( 𝜑 → 𝐷 ∈ ( 𝑂 ‘ { 𝐸 } ) )
hdmapglem6.cd ⊢ ( 𝜑 → ( ( 𝑆 ‘ 𝐷 ) ‘ 𝐶 ) = 1 )
Assertion hgmapvvlem2 ( 𝜑 → ( 𝐺 ‘ ( 𝐺 ‘ 𝑋 ) ) = 𝑋 )

Proof

Step Hyp Ref Expression
1 hdmapglem6.h ⊢ 𝐻 = ( LHyp ‘ 𝐾 )
2 hdmapglem6.e ⊢ 𝐸 = ⟨ ( I ↾ ( Base ‘ 𝐾 ) ) , ( I ↾ ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 ) ) ⟩
3 hdmapglem6.o ⊢ 𝑂 = ( ( ocH ‘ 𝐾 ) ‘ 𝑊 )
4 hdmapglem6.u ⊢ 𝑈 = ( ( DVecH ‘ 𝐾 ) ‘ 𝑊 )
5 hdmapglem6.v ⊢ 𝑉 = ( Base ‘ 𝑈 )
6 hdmapglem6.q ⊢ · = ( ·𝑠 ‘ 𝑈 )
7 hdmapglem6.r ⊢ 𝑅 = ( Scalar ‘ 𝑈 )
8 hdmapglem6.b ⊢ 𝐵 = ( Base ‘ 𝑅 )
9 hdmapglem6.t ⊢ × = ( .r ‘ 𝑅 )
10 hdmapglem6.z ⊢ 0 = ( 0g ‘ 𝑅 )
11 hdmapglem6.i ⊢ 1 = ( 1r ‘ 𝑅 )
12 hdmapglem6.n ⊢ 𝑁 = ( invr ‘ 𝑅 )
13 hdmapglem6.s ⊢ 𝑆 = ( ( HDMap ‘ 𝐾 ) ‘ 𝑊 )
14 hdmapglem6.g ⊢ 𝐺 = ( ( HGMap ‘ 𝐾 ) ‘ 𝑊 )
15 hdmapglem6.k ⊢ ( 𝜑 → ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) )
16 hdmapglem6.x ⊢ ( 𝜑 → 𝑋 ∈ ( 𝐵 ∖ { 0 } ) )
17 hdmapglem6.c ⊢ ( 𝜑 → 𝐶 ∈ ( 𝑂 ‘ { 𝐸 } ) )
18 hdmapglem6.d ⊢ ( 𝜑 → 𝐷 ∈ ( 𝑂 ‘ { 𝐸 } ) )
19 hdmapglem6.cd ⊢ ( 𝜑 → ( ( 𝑆 ‘ 𝐷 ) ‘ 𝐶 ) = 1 )
20 1 4 15 dvhlvec ⊢ ( 𝜑 → 𝑈 ∈ LVec )
21 7 lvecdrng ⊢ ( 𝑈 ∈ LVec → 𝑅 ∈ DivRing )
22 20 21 syl ⊢ ( 𝜑 → 𝑅 ∈ DivRing )
23 16 eldifad ⊢ ( 𝜑 → 𝑋 ∈ 𝐵 )
24 1 4 7 8 14 15 23 hgmapcl ⊢ ( 𝜑 → ( 𝐺 ‘ 𝑋 ) ∈ 𝐵 )
25 eldifsni ⊢ ( 𝑋 ∈ ( 𝐵 ∖ { 0 } ) → 𝑋 ≠ 0 )
26 16 25 syl ⊢ ( 𝜑 → 𝑋 ≠ 0 )
27 1 4 7 8 10 14 15 23 hgmapeq0 ⊢ ( 𝜑 → ( ( 𝐺 ‘ 𝑋 ) = 0 ↔ 𝑋 = 0 ) )
28 27 necon3bid ⊢ ( 𝜑 → ( ( 𝐺 ‘ 𝑋 ) ≠ 0 ↔ 𝑋 ≠ 0 ) )
29 26 28 mpbird ⊢ ( 𝜑 → ( 𝐺 ‘ 𝑋 ) ≠ 0 )
30 8 10 12 drnginvrcl ⊢ ( ( 𝑅 ∈ DivRing ∧ ( 𝐺 ‘ 𝑋 ) ∈ 𝐵 ∧ ( 𝐺 ‘ 𝑋 ) ≠ 0 ) → ( 𝑁 ‘ ( 𝐺 ‘ 𝑋 ) ) ∈ 𝐵 )
31 22 24 29 30 syl3anc ⊢ ( 𝜑 → ( 𝑁 ‘ ( 𝐺 ‘ 𝑋 ) ) ∈ 𝐵 )
32 8 10 12 drnginvrn0 ⊢ ( ( 𝑅 ∈ DivRing ∧ ( 𝐺 ‘ 𝑋 ) ∈ 𝐵 ∧ ( 𝐺 ‘ 𝑋 ) ≠ 0 ) → ( 𝑁 ‘ ( 𝐺 ‘ 𝑋 ) ) ≠ 0 )
33 22 24 29 32 syl3anc ⊢ ( 𝜑 → ( 𝑁 ‘ ( 𝐺 ‘ 𝑋 ) ) ≠ 0 )
34 eldifsn ⊢ ( ( 𝑁 ‘ ( 𝐺 ‘ 𝑋 ) ) ∈ ( 𝐵 ∖ { 0 } ) ↔ ( ( 𝑁 ‘ ( 𝐺 ‘ 𝑋 ) ) ∈ 𝐵 ∧ ( 𝑁 ‘ ( 𝐺 ‘ 𝑋 ) ) ≠ 0 ) )
35 31 33 34 sylanbrc ⊢ ( 𝜑 → ( 𝑁 ‘ ( 𝐺 ‘ 𝑋 ) ) ∈ ( 𝐵 ∖ { 0 } ) )
36 8 10 9 11 12 drnginvrl ⊢ ( ( 𝑅 ∈ DivRing ∧ ( 𝐺 ‘ 𝑋 ) ∈ 𝐵 ∧ ( 𝐺 ‘ 𝑋 ) ≠ 0 ) → ( ( 𝑁 ‘ ( 𝐺 ‘ 𝑋 ) ) × ( 𝐺 ‘ 𝑋 ) ) = 1 )
37 22 24 29 36 syl3anc ⊢ ( 𝜑 → ( ( 𝑁 ‘ ( 𝐺 ‘ 𝑋 ) ) × ( 𝐺 ‘ 𝑋 ) ) = 1 )
38 1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 35 37 hgmapvvlem1 ⊢ ( 𝜑 → ( 𝐺 ‘ ( 𝐺 ‘ 𝑋 ) ) = 𝑋 )