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 = ( 0_g ‘ 𝑅 )
	hdmapglem6.i	⊢ 1 = ( 1_r ‘ 𝑅 )
	hdmapglem6.n	⊢ 𝑁 = ( inv_r ‘ 𝑅 )
	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 = ( 0_g ‘ 𝑅 )
11		hdmapglem6.i	⊢ 1 = ( 1_r ‘ 𝑅 )
12		hdmapglem6.n	⊢ 𝑁 = ( inv_r ‘ 𝑅 )
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	⊢ ( 𝜑 → ( 𝐺 ‘ ( 𝐺 ‘ 𝑋 ) ) = 𝑋 )

Metamath Proof Explorer

Theorem hgmapvvlem2

Proof