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 )