Theorem hgmapvvlem3

Description: Lemma for hgmapvv . Eliminate ( ( SD )C ) = .1. (Baer's f(h,k)=1). (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 } ) )
Assertion	hgmapvvlem3	⊢ ( 𝜑 → ( 𝐺 ‘ ( 𝐺 ‘ 𝑋 ) ) = 𝑋 )

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		eqid	⊢ ( 0g ‘ 𝑈 ) = ( 0g ‘ 𝑈 )
18		eqid	⊢ ( Base ‘ 𝐾 ) = ( Base ‘ 𝐾 )
19		eqid	⊢ ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 ) = ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 )
20	1 18 19 4 5 17 2 15	dvheveccl	⊢ ( 𝜑 → 𝐸 ∈ ( 𝑉 ∖ { ( 0g ‘ 𝑈 ) } ) )
21	20	eldifad	⊢ ( 𝜑 → 𝐸 ∈ 𝑉 )
22	1 3 4 5 17 15 21	dochsnnz	⊢ ( 𝜑 → ( 𝑂 ‘ { 𝐸 } ) ≠ { ( 0g ‘ 𝑈 ) } )
23	21	snssd	⊢ ( 𝜑 → { 𝐸 } ⊆ 𝑉 )
24		eqid	⊢ ( LSubSp ‘ 𝑈 ) = ( LSubSp ‘ 𝑈 )
25	1 4 5 24 3	dochlss	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ { 𝐸 } ⊆ 𝑉 ) → ( 𝑂 ‘ { 𝐸 } ) ∈ ( LSubSp ‘ 𝑈 ) )
26	15 23 25	syl2anc	⊢ ( 𝜑 → ( 𝑂 ‘ { 𝐸 } ) ∈ ( LSubSp ‘ 𝑈 ) )
27	17 24	lssne0	⊢ ( ( 𝑂 ‘ { 𝐸 } ) ∈ ( LSubSp ‘ 𝑈 ) → ( ( 𝑂 ‘ { 𝐸 } ) ≠ { ( 0g ‘ 𝑈 ) } ↔ ∃ 𝑘 ∈ ( 𝑂 ‘ { 𝐸 } ) 𝑘 ≠ ( 0g ‘ 𝑈 ) ) )
28	26 27	syl	⊢ ( 𝜑 → ( ( 𝑂 ‘ { 𝐸 } ) ≠ { ( 0g ‘ 𝑈 ) } ↔ ∃ 𝑘 ∈ ( 𝑂 ‘ { 𝐸 } ) 𝑘 ≠ ( 0g ‘ 𝑈 ) ) )
29	22 28	mpbid	⊢ ( 𝜑 → ∃ 𝑘 ∈ ( 𝑂 ‘ { 𝐸 } ) 𝑘 ≠ ( 0g ‘ 𝑈 ) )
30		eqid	⊢ ( ·𝑠 ‘ 𝑈 ) = ( ·𝑠 ‘ 𝑈 )
31	15	3ad2ant1	⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 𝑂 ‘ { 𝐸 } ) ∧ 𝑘 ≠ ( 0g ‘ 𝑈 ) ) → ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) )
32	1 4 5 3	dochssv	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ { 𝐸 } ⊆ 𝑉 ) → ( 𝑂 ‘ { 𝐸 } ) ⊆ 𝑉 )
33	15 23 32	syl2anc	⊢ ( 𝜑 → ( 𝑂 ‘ { 𝐸 } ) ⊆ 𝑉 )
34	33	sselda	⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 𝑂 ‘ { 𝐸 } ) ) → 𝑘 ∈ 𝑉 )
35	34	3adant3	⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 𝑂 ‘ { 𝐸 } ) ∧ 𝑘 ≠ ( 0g ‘ 𝑈 ) ) → 𝑘 ∈ 𝑉 )
36		simp3	⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 𝑂 ‘ { 𝐸 } ) ∧ 𝑘 ≠ ( 0g ‘ 𝑈 ) ) → 𝑘 ≠ ( 0g ‘ 𝑈 ) )
37		eldifsn	⊢ ( 𝑘 ∈ ( 𝑉 ∖ { ( 0g ‘ 𝑈 ) } ) ↔ ( 𝑘 ∈ 𝑉 ∧ 𝑘 ≠ ( 0g ‘ 𝑈 ) ) )
38	35 36 37	sylanbrc	⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 𝑂 ‘ { 𝐸 } ) ∧ 𝑘 ≠ ( 0g ‘ 𝑈 ) ) → 𝑘 ∈ ( 𝑉 ∖ { ( 0g ‘ 𝑈 ) } ) )
39		eqid	⊢ ( ( 𝑁 ‘ ( ( 𝑆 ‘ 𝑘 ) ‘ 𝑘 ) ) ( ·𝑠 ‘ 𝑈 ) 𝑘 ) = ( ( 𝑁 ‘ ( ( 𝑆 ‘ 𝑘 ) ‘ 𝑘 ) ) ( ·𝑠 ‘ 𝑈 ) 𝑘 )
40	1 4 5 30 17 7 11 12 13 31 38 39	hdmapip1	⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 𝑂 ‘ { 𝐸 } ) ∧ 𝑘 ≠ ( 0g ‘ 𝑈 ) ) → ( ( 𝑆 ‘ 𝑘 ) ‘ ( ( 𝑁 ‘ ( ( 𝑆 ‘ 𝑘 ) ‘ 𝑘 ) ) ( ·𝑠 ‘ 𝑈 ) 𝑘 ) ) = 1 )
41		simpl1	⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ( 𝑂 ‘ { 𝐸 } ) ∧ 𝑘 ≠ ( 0g ‘ 𝑈 ) ) ∧ ( ( 𝑆 ‘ 𝑘 ) ‘ ( ( 𝑁 ‘ ( ( 𝑆 ‘ 𝑘 ) ‘ 𝑘 ) ) ( ·𝑠 ‘ 𝑈 ) 𝑘 ) ) = 1 ) → 𝜑 )
42	41 15	syl	⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ( 𝑂 ‘ { 𝐸 } ) ∧ 𝑘 ≠ ( 0g ‘ 𝑈 ) ) ∧ ( ( 𝑆 ‘ 𝑘 ) ‘ ( ( 𝑁 ‘ ( ( 𝑆 ‘ 𝑘 ) ‘ 𝑘 ) ) ( ·𝑠 ‘ 𝑈 ) 𝑘 ) ) = 1 ) → ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) )
43	41 16	syl	⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ( 𝑂 ‘ { 𝐸 } ) ∧ 𝑘 ≠ ( 0g ‘ 𝑈 ) ) ∧ ( ( 𝑆 ‘ 𝑘 ) ‘ ( ( 𝑁 ‘ ( ( 𝑆 ‘ 𝑘 ) ‘ 𝑘 ) ) ( ·𝑠 ‘ 𝑈 ) 𝑘 ) ) = 1 ) → 𝑋 ∈ ( 𝐵 ∖ { 0 } ) )
44	1 4 15	dvhlmod	⊢ ( 𝜑 → 𝑈 ∈ LMod )
45	41 44	syl	⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ( 𝑂 ‘ { 𝐸 } ) ∧ 𝑘 ≠ ( 0g ‘ 𝑈 ) ) ∧ ( ( 𝑆 ‘ 𝑘 ) ‘ ( ( 𝑁 ‘ ( ( 𝑆 ‘ 𝑘 ) ‘ 𝑘 ) ) ( ·𝑠 ‘ 𝑈 ) 𝑘 ) ) = 1 ) → 𝑈 ∈ LMod )
46	41 26	syl	⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ( 𝑂 ‘ { 𝐸 } ) ∧ 𝑘 ≠ ( 0g ‘ 𝑈 ) ) ∧ ( ( 𝑆 ‘ 𝑘 ) ‘ ( ( 𝑁 ‘ ( ( 𝑆 ‘ 𝑘 ) ‘ 𝑘 ) ) ( ·𝑠 ‘ 𝑈 ) 𝑘 ) ) = 1 ) → ( 𝑂 ‘ { 𝐸 } ) ∈ ( LSubSp ‘ 𝑈 ) )
47	1 4 15	dvhlvec	⊢ ( 𝜑 → 𝑈 ∈ LVec )
48	7	lvecdrng	⊢ ( 𝑈 ∈ LVec → 𝑅 ∈ DivRing )
49	47 48	syl	⊢ ( 𝜑 → 𝑅 ∈ DivRing )
50	41 49	syl	⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ( 𝑂 ‘ { 𝐸 } ) ∧ 𝑘 ≠ ( 0g ‘ 𝑈 ) ) ∧ ( ( 𝑆 ‘ 𝑘 ) ‘ ( ( 𝑁 ‘ ( ( 𝑆 ‘ 𝑘 ) ‘ 𝑘 ) ) ( ·𝑠 ‘ 𝑈 ) 𝑘 ) ) = 1 ) → 𝑅 ∈ DivRing )
51	35	adantr	⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ( 𝑂 ‘ { 𝐸 } ) ∧ 𝑘 ≠ ( 0g ‘ 𝑈 ) ) ∧ ( ( 𝑆 ‘ 𝑘 ) ‘ ( ( 𝑁 ‘ ( ( 𝑆 ‘ 𝑘 ) ‘ 𝑘 ) ) ( ·𝑠 ‘ 𝑈 ) 𝑘 ) ) = 1 ) → 𝑘 ∈ 𝑉 )
52	1 4 5 7 8 13 42 51 51	hdmapipcl	⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ( 𝑂 ‘ { 𝐸 } ) ∧ 𝑘 ≠ ( 0g ‘ 𝑈 ) ) ∧ ( ( 𝑆 ‘ 𝑘 ) ‘ ( ( 𝑁 ‘ ( ( 𝑆 ‘ 𝑘 ) ‘ 𝑘 ) ) ( ·𝑠 ‘ 𝑈 ) 𝑘 ) ) = 1 ) → ( ( 𝑆 ‘ 𝑘 ) ‘ 𝑘 ) ∈ 𝐵 )
53	15	adantr	⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 𝑂 ‘ { 𝐸 } ) ) → ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) )
54	1 4 5 17 7 10 13 53 34	hdmapip0	⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 𝑂 ‘ { 𝐸 } ) ) → ( ( ( 𝑆 ‘ 𝑘 ) ‘ 𝑘 ) = 0 ↔ 𝑘 = ( 0g ‘ 𝑈 ) ) )
55	54	necon3bid	⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 𝑂 ‘ { 𝐸 } ) ) → ( ( ( 𝑆 ‘ 𝑘 ) ‘ 𝑘 ) ≠ 0 ↔ 𝑘 ≠ ( 0g ‘ 𝑈 ) ) )
56	55	biimp3ar	⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 𝑂 ‘ { 𝐸 } ) ∧ 𝑘 ≠ ( 0g ‘ 𝑈 ) ) → ( ( 𝑆 ‘ 𝑘 ) ‘ 𝑘 ) ≠ 0 )
57	56	adantr	⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ( 𝑂 ‘ { 𝐸 } ) ∧ 𝑘 ≠ ( 0g ‘ 𝑈 ) ) ∧ ( ( 𝑆 ‘ 𝑘 ) ‘ ( ( 𝑁 ‘ ( ( 𝑆 ‘ 𝑘 ) ‘ 𝑘 ) ) ( ·𝑠 ‘ 𝑈 ) 𝑘 ) ) = 1 ) → ( ( 𝑆 ‘ 𝑘 ) ‘ 𝑘 ) ≠ 0 )
58	8 10 12	drnginvrcl	⊢ ( ( 𝑅 ∈ DivRing ∧ ( ( 𝑆 ‘ 𝑘 ) ‘ 𝑘 ) ∈ 𝐵 ∧ ( ( 𝑆 ‘ 𝑘 ) ‘ 𝑘 ) ≠ 0 ) → ( 𝑁 ‘ ( ( 𝑆 ‘ 𝑘 ) ‘ 𝑘 ) ) ∈ 𝐵 )
59	50 52 57 58	syl3anc	⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ( 𝑂 ‘ { 𝐸 } ) ∧ 𝑘 ≠ ( 0g ‘ 𝑈 ) ) ∧ ( ( 𝑆 ‘ 𝑘 ) ‘ ( ( 𝑁 ‘ ( ( 𝑆 ‘ 𝑘 ) ‘ 𝑘 ) ) ( ·𝑠 ‘ 𝑈 ) 𝑘 ) ) = 1 ) → ( 𝑁 ‘ ( ( 𝑆 ‘ 𝑘 ) ‘ 𝑘 ) ) ∈ 𝐵 )
60		simpl2	⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ( 𝑂 ‘ { 𝐸 } ) ∧ 𝑘 ≠ ( 0g ‘ 𝑈 ) ) ∧ ( ( 𝑆 ‘ 𝑘 ) ‘ ( ( 𝑁 ‘ ( ( 𝑆 ‘ 𝑘 ) ‘ 𝑘 ) ) ( ·𝑠 ‘ 𝑈 ) 𝑘 ) ) = 1 ) → 𝑘 ∈ ( 𝑂 ‘ { 𝐸 } ) )
61	7 30 8 24	lssvscl	⊢ ( ( ( 𝑈 ∈ LMod ∧ ( 𝑂 ‘ { 𝐸 } ) ∈ ( LSubSp ‘ 𝑈 ) ) ∧ ( ( 𝑁 ‘ ( ( 𝑆 ‘ 𝑘 ) ‘ 𝑘 ) ) ∈ 𝐵 ∧ 𝑘 ∈ ( 𝑂 ‘ { 𝐸 } ) ) ) → ( ( 𝑁 ‘ ( ( 𝑆 ‘ 𝑘 ) ‘ 𝑘 ) ) ( ·𝑠 ‘ 𝑈 ) 𝑘 ) ∈ ( 𝑂 ‘ { 𝐸 } ) )
62	45 46 59 60 61	syl22anc	⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ( 𝑂 ‘ { 𝐸 } ) ∧ 𝑘 ≠ ( 0g ‘ 𝑈 ) ) ∧ ( ( 𝑆 ‘ 𝑘 ) ‘ ( ( 𝑁 ‘ ( ( 𝑆 ‘ 𝑘 ) ‘ 𝑘 ) ) ( ·𝑠 ‘ 𝑈 ) 𝑘 ) ) = 1 ) → ( ( 𝑁 ‘ ( ( 𝑆 ‘ 𝑘 ) ‘ 𝑘 ) ) ( ·𝑠 ‘ 𝑈 ) 𝑘 ) ∈ ( 𝑂 ‘ { 𝐸 } ) )
63		simpr	⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ( 𝑂 ‘ { 𝐸 } ) ∧ 𝑘 ≠ ( 0g ‘ 𝑈 ) ) ∧ ( ( 𝑆 ‘ 𝑘 ) ‘ ( ( 𝑁 ‘ ( ( 𝑆 ‘ 𝑘 ) ‘ 𝑘 ) ) ( ·𝑠 ‘ 𝑈 ) 𝑘 ) ) = 1 ) → ( ( 𝑆 ‘ 𝑘 ) ‘ ( ( 𝑁 ‘ ( ( 𝑆 ‘ 𝑘 ) ‘ 𝑘 ) ) ( ·𝑠 ‘ 𝑈 ) 𝑘 ) ) = 1 )
64	1 2 3 4 5 6 7 8 9 10 11 12 13 14 42 43 62 60 63	hgmapvvlem2	⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ( 𝑂 ‘ { 𝐸 } ) ∧ 𝑘 ≠ ( 0g ‘ 𝑈 ) ) ∧ ( ( 𝑆 ‘ 𝑘 ) ‘ ( ( 𝑁 ‘ ( ( 𝑆 ‘ 𝑘 ) ‘ 𝑘 ) ) ( ·𝑠 ‘ 𝑈 ) 𝑘 ) ) = 1 ) → ( 𝐺 ‘ ( 𝐺 ‘ 𝑋 ) ) = 𝑋 )
65	40 64	mpdan	⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 𝑂 ‘ { 𝐸 } ) ∧ 𝑘 ≠ ( 0g ‘ 𝑈 ) ) → ( 𝐺 ‘ ( 𝐺 ‘ 𝑋 ) ) = 𝑋 )
66	65	rexlimdv3a	⊢ ( 𝜑 → ( ∃ 𝑘 ∈ ( 𝑂 ‘ { 𝐸 } ) 𝑘 ≠ ( 0g ‘ 𝑈 ) → ( 𝐺 ‘ ( 𝐺 ‘ 𝑋 ) ) = 𝑋 ) )
67	29 66	mpd	⊢ ( 𝜑 → ( 𝐺 ‘ ( 𝐺 ‘ 𝑋 ) ) = 𝑋 )