Metamath Proof Explorer

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