Metamath Proof Explorer

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