This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem dochkr1

Description: A nonzero functional has a value of 1 at some argument belonging to the orthocomplement of its kernel (when its kernel is a closed hyperplane). Tighter version of lfl1 . (Contributed by NM, 2-Jan-2015)

Ref Expression
Hypotheses dochkr1.h ⊢ 𝐻 = ( LHyp ‘ 𝐾 )
dochkr1.o ⊢ ⊥ = ( ( ocH ‘ 𝐾 ) ‘ 𝑊 )
dochkr1.u ⊢ 𝑈 = ( ( DVecH ‘ 𝐾 ) ‘ 𝑊 )
dochkr1.v ⊢ 𝑉 = ( Base ‘ 𝑈 )
dochkr1.r ⊢ 𝑅 = ( Scalar ‘ 𝑈 )
dochkr1.z ⊢ 0 = ( 0g ‘ 𝑈 )
dochkr1.i ⊢ 1 = ( 1r ‘ 𝑅 )
dochkr1.f ⊢ 𝐹 = ( LFnl ‘ 𝑈 )
dochkr1.l ⊢ 𝐿 = ( LKer ‘ 𝑈 )
dochkr1.k ⊢ ( 𝜑 → ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) )
dochkr1.g ⊢ ( 𝜑 → 𝐺 ∈ 𝐹 )
dochkr1.n ⊢ ( 𝜑 → ( ⊥ ‘ ( ⊥ ‘ ( 𝐿 ‘ 𝐺 ) ) ) ≠ 𝑉 )
Assertion dochkr1 ( 𝜑 → ∃ 𝑥 ∈ ( ( ⊥ ‘ ( 𝐿 ‘ 𝐺 ) ) ∖ { 0 } ) ( 𝐺 ‘ 𝑥 ) = 1 )

Proof

Step Hyp Ref Expression
1 dochkr1.h ⊢ 𝐻 = ( LHyp ‘ 𝐾 )
2 dochkr1.o ⊢ ⊥ = ( ( ocH ‘ 𝐾 ) ‘ 𝑊 )
3 dochkr1.u ⊢ 𝑈 = ( ( DVecH ‘ 𝐾 ) ‘ 𝑊 )
4 dochkr1.v ⊢ 𝑉 = ( Base ‘ 𝑈 )
5 dochkr1.r ⊢ 𝑅 = ( Scalar ‘ 𝑈 )
6 dochkr1.z ⊢ 0 = ( 0g ‘ 𝑈 )
7 dochkr1.i ⊢ 1 = ( 1r ‘ 𝑅 )
8 dochkr1.f ⊢ 𝐹 = ( LFnl ‘ 𝑈 )
9 dochkr1.l ⊢ 𝐿 = ( LKer ‘ 𝑈 )
10 dochkr1.k ⊢ ( 𝜑 → ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) )
11 dochkr1.g ⊢ ( 𝜑 → 𝐺 ∈ 𝐹 )
12 dochkr1.n ⊢ ( 𝜑 → ( ⊥ ‘ ( ⊥ ‘ ( 𝐿 ‘ 𝐺 ) ) ) ≠ 𝑉 )
13 eqid ⊢ ( 0g ‘ 𝑈 ) = ( 0g ‘ 𝑈 )
14 eqid ⊢ ( LSAtoms ‘ 𝑈 ) = ( LSAtoms ‘ 𝑈 )
15 1 3 10 dvhlmod ⊢ ( 𝜑 → 𝑈 ∈ LMod )
16 1 2 3 4 14 8 9 10 11 dochkrsat2 ⊢ ( 𝜑 → ( ( ⊥ ‘ ( ⊥ ‘ ( 𝐿 ‘ 𝐺 ) ) ) ≠ 𝑉 ↔ ( ⊥ ‘ ( 𝐿 ‘ 𝐺 ) ) ∈ ( LSAtoms ‘ 𝑈 ) ) )
17 12 16 mpbid ⊢ ( 𝜑 → ( ⊥ ‘ ( 𝐿 ‘ 𝐺 ) ) ∈ ( LSAtoms ‘ 𝑈 ) )
18 13 14 15 17 lsateln0 ⊢ ( 𝜑 → ∃ 𝑧 ∈ ( ⊥ ‘ ( 𝐿 ‘ 𝐺 ) ) 𝑧 ≠ ( 0g ‘ 𝑈 ) )
19 eqid ⊢ ( 0g ‘ 𝑅 ) = ( 0g ‘ 𝑅 )
20 10 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ ( ⊥ ‘ ( 𝐿 ‘ 𝐺 ) ) ) ∧ 𝑧 ≠ ( 0g ‘ 𝑈 ) ) → ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) )
21 11 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ ( ⊥ ‘ ( 𝐿 ‘ 𝐺 ) ) ) ∧ 𝑧 ≠ ( 0g ‘ 𝑈 ) ) → 𝐺 ∈ 𝐹 )
22 eldifsn ⊢ ( 𝑧 ∈ ( ( ⊥ ‘ ( 𝐿 ‘ 𝐺 ) ) ∖ { ( 0g ‘ 𝑈 ) } ) ↔ ( 𝑧 ∈ ( ⊥ ‘ ( 𝐿 ‘ 𝐺 ) ) ∧ 𝑧 ≠ ( 0g ‘ 𝑈 ) ) )
23 22 biimpri ⊢ ( ( 𝑧 ∈ ( ⊥ ‘ ( 𝐿 ‘ 𝐺 ) ) ∧ 𝑧 ≠ ( 0g ‘ 𝑈 ) ) → 𝑧 ∈ ( ( ⊥ ‘ ( 𝐿 ‘ 𝐺 ) ) ∖ { ( 0g ‘ 𝑈 ) } ) )
24 23 adantll ⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ ( ⊥ ‘ ( 𝐿 ‘ 𝐺 ) ) ) ∧ 𝑧 ≠ ( 0g ‘ 𝑈 ) ) → 𝑧 ∈ ( ( ⊥ ‘ ( 𝐿 ‘ 𝐺 ) ) ∖ { ( 0g ‘ 𝑈 ) } ) )
25 1 2 3 4 5 19 13 8 9 20 21 24 dochfln0 ⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ ( ⊥ ‘ ( 𝐿 ‘ 𝐺 ) ) ) ∧ 𝑧 ≠ ( 0g ‘ 𝑈 ) ) → ( 𝐺 ‘ 𝑧 ) ≠ ( 0g ‘ 𝑅 ) )
26 25 ex ⊢ ( ( 𝜑 ∧ 𝑧 ∈ ( ⊥ ‘ ( 𝐿 ‘ 𝐺 ) ) ) → ( 𝑧 ≠ ( 0g ‘ 𝑈 ) → ( 𝐺 ‘ 𝑧 ) ≠ ( 0g ‘ 𝑅 ) ) )
27 26 reximdva ⊢ ( 𝜑 → ( ∃ 𝑧 ∈ ( ⊥ ‘ ( 𝐿 ‘ 𝐺 ) ) 𝑧 ≠ ( 0g ‘ 𝑈 ) → ∃ 𝑧 ∈ ( ⊥ ‘ ( 𝐿 ‘ 𝐺 ) ) ( 𝐺 ‘ 𝑧 ) ≠ ( 0g ‘ 𝑅 ) ) )
28 18 27 mpd ⊢ ( 𝜑 → ∃ 𝑧 ∈ ( ⊥ ‘ ( 𝐿 ‘ 𝐺 ) ) ( 𝐺 ‘ 𝑧 ) ≠ ( 0g ‘ 𝑅 ) )
29 4 8 9 15 11 lkrssv ⊢ ( 𝜑 → ( 𝐿 ‘ 𝐺 ) ⊆ 𝑉 )
30 eqid ⊢ ( LSubSp ‘ 𝑈 ) = ( LSubSp ‘ 𝑈 )
31 1 3 4 30 2 dochlss ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝐿 ‘ 𝐺 ) ⊆ 𝑉 ) → ( ⊥ ‘ ( 𝐿 ‘ 𝐺 ) ) ∈ ( LSubSp ‘ 𝑈 ) )
32 10 29 31 syl2anc ⊢ ( 𝜑 → ( ⊥ ‘ ( 𝐿 ‘ 𝐺 ) ) ∈ ( LSubSp ‘ 𝑈 ) )
33 15 32 jca ⊢ ( 𝜑 → ( 𝑈 ∈ LMod ∧ ( ⊥ ‘ ( 𝐿 ‘ 𝐺 ) ) ∈ ( LSubSp ‘ 𝑈 ) ) )
34 33 3ad2ant1 ⊢ ( ( 𝜑 ∧ 𝑧 ∈ ( ⊥ ‘ ( 𝐿 ‘ 𝐺 ) ) ∧ ( 𝐺 ‘ 𝑧 ) ≠ ( 0g ‘ 𝑅 ) ) → ( 𝑈 ∈ LMod ∧ ( ⊥ ‘ ( 𝐿 ‘ 𝐺 ) ) ∈ ( LSubSp ‘ 𝑈 ) ) )
35 1 3 10 dvhlvec ⊢ ( 𝜑 → 𝑈 ∈ LVec )
36 35 3ad2ant1 ⊢ ( ( 𝜑 ∧ 𝑧 ∈ ( ⊥ ‘ ( 𝐿 ‘ 𝐺 ) ) ∧ ( 𝐺 ‘ 𝑧 ) ≠ ( 0g ‘ 𝑅 ) ) → 𝑈 ∈ LVec )
37 5 lvecdrng ⊢ ( 𝑈 ∈ LVec → 𝑅 ∈ DivRing )
38 36 37 syl ⊢ ( ( 𝜑 ∧ 𝑧 ∈ ( ⊥ ‘ ( 𝐿 ‘ 𝐺 ) ) ∧ ( 𝐺 ‘ 𝑧 ) ≠ ( 0g ‘ 𝑅 ) ) → 𝑅 ∈ DivRing )
39 15 3ad2ant1 ⊢ ( ( 𝜑 ∧ 𝑧 ∈ ( ⊥ ‘ ( 𝐿 ‘ 𝐺 ) ) ∧ ( 𝐺 ‘ 𝑧 ) ≠ ( 0g ‘ 𝑅 ) ) → 𝑈 ∈ LMod )
40 11 3ad2ant1 ⊢ ( ( 𝜑 ∧ 𝑧 ∈ ( ⊥ ‘ ( 𝐿 ‘ 𝐺 ) ) ∧ ( 𝐺 ‘ 𝑧 ) ≠ ( 0g ‘ 𝑅 ) ) → 𝐺 ∈ 𝐹 )
41 1 3 4 2 dochssv ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝐿 ‘ 𝐺 ) ⊆ 𝑉 ) → ( ⊥ ‘ ( 𝐿 ‘ 𝐺 ) ) ⊆ 𝑉 )
42 10 29 41 syl2anc ⊢ ( 𝜑 → ( ⊥ ‘ ( 𝐿 ‘ 𝐺 ) ) ⊆ 𝑉 )
43 42 sselda ⊢ ( ( 𝜑 ∧ 𝑧 ∈ ( ⊥ ‘ ( 𝐿 ‘ 𝐺 ) ) ) → 𝑧 ∈ 𝑉 )
44 43 3adant3 ⊢ ( ( 𝜑 ∧ 𝑧 ∈ ( ⊥ ‘ ( 𝐿 ‘ 𝐺 ) ) ∧ ( 𝐺 ‘ 𝑧 ) ≠ ( 0g ‘ 𝑅 ) ) → 𝑧 ∈ 𝑉 )
45 eqid ⊢ ( Base ‘ 𝑅 ) = ( Base ‘ 𝑅 )
46 5 45 4 8 lflcl ⊢ ( ( 𝑈 ∈ LMod ∧ 𝐺 ∈ 𝐹 ∧ 𝑧 ∈ 𝑉 ) → ( 𝐺 ‘ 𝑧 ) ∈ ( Base ‘ 𝑅 ) )
47 39 40 44 46 syl3anc ⊢ ( ( 𝜑 ∧ 𝑧 ∈ ( ⊥ ‘ ( 𝐿 ‘ 𝐺 ) ) ∧ ( 𝐺 ‘ 𝑧 ) ≠ ( 0g ‘ 𝑅 ) ) → ( 𝐺 ‘ 𝑧 ) ∈ ( Base ‘ 𝑅 ) )
48 simp3 ⊢ ( ( 𝜑 ∧ 𝑧 ∈ ( ⊥ ‘ ( 𝐿 ‘ 𝐺 ) ) ∧ ( 𝐺 ‘ 𝑧 ) ≠ ( 0g ‘ 𝑅 ) ) → ( 𝐺 ‘ 𝑧 ) ≠ ( 0g ‘ 𝑅 ) )
49 eqid ⊢ ( invr ‘ 𝑅 ) = ( invr ‘ 𝑅 )
50 45 19 49 drnginvrcl ⊢ ( ( 𝑅 ∈ DivRing ∧ ( 𝐺 ‘ 𝑧 ) ∈ ( Base ‘ 𝑅 ) ∧ ( 𝐺 ‘ 𝑧 ) ≠ ( 0g ‘ 𝑅 ) ) → ( ( invr ‘ 𝑅 ) ‘ ( 𝐺 ‘ 𝑧 ) ) ∈ ( Base ‘ 𝑅 ) )
51 38 47 48 50 syl3anc ⊢ ( ( 𝜑 ∧ 𝑧 ∈ ( ⊥ ‘ ( 𝐿 ‘ 𝐺 ) ) ∧ ( 𝐺 ‘ 𝑧 ) ≠ ( 0g ‘ 𝑅 ) ) → ( ( invr ‘ 𝑅 ) ‘ ( 𝐺 ‘ 𝑧 ) ) ∈ ( Base ‘ 𝑅 ) )
52 simp2 ⊢ ( ( 𝜑 ∧ 𝑧 ∈ ( ⊥ ‘ ( 𝐿 ‘ 𝐺 ) ) ∧ ( 𝐺 ‘ 𝑧 ) ≠ ( 0g ‘ 𝑅 ) ) → 𝑧 ∈ ( ⊥ ‘ ( 𝐿 ‘ 𝐺 ) ) )
53 51 52 jca ⊢ ( ( 𝜑 ∧ 𝑧 ∈ ( ⊥ ‘ ( 𝐿 ‘ 𝐺 ) ) ∧ ( 𝐺 ‘ 𝑧 ) ≠ ( 0g ‘ 𝑅 ) ) → ( ( ( invr ‘ 𝑅 ) ‘ ( 𝐺 ‘ 𝑧 ) ) ∈ ( Base ‘ 𝑅 ) ∧ 𝑧 ∈ ( ⊥ ‘ ( 𝐿 ‘ 𝐺 ) ) ) )
54 eqid ⊢ ( ·𝑠 ‘ 𝑈 ) = ( ·𝑠 ‘ 𝑈 )
55 5 54 45 30 lssvscl ⊢ ( ( ( 𝑈 ∈ LMod ∧ ( ⊥ ‘ ( 𝐿 ‘ 𝐺 ) ) ∈ ( LSubSp ‘ 𝑈 ) ) ∧ ( ( ( invr ‘ 𝑅 ) ‘ ( 𝐺 ‘ 𝑧 ) ) ∈ ( Base ‘ 𝑅 ) ∧ 𝑧 ∈ ( ⊥ ‘ ( 𝐿 ‘ 𝐺 ) ) ) ) → ( ( ( invr ‘ 𝑅 ) ‘ ( 𝐺 ‘ 𝑧 ) ) ( ·𝑠 ‘ 𝑈 ) 𝑧 ) ∈ ( ⊥ ‘ ( 𝐿 ‘ 𝐺 ) ) )
56 34 53 55 syl2anc ⊢ ( ( 𝜑 ∧ 𝑧 ∈ ( ⊥ ‘ ( 𝐿 ‘ 𝐺 ) ) ∧ ( 𝐺 ‘ 𝑧 ) ≠ ( 0g ‘ 𝑅 ) ) → ( ( ( invr ‘ 𝑅 ) ‘ ( 𝐺 ‘ 𝑧 ) ) ( ·𝑠 ‘ 𝑈 ) 𝑧 ) ∈ ( ⊥ ‘ ( 𝐿 ‘ 𝐺 ) ) )
57 45 19 49 drnginvrn0 ⊢ ( ( 𝑅 ∈ DivRing ∧ ( 𝐺 ‘ 𝑧 ) ∈ ( Base ‘ 𝑅 ) ∧ ( 𝐺 ‘ 𝑧 ) ≠ ( 0g ‘ 𝑅 ) ) → ( ( invr ‘ 𝑅 ) ‘ ( 𝐺 ‘ 𝑧 ) ) ≠ ( 0g ‘ 𝑅 ) )
58 38 47 48 57 syl3anc ⊢ ( ( 𝜑 ∧ 𝑧 ∈ ( ⊥ ‘ ( 𝐿 ‘ 𝐺 ) ) ∧ ( 𝐺 ‘ 𝑧 ) ≠ ( 0g ‘ 𝑅 ) ) → ( ( invr ‘ 𝑅 ) ‘ ( 𝐺 ‘ 𝑧 ) ) ≠ ( 0g ‘ 𝑅 ) )
59 15 adantr ⊢ ( ( 𝜑 ∧ 𝑧 ∈ ( ⊥ ‘ ( 𝐿 ‘ 𝐺 ) ) ) → 𝑈 ∈ LMod )
60 11 adantr ⊢ ( ( 𝜑 ∧ 𝑧 ∈ ( ⊥ ‘ ( 𝐿 ‘ 𝐺 ) ) ) → 𝐺 ∈ 𝐹 )
61 5 19 6 8 lfl0 ⊢ ( ( 𝑈 ∈ LMod ∧ 𝐺 ∈ 𝐹 ) → ( 𝐺 ‘ 0 ) = ( 0g ‘ 𝑅 ) )
62 59 60 61 syl2anc ⊢ ( ( 𝜑 ∧ 𝑧 ∈ ( ⊥ ‘ ( 𝐿 ‘ 𝐺 ) ) ) → ( 𝐺 ‘ 0 ) = ( 0g ‘ 𝑅 ) )
63 fveqeq2 ⊢ ( 𝑧 = 0 → ( ( 𝐺 ‘ 𝑧 ) = ( 0g ‘ 𝑅 ) ↔ ( 𝐺 ‘ 0 ) = ( 0g ‘ 𝑅 ) ) )
64 62 63 syl5ibrcom ⊢ ( ( 𝜑 ∧ 𝑧 ∈ ( ⊥ ‘ ( 𝐿 ‘ 𝐺 ) ) ) → ( 𝑧 = 0 → ( 𝐺 ‘ 𝑧 ) = ( 0g ‘ 𝑅 ) ) )
65 64 necon3d ⊢ ( ( 𝜑 ∧ 𝑧 ∈ ( ⊥ ‘ ( 𝐿 ‘ 𝐺 ) ) ) → ( ( 𝐺 ‘ 𝑧 ) ≠ ( 0g ‘ 𝑅 ) → 𝑧 ≠ 0 ) )
66 65 3impia ⊢ ( ( 𝜑 ∧ 𝑧 ∈ ( ⊥ ‘ ( 𝐿 ‘ 𝐺 ) ) ∧ ( 𝐺 ‘ 𝑧 ) ≠ ( 0g ‘ 𝑅 ) ) → 𝑧 ≠ 0 )
67 4 54 5 45 19 6 36 51 44 lvecvsn0 ⊢ ( ( 𝜑 ∧ 𝑧 ∈ ( ⊥ ‘ ( 𝐿 ‘ 𝐺 ) ) ∧ ( 𝐺 ‘ 𝑧 ) ≠ ( 0g ‘ 𝑅 ) ) → ( ( ( ( invr ‘ 𝑅 ) ‘ ( 𝐺 ‘ 𝑧 ) ) ( ·𝑠 ‘ 𝑈 ) 𝑧 ) ≠ 0 ↔ ( ( ( invr ‘ 𝑅 ) ‘ ( 𝐺 ‘ 𝑧 ) ) ≠ ( 0g ‘ 𝑅 ) ∧ 𝑧 ≠ 0 ) ) )
68 58 66 67 mpbir2and ⊢ ( ( 𝜑 ∧ 𝑧 ∈ ( ⊥ ‘ ( 𝐿 ‘ 𝐺 ) ) ∧ ( 𝐺 ‘ 𝑧 ) ≠ ( 0g ‘ 𝑅 ) ) → ( ( ( invr ‘ 𝑅 ) ‘ ( 𝐺 ‘ 𝑧 ) ) ( ·𝑠 ‘ 𝑈 ) 𝑧 ) ≠ 0 )
69 eldifsn ⊢ ( ( ( ( invr ‘ 𝑅 ) ‘ ( 𝐺 ‘ 𝑧 ) ) ( ·𝑠 ‘ 𝑈 ) 𝑧 ) ∈ ( ( ⊥ ‘ ( 𝐿 ‘ 𝐺 ) ) ∖ { 0 } ) ↔ ( ( ( ( invr ‘ 𝑅 ) ‘ ( 𝐺 ‘ 𝑧 ) ) ( ·𝑠 ‘ 𝑈 ) 𝑧 ) ∈ ( ⊥ ‘ ( 𝐿 ‘ 𝐺 ) ) ∧ ( ( ( invr ‘ 𝑅 ) ‘ ( 𝐺 ‘ 𝑧 ) ) ( ·𝑠 ‘ 𝑈 ) 𝑧 ) ≠ 0 ) )
70 56 68 69 sylanbrc ⊢ ( ( 𝜑 ∧ 𝑧 ∈ ( ⊥ ‘ ( 𝐿 ‘ 𝐺 ) ) ∧ ( 𝐺 ‘ 𝑧 ) ≠ ( 0g ‘ 𝑅 ) ) → ( ( ( invr ‘ 𝑅 ) ‘ ( 𝐺 ‘ 𝑧 ) ) ( ·𝑠 ‘ 𝑈 ) 𝑧 ) ∈ ( ( ⊥ ‘ ( 𝐿 ‘ 𝐺 ) ) ∖ { 0 } ) )
71 eqid ⊢ ( .r ‘ 𝑅 ) = ( .r ‘ 𝑅 )
72 5 45 71 4 54 8 lflmul ⊢ ( ( 𝑈 ∈ LMod ∧ 𝐺 ∈ 𝐹 ∧ ( ( ( invr ‘ 𝑅 ) ‘ ( 𝐺 ‘ 𝑧 ) ) ∈ ( Base ‘ 𝑅 ) ∧ 𝑧 ∈ 𝑉 ) ) → ( 𝐺 ‘ ( ( ( invr ‘ 𝑅 ) ‘ ( 𝐺 ‘ 𝑧 ) ) ( ·𝑠 ‘ 𝑈 ) 𝑧 ) ) = ( ( ( invr ‘ 𝑅 ) ‘ ( 𝐺 ‘ 𝑧 ) ) ( .r ‘ 𝑅 ) ( 𝐺 ‘ 𝑧 ) ) )
73 39 40 51 44 72 syl112anc ⊢ ( ( 𝜑 ∧ 𝑧 ∈ ( ⊥ ‘ ( 𝐿 ‘ 𝐺 ) ) ∧ ( 𝐺 ‘ 𝑧 ) ≠ ( 0g ‘ 𝑅 ) ) → ( 𝐺 ‘ ( ( ( invr ‘ 𝑅 ) ‘ ( 𝐺 ‘ 𝑧 ) ) ( ·𝑠 ‘ 𝑈 ) 𝑧 ) ) = ( ( ( invr ‘ 𝑅 ) ‘ ( 𝐺 ‘ 𝑧 ) ) ( .r ‘ 𝑅 ) ( 𝐺 ‘ 𝑧 ) ) )
74 45 19 71 7 49 drnginvrl ⊢ ( ( 𝑅 ∈ DivRing ∧ ( 𝐺 ‘ 𝑧 ) ∈ ( Base ‘ 𝑅 ) ∧ ( 𝐺 ‘ 𝑧 ) ≠ ( 0g ‘ 𝑅 ) ) → ( ( ( invr ‘ 𝑅 ) ‘ ( 𝐺 ‘ 𝑧 ) ) ( .r ‘ 𝑅 ) ( 𝐺 ‘ 𝑧 ) ) = 1 )
75 38 47 48 74 syl3anc ⊢ ( ( 𝜑 ∧ 𝑧 ∈ ( ⊥ ‘ ( 𝐿 ‘ 𝐺 ) ) ∧ ( 𝐺 ‘ 𝑧 ) ≠ ( 0g ‘ 𝑅 ) ) → ( ( ( invr ‘ 𝑅 ) ‘ ( 𝐺 ‘ 𝑧 ) ) ( .r ‘ 𝑅 ) ( 𝐺 ‘ 𝑧 ) ) = 1 )
76 73 75 eqtrd ⊢ ( ( 𝜑 ∧ 𝑧 ∈ ( ⊥ ‘ ( 𝐿 ‘ 𝐺 ) ) ∧ ( 𝐺 ‘ 𝑧 ) ≠ ( 0g ‘ 𝑅 ) ) → ( 𝐺 ‘ ( ( ( invr ‘ 𝑅 ) ‘ ( 𝐺 ‘ 𝑧 ) ) ( ·𝑠 ‘ 𝑈 ) 𝑧 ) ) = 1 )
77 fveqeq2 ⊢ ( 𝑥 = ( ( ( invr ‘ 𝑅 ) ‘ ( 𝐺 ‘ 𝑧 ) ) ( ·𝑠 ‘ 𝑈 ) 𝑧 ) → ( ( 𝐺 ‘ 𝑥 ) = 1 ↔ ( 𝐺 ‘ ( ( ( invr ‘ 𝑅 ) ‘ ( 𝐺 ‘ 𝑧 ) ) ( ·𝑠 ‘ 𝑈 ) 𝑧 ) ) = 1 ) )
78 77 rspcev ⊢ ( ( ( ( ( invr ‘ 𝑅 ) ‘ ( 𝐺 ‘ 𝑧 ) ) ( ·𝑠 ‘ 𝑈 ) 𝑧 ) ∈ ( ( ⊥ ‘ ( 𝐿 ‘ 𝐺 ) ) ∖ { 0 } ) ∧ ( 𝐺 ‘ ( ( ( invr ‘ 𝑅 ) ‘ ( 𝐺 ‘ 𝑧 ) ) ( ·𝑠 ‘ 𝑈 ) 𝑧 ) ) = 1 ) → ∃ 𝑥 ∈ ( ( ⊥ ‘ ( 𝐿 ‘ 𝐺 ) ) ∖ { 0 } ) ( 𝐺 ‘ 𝑥 ) = 1 )
79 70 76 78 syl2anc ⊢ ( ( 𝜑 ∧ 𝑧 ∈ ( ⊥ ‘ ( 𝐿 ‘ 𝐺 ) ) ∧ ( 𝐺 ‘ 𝑧 ) ≠ ( 0g ‘ 𝑅 ) ) → ∃ 𝑥 ∈ ( ( ⊥ ‘ ( 𝐿 ‘ 𝐺 ) ) ∖ { 0 } ) ( 𝐺 ‘ 𝑥 ) = 1 )
80 79 rexlimdv3a ⊢ ( 𝜑 → ( ∃ 𝑧 ∈ ( ⊥ ‘ ( 𝐿 ‘ 𝐺 ) ) ( 𝐺 ‘ 𝑧 ) ≠ ( 0g ‘ 𝑅 ) → ∃ 𝑥 ∈ ( ( ⊥ ‘ ( 𝐿 ‘ 𝐺 ) ) ∖ { 0 } ) ( 𝐺 ‘ 𝑥 ) = 1 ) )
81 28 80 mpd ⊢ ( 𝜑 → ∃ 𝑥 ∈ ( ( ⊥ ‘ ( 𝐿 ‘ 𝐺 ) ) ∖ { 0 } ) ( 𝐺 ‘ 𝑥 ) = 1 )