Theorem lcfrlem16

Description: Lemma for lcfr . (Contributed by NM, 8-Mar-2015)

	Ref	Expression
Hypotheses	lcf1o.h	⊢ 𝐻 = ( LHyp ‘ 𝐾 )
	lcf1o.o	⊢ ⊥ = ( ( ocH ‘ 𝐾 ) ‘ 𝑊 )
	lcf1o.u	⊢ 𝑈 = ( ( DVecH ‘ 𝐾 ) ‘ 𝑊 )
	lcf1o.v	⊢ 𝑉 = ( Base ‘ 𝑈 )
	lcf1o.a	⊢ + = ( +g ‘ 𝑈 )
	lcf1o.t	⊢ · = ( ·𝑠 ‘ 𝑈 )
	lcf1o.s	⊢ 𝑆 = ( Scalar ‘ 𝑈 )
	lcf1o.r	⊢ 𝑅 = ( Base ‘ 𝑆 )
	lcf1o.z	⊢ 0 = ( 0g ‘ 𝑈 )
	lcf1o.f	⊢ 𝐹 = ( LFnl ‘ 𝑈 )
	lcf1o.l	⊢ 𝐿 = ( LKer ‘ 𝑈 )
	lcf1o.d	⊢ 𝐷 = ( LDual ‘ 𝑈 )
	lcf1o.q	⊢ 𝑄 = ( 0g ‘ 𝐷 )
	lcf1o.c	⊢ 𝐶 = { 𝑓 ∈ 𝐹 ∣ ( ⊥ ‘ ( ⊥ ‘ ( 𝐿 ‘ 𝑓 ) ) ) = ( 𝐿 ‘ 𝑓 ) }
	lcf1o.j	⊢ 𝐽 = ( 𝑥 ∈ ( 𝑉 ∖ { 0 } ) ↦ ( 𝑣 ∈ 𝑉 ↦ ( ℩ 𝑘 ∈ 𝑅 ∃ 𝑤 ∈ ( ⊥ ‘ { 𝑥 } ) 𝑣 = ( 𝑤 + ( 𝑘 · 𝑥 ) ) ) ) )
	lcflo.k	⊢ ( 𝜑 → ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) )
	lcfrlem16.p	⊢ 𝑃 = ( LSubSp ‘ 𝐷 )
	lcfrlem16.g	⊢ ( 𝜑 → 𝐺 ∈ 𝑃 )
	lcfrlem16.gs	⊢ ( 𝜑 → 𝐺 ⊆ 𝐶 )
	lcfrlem16.m	⊢ 𝐸 = ∪ 𝑔 ∈ 𝐺 ( ⊥ ‘ ( 𝐿 ‘ 𝑔 ) )
	lcfrlem16.x	⊢ ( 𝜑 → 𝑋 ∈ ( 𝐸 ∖ { 0 } ) )
Assertion	lcfrlem16	⊢ ( 𝜑 → ( 𝐽 ‘ 𝑋 ) ∈ 𝐺 )

Proof

Step	Hyp	Ref	Expression
1		lcf1o.h	⊢ 𝐻 = ( LHyp ‘ 𝐾 )
2		lcf1o.o	⊢ ⊥ = ( ( ocH ‘ 𝐾 ) ‘ 𝑊 )
3		lcf1o.u	⊢ 𝑈 = ( ( DVecH ‘ 𝐾 ) ‘ 𝑊 )
4		lcf1o.v	⊢ 𝑉 = ( Base ‘ 𝑈 )
5		lcf1o.a	⊢ + = ( +g ‘ 𝑈 )
6		lcf1o.t	⊢ · = ( ·𝑠 ‘ 𝑈 )
7		lcf1o.s	⊢ 𝑆 = ( Scalar ‘ 𝑈 )
8		lcf1o.r	⊢ 𝑅 = ( Base ‘ 𝑆 )
9		lcf1o.z	⊢ 0 = ( 0g ‘ 𝑈 )
10		lcf1o.f	⊢ 𝐹 = ( LFnl ‘ 𝑈 )
11		lcf1o.l	⊢ 𝐿 = ( LKer ‘ 𝑈 )
12		lcf1o.d	⊢ 𝐷 = ( LDual ‘ 𝑈 )
13		lcf1o.q	⊢ 𝑄 = ( 0g ‘ 𝐷 )
14		lcf1o.c	⊢ 𝐶 = { 𝑓 ∈ 𝐹 ∣ ( ⊥ ‘ ( ⊥ ‘ ( 𝐿 ‘ 𝑓 ) ) ) = ( 𝐿 ‘ 𝑓 ) }
15		lcf1o.j	⊢ 𝐽 = ( 𝑥 ∈ ( 𝑉 ∖ { 0 } ) ↦ ( 𝑣 ∈ 𝑉 ↦ ( ℩ 𝑘 ∈ 𝑅 ∃ 𝑤 ∈ ( ⊥ ‘ { 𝑥 } ) 𝑣 = ( 𝑤 + ( 𝑘 · 𝑥 ) ) ) ) )
16		lcflo.k	⊢ ( 𝜑 → ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) )
17		lcfrlem16.p	⊢ 𝑃 = ( LSubSp ‘ 𝐷 )
18		lcfrlem16.g	⊢ ( 𝜑 → 𝐺 ∈ 𝑃 )
19		lcfrlem16.gs	⊢ ( 𝜑 → 𝐺 ⊆ 𝐶 )
20		lcfrlem16.m	⊢ 𝐸 = ∪ 𝑔 ∈ 𝐺 ( ⊥ ‘ ( 𝐿 ‘ 𝑔 ) )
21		lcfrlem16.x	⊢ ( 𝜑 → 𝑋 ∈ ( 𝐸 ∖ { 0 } ) )
22	21	eldifad	⊢ ( 𝜑 → 𝑋 ∈ 𝐸 )
23	22 20	eleqtrdi	⊢ ( 𝜑 → 𝑋 ∈ ∪ 𝑔 ∈ 𝐺 ( ⊥ ‘ ( 𝐿 ‘ 𝑔 ) ) )
24		eliun	⊢ ( 𝑋 ∈ ∪ 𝑔 ∈ 𝐺 ( ⊥ ‘ ( 𝐿 ‘ 𝑔 ) ) ↔ ∃ 𝑔 ∈ 𝐺 𝑋 ∈ ( ⊥ ‘ ( 𝐿 ‘ 𝑔 ) ) )
25	23 24	sylib	⊢ ( 𝜑 → ∃ 𝑔 ∈ 𝐺 𝑋 ∈ ( ⊥ ‘ ( 𝐿 ‘ 𝑔 ) ) )
26		eqid	⊢ ( ·𝑠 ‘ 𝐷 ) = ( ·𝑠 ‘ 𝐷 )
27	1 3 16	dvhlvec	⊢ ( 𝜑 → 𝑈 ∈ LVec )
28	27	3ad2ant1	⊢ ( ( 𝜑 ∧ 𝑔 ∈ 𝐺 ∧ 𝑋 ∈ ( ⊥ ‘ ( 𝐿 ‘ 𝑔 ) ) ) → 𝑈 ∈ LVec )
29		eqid	⊢ ( Base ‘ 𝐷 ) = ( Base ‘ 𝐷 )
30	29 17	lssel	⊢ ( ( 𝐺 ∈ 𝑃 ∧ 𝑔 ∈ 𝐺 ) → 𝑔 ∈ ( Base ‘ 𝐷 ) )
31	18 30	sylan	⊢ ( ( 𝜑 ∧ 𝑔 ∈ 𝐺 ) → 𝑔 ∈ ( Base ‘ 𝐷 ) )
32	1 3 16	dvhlmod	⊢ ( 𝜑 → 𝑈 ∈ LMod )
33	10 12 29 32	ldualvbase	⊢ ( 𝜑 → ( Base ‘ 𝐷 ) = 𝐹 )
34	33	adantr	⊢ ( ( 𝜑 ∧ 𝑔 ∈ 𝐺 ) → ( Base ‘ 𝐷 ) = 𝐹 )
35	31 34	eleqtrd	⊢ ( ( 𝜑 ∧ 𝑔 ∈ 𝐺 ) → 𝑔 ∈ 𝐹 )
36	35	3adant3	⊢ ( ( 𝜑 ∧ 𝑔 ∈ 𝐺 ∧ 𝑋 ∈ ( ⊥ ‘ ( 𝐿 ‘ 𝑔 ) ) ) → 𝑔 ∈ 𝐹 )
37	16	adantr	⊢ ( ( 𝜑 ∧ 𝑔 ∈ 𝐺 ) → ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) )
38	32	adantr	⊢ ( ( 𝜑 ∧ 𝑔 ∈ 𝐺 ) → 𝑈 ∈ LMod )
39	4 10 11 38 35	lkrssv	⊢ ( ( 𝜑 ∧ 𝑔 ∈ 𝐺 ) → ( 𝐿 ‘ 𝑔 ) ⊆ 𝑉 )
40	1 3 4 2	dochssv	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝐿 ‘ 𝑔 ) ⊆ 𝑉 ) → ( ⊥ ‘ ( 𝐿 ‘ 𝑔 ) ) ⊆ 𝑉 )
41	37 39 40	syl2anc	⊢ ( ( 𝜑 ∧ 𝑔 ∈ 𝐺 ) → ( ⊥ ‘ ( 𝐿 ‘ 𝑔 ) ) ⊆ 𝑉 )
42	41	ralrimiva	⊢ ( 𝜑 → ∀ 𝑔 ∈ 𝐺 ( ⊥ ‘ ( 𝐿 ‘ 𝑔 ) ) ⊆ 𝑉 )
43		iunss	⊢ ( ∪ 𝑔 ∈ 𝐺 ( ⊥ ‘ ( 𝐿 ‘ 𝑔 ) ) ⊆ 𝑉 ↔ ∀ 𝑔 ∈ 𝐺 ( ⊥ ‘ ( 𝐿 ‘ 𝑔 ) ) ⊆ 𝑉 )
44	42 43	sylibr	⊢ ( 𝜑 → ∪ 𝑔 ∈ 𝐺 ( ⊥ ‘ ( 𝐿 ‘ 𝑔 ) ) ⊆ 𝑉 )
45	20 44	eqsstrid	⊢ ( 𝜑 → 𝐸 ⊆ 𝑉 )
46	45	ssdifd	⊢ ( 𝜑 → ( 𝐸 ∖ { 0 } ) ⊆ ( 𝑉 ∖ { 0 } ) )
47	46 21	sseldd	⊢ ( 𝜑 → 𝑋 ∈ ( 𝑉 ∖ { 0 } ) )
48	1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 47	lcfrlem10	⊢ ( 𝜑 → ( 𝐽 ‘ 𝑋 ) ∈ 𝐹 )
49	48	3ad2ant1	⊢ ( ( 𝜑 ∧ 𝑔 ∈ 𝐺 ∧ 𝑋 ∈ ( ⊥ ‘ ( 𝐿 ‘ 𝑔 ) ) ) → ( 𝐽 ‘ 𝑋 ) ∈ 𝐹 )
50		eqid	⊢ ( LSAtoms ‘ 𝑈 ) = ( LSAtoms ‘ 𝑈 )
51	16	3ad2ant1	⊢ ( ( 𝜑 ∧ 𝑔 ∈ 𝐺 ∧ 𝑋 ∈ ( ⊥ ‘ ( 𝐿 ‘ 𝑔 ) ) ) → ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) )
52		simp3	⊢ ( ( 𝜑 ∧ 𝑔 ∈ 𝐺 ∧ 𝑋 ∈ ( ⊥ ‘ ( 𝐿 ‘ 𝑔 ) ) ) → 𝑋 ∈ ( ⊥ ‘ ( 𝐿 ‘ 𝑔 ) ) )
53		eldifsni	⊢ ( 𝑋 ∈ ( 𝐸 ∖ { 0 } ) → 𝑋 ≠ 0 )
54	21 53	syl	⊢ ( 𝜑 → 𝑋 ≠ 0 )
55	54	3ad2ant1	⊢ ( ( 𝜑 ∧ 𝑔 ∈ 𝐺 ∧ 𝑋 ∈ ( ⊥ ‘ ( 𝐿 ‘ 𝑔 ) ) ) → 𝑋 ≠ 0 )
56		eldifsn	⊢ ( 𝑋 ∈ ( ( ⊥ ‘ ( 𝐿 ‘ 𝑔 ) ) ∖ { 0 } ) ↔ ( 𝑋 ∈ ( ⊥ ‘ ( 𝐿 ‘ 𝑔 ) ) ∧ 𝑋 ≠ 0 ) )
57	52 55 56	sylanbrc	⊢ ( ( 𝜑 ∧ 𝑔 ∈ 𝐺 ∧ 𝑋 ∈ ( ⊥ ‘ ( 𝐿 ‘ 𝑔 ) ) ) → 𝑋 ∈ ( ( ⊥ ‘ ( 𝐿 ‘ 𝑔 ) ) ∖ { 0 } ) )
58	1 2 3 4 9 10 11 51 36 57 50	dochsnkrlem2	⊢ ( ( 𝜑 ∧ 𝑔 ∈ 𝐺 ∧ 𝑋 ∈ ( ⊥ ‘ ( 𝐿 ‘ 𝑔 ) ) ) → ( ⊥ ‘ ( 𝐿 ‘ 𝑔 ) ) ∈ ( LSAtoms ‘ 𝑈 ) )
59	1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 47	lcfrlem15	⊢ ( 𝜑 → 𝑋 ∈ ( ⊥ ‘ ( 𝐿 ‘ ( 𝐽 ‘ 𝑋 ) ) ) )
60		eldifsn	⊢ ( 𝑋 ∈ ( ( ⊥ ‘ ( 𝐿 ‘ ( 𝐽 ‘ 𝑋 ) ) ) ∖ { 0 } ) ↔ ( 𝑋 ∈ ( ⊥ ‘ ( 𝐿 ‘ ( 𝐽 ‘ 𝑋 ) ) ) ∧ 𝑋 ≠ 0 ) )
61	59 54 60	sylanbrc	⊢ ( 𝜑 → 𝑋 ∈ ( ( ⊥ ‘ ( 𝐿 ‘ ( 𝐽 ‘ 𝑋 ) ) ) ∖ { 0 } ) )
62	1 2 3 4 9 10 11 16 48 61 50	dochsnkrlem2	⊢ ( 𝜑 → ( ⊥ ‘ ( 𝐿 ‘ ( 𝐽 ‘ 𝑋 ) ) ) ∈ ( LSAtoms ‘ 𝑈 ) )
63	62	3ad2ant1	⊢ ( ( 𝜑 ∧ 𝑔 ∈ 𝐺 ∧ 𝑋 ∈ ( ⊥ ‘ ( 𝐿 ‘ 𝑔 ) ) ) → ( ⊥ ‘ ( 𝐿 ‘ ( 𝐽 ‘ 𝑋 ) ) ) ∈ ( LSAtoms ‘ 𝑈 ) )
64	59	3ad2ant1	⊢ ( ( 𝜑 ∧ 𝑔 ∈ 𝐺 ∧ 𝑋 ∈ ( ⊥ ‘ ( 𝐿 ‘ 𝑔 ) ) ) → 𝑋 ∈ ( ⊥ ‘ ( 𝐿 ‘ ( 𝐽 ‘ 𝑋 ) ) ) )
65	9 50 28 58 63 55 52 64	lsat2el	⊢ ( ( 𝜑 ∧ 𝑔 ∈ 𝐺 ∧ 𝑋 ∈ ( ⊥ ‘ ( 𝐿 ‘ 𝑔 ) ) ) → ( ⊥ ‘ ( 𝐿 ‘ 𝑔 ) ) = ( ⊥ ‘ ( 𝐿 ‘ ( 𝐽 ‘ 𝑋 ) ) ) )
66		eqid	⊢ ( ( DIsoH ‘ 𝐾 ) ‘ 𝑊 ) = ( ( DIsoH ‘ 𝐾 ) ‘ 𝑊 )
67	19	3ad2ant1	⊢ ( ( 𝜑 ∧ 𝑔 ∈ 𝐺 ∧ 𝑋 ∈ ( ⊥ ‘ ( 𝐿 ‘ 𝑔 ) ) ) → 𝐺 ⊆ 𝐶 )
68		simp2	⊢ ( ( 𝜑 ∧ 𝑔 ∈ 𝐺 ∧ 𝑋 ∈ ( ⊥ ‘ ( 𝐿 ‘ 𝑔 ) ) ) → 𝑔 ∈ 𝐺 )
69	67 68	sseldd	⊢ ( ( 𝜑 ∧ 𝑔 ∈ 𝐺 ∧ 𝑋 ∈ ( ⊥ ‘ ( 𝐿 ‘ 𝑔 ) ) ) → 𝑔 ∈ 𝐶 )
70	1 66 2 3 10 11 14 51 36	lcfl5	⊢ ( ( 𝜑 ∧ 𝑔 ∈ 𝐺 ∧ 𝑋 ∈ ( ⊥ ‘ ( 𝐿 ‘ 𝑔 ) ) ) → ( 𝑔 ∈ 𝐶 ↔ ( 𝐿 ‘ 𝑔 ) ∈ ran ( ( DIsoH ‘ 𝐾 ) ‘ 𝑊 ) ) )
71	69 70	mpbid	⊢ ( ( 𝜑 ∧ 𝑔 ∈ 𝐺 ∧ 𝑋 ∈ ( ⊥ ‘ ( 𝐿 ‘ 𝑔 ) ) ) → ( 𝐿 ‘ 𝑔 ) ∈ ran ( ( DIsoH ‘ 𝐾 ) ‘ 𝑊 ) )
72	1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 47	lcfrlem13	⊢ ( 𝜑 → ( 𝐽 ‘ 𝑋 ) ∈ ( 𝐶 ∖ { 𝑄 } ) )
73	72	eldifad	⊢ ( 𝜑 → ( 𝐽 ‘ 𝑋 ) ∈ 𝐶 )
74	1 66 2 3 10 11 14 16 48	lcfl5	⊢ ( 𝜑 → ( ( 𝐽 ‘ 𝑋 ) ∈ 𝐶 ↔ ( 𝐿 ‘ ( 𝐽 ‘ 𝑋 ) ) ∈ ran ( ( DIsoH ‘ 𝐾 ) ‘ 𝑊 ) ) )
75	73 74	mpbid	⊢ ( 𝜑 → ( 𝐿 ‘ ( 𝐽 ‘ 𝑋 ) ) ∈ ran ( ( DIsoH ‘ 𝐾 ) ‘ 𝑊 ) )
76	75	3ad2ant1	⊢ ( ( 𝜑 ∧ 𝑔 ∈ 𝐺 ∧ 𝑋 ∈ ( ⊥ ‘ ( 𝐿 ‘ 𝑔 ) ) ) → ( 𝐿 ‘ ( 𝐽 ‘ 𝑋 ) ) ∈ ran ( ( DIsoH ‘ 𝐾 ) ‘ 𝑊 ) )
77	1 66 2 51 71 76	doch11	⊢ ( ( 𝜑 ∧ 𝑔 ∈ 𝐺 ∧ 𝑋 ∈ ( ⊥ ‘ ( 𝐿 ‘ 𝑔 ) ) ) → ( ( ⊥ ‘ ( 𝐿 ‘ 𝑔 ) ) = ( ⊥ ‘ ( 𝐿 ‘ ( 𝐽 ‘ 𝑋 ) ) ) ↔ ( 𝐿 ‘ 𝑔 ) = ( 𝐿 ‘ ( 𝐽 ‘ 𝑋 ) ) ) )
78	65 77	mpbid	⊢ ( ( 𝜑 ∧ 𝑔 ∈ 𝐺 ∧ 𝑋 ∈ ( ⊥ ‘ ( 𝐿 ‘ 𝑔 ) ) ) → ( 𝐿 ‘ 𝑔 ) = ( 𝐿 ‘ ( 𝐽 ‘ 𝑋 ) ) )
79	7 8 10 11 12 26 28 36 49 78	eqlkr4	⊢ ( ( 𝜑 ∧ 𝑔 ∈ 𝐺 ∧ 𝑋 ∈ ( ⊥ ‘ ( 𝐿 ‘ 𝑔 ) ) ) → ∃ 𝑘 ∈ 𝑅 ( 𝐽 ‘ 𝑋 ) = ( 𝑘 ( ·𝑠 ‘ 𝐷 ) 𝑔 ) )
80	32	3ad2ant1	⊢ ( ( 𝜑 ∧ 𝑔 ∈ 𝐺 ∧ 𝑋 ∈ ( ⊥ ‘ ( 𝐿 ‘ 𝑔 ) ) ) → 𝑈 ∈ LMod )
81	80	adantr	⊢ ( ( ( 𝜑 ∧ 𝑔 ∈ 𝐺 ∧ 𝑋 ∈ ( ⊥ ‘ ( 𝐿 ‘ 𝑔 ) ) ) ∧ 𝑘 ∈ 𝑅 ) → 𝑈 ∈ LMod )
82	18	3ad2ant1	⊢ ( ( 𝜑 ∧ 𝑔 ∈ 𝐺 ∧ 𝑋 ∈ ( ⊥ ‘ ( 𝐿 ‘ 𝑔 ) ) ) → 𝐺 ∈ 𝑃 )
83	82	adantr	⊢ ( ( ( 𝜑 ∧ 𝑔 ∈ 𝐺 ∧ 𝑋 ∈ ( ⊥ ‘ ( 𝐿 ‘ 𝑔 ) ) ) ∧ 𝑘 ∈ 𝑅 ) → 𝐺 ∈ 𝑃 )
84		simpr	⊢ ( ( ( 𝜑 ∧ 𝑔 ∈ 𝐺 ∧ 𝑋 ∈ ( ⊥ ‘ ( 𝐿 ‘ 𝑔 ) ) ) ∧ 𝑘 ∈ 𝑅 ) → 𝑘 ∈ 𝑅 )
85		simpl2	⊢ ( ( ( 𝜑 ∧ 𝑔 ∈ 𝐺 ∧ 𝑋 ∈ ( ⊥ ‘ ( 𝐿 ‘ 𝑔 ) ) ) ∧ 𝑘 ∈ 𝑅 ) → 𝑔 ∈ 𝐺 )
86	7 8 12 26 17 81 83 84 85	ldualssvscl	⊢ ( ( ( 𝜑 ∧ 𝑔 ∈ 𝐺 ∧ 𝑋 ∈ ( ⊥ ‘ ( 𝐿 ‘ 𝑔 ) ) ) ∧ 𝑘 ∈ 𝑅 ) → ( 𝑘 ( ·𝑠 ‘ 𝐷 ) 𝑔 ) ∈ 𝐺 )
87		eleq1	⊢ ( ( 𝐽 ‘ 𝑋 ) = ( 𝑘 ( ·𝑠 ‘ 𝐷 ) 𝑔 ) → ( ( 𝐽 ‘ 𝑋 ) ∈ 𝐺 ↔ ( 𝑘 ( ·𝑠 ‘ 𝐷 ) 𝑔 ) ∈ 𝐺 ) )
88	86 87	syl5ibrcom	⊢ ( ( ( 𝜑 ∧ 𝑔 ∈ 𝐺 ∧ 𝑋 ∈ ( ⊥ ‘ ( 𝐿 ‘ 𝑔 ) ) ) ∧ 𝑘 ∈ 𝑅 ) → ( ( 𝐽 ‘ 𝑋 ) = ( 𝑘 ( ·𝑠 ‘ 𝐷 ) 𝑔 ) → ( 𝐽 ‘ 𝑋 ) ∈ 𝐺 ) )
89	88	rexlimdva	⊢ ( ( 𝜑 ∧ 𝑔 ∈ 𝐺 ∧ 𝑋 ∈ ( ⊥ ‘ ( 𝐿 ‘ 𝑔 ) ) ) → ( ∃ 𝑘 ∈ 𝑅 ( 𝐽 ‘ 𝑋 ) = ( 𝑘 ( ·𝑠 ‘ 𝐷 ) 𝑔 ) → ( 𝐽 ‘ 𝑋 ) ∈ 𝐺 ) )
90	79 89	mpd	⊢ ( ( 𝜑 ∧ 𝑔 ∈ 𝐺 ∧ 𝑋 ∈ ( ⊥ ‘ ( 𝐿 ‘ 𝑔 ) ) ) → ( 𝐽 ‘ 𝑋 ) ∈ 𝐺 )
91	90	rexlimdv3a	⊢ ( 𝜑 → ( ∃ 𝑔 ∈ 𝐺 𝑋 ∈ ( ⊥ ‘ ( 𝐿 ‘ 𝑔 ) ) → ( 𝐽 ‘ 𝑋 ) ∈ 𝐺 ) )
92	25 91	mpd	⊢ ( 𝜑 → ( 𝐽 ‘ 𝑋 ) ∈ 𝐺 )