lcfrlem16 - Mathbox for Norm Megill

	Mathbox for Norm Megill		< Previous Next > Nearby theorems
Mirrors > Home > MPE Home > Th. List > Mathboxes > lcfrlem16		Structured version Visualization version GIF version

Theorem lcfrlem16 41677

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

**Hypotheses**
Ref	Expression
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 = (0_g‘𝑈)
lcf1o.f	⊢ 𝐹 = (LFnl‘𝑈)
lcf1o.l	⊢ 𝐿 = (LKer‘𝑈)
lcf1o.d	⊢ 𝐷 = (LDual‘𝑈)
lcf1o.q	⊢ 𝑄 = (0_g‘𝐷)
lcf1o.c	⊢ 𝐶 = {𝑓 ∈ 𝐹 ∣ ( ⊥ ‘( ⊥ ‘(𝐿‘𝑓))) = (𝐿‘𝑓)}
lcf1o.j	⊢ 𝐽 = (𝑥 ∈ (𝑉 ∖ { 0 }) ↦ (𝑣 ∈ 𝑉 ↦ (℩𝑘 ∈ 𝑅 ∃𝑤 ∈ ( ⊥ ‘{𝑥})𝑣 = (𝑤 + (𝑘 · 𝑥)))))
lcflo.k	⊢ (𝜑 → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻))
lcfrlem16.p	⊢ 𝑃 = (LSubSp‘𝐷)
lcfrlem16.g	⊢ (𝜑 → 𝐺 ∈ 𝑃)
lcfrlem16.gs	⊢ (𝜑 → 𝐺 ⊆ 𝐶)
lcfrlem16.m	⊢ 𝐸 = ∪ 𝑔 ∈ 𝐺 ( ⊥ ‘(𝐿‘𝑔))
lcfrlem16.x	⊢ (𝜑 → 𝑋 ∈ (𝐸 ∖ { 0 }))

**Assertion**
Ref	Expression
lcfrlem16	⊢ (𝜑 → (𝐽‘𝑋) ∈ 𝐺)

Distinct variable groups: 𝑥,𝑤, ⊥ 𝑥, 0 𝑥,𝑣,𝑉 𝑥, · 𝑣,𝑘,𝑤,𝑥,𝑋 𝑥, + 𝑥,𝑅 𝑓,𝑘,𝑣,𝑤, + 𝑓,𝐹,𝑘 𝑔,𝑘,𝐺 𝑓,𝑔,𝐽,𝑘 𝑓,𝐿,𝑘 ⊥ ,𝑓,𝑘,𝑣 𝑅,𝑓,𝑘,𝑣 𝑆,𝑘 · ,𝑓,𝑘,𝑣,𝑤 𝑈,𝑘 𝑓,𝑉,𝑔,𝑥 𝑓,𝑋 𝑣,𝑔,𝑤,𝑥,𝑋 𝜑,𝑔,𝑘 Allowed substitution hints: 𝜑(𝑥,𝑤,𝑣,𝑓) 𝐶(𝑥,𝑤,𝑣,𝑓,𝑔,𝑘) 𝐷(𝑥,𝑤,𝑣,𝑓,𝑔,𝑘) 𝑃(𝑥,𝑤,𝑣,𝑓,𝑔,𝑘) + (𝑔) 𝑄(𝑥,𝑤,𝑣,𝑓,𝑔,𝑘) 𝑅(𝑤,𝑔) 𝑆(𝑥,𝑤,𝑣,𝑓,𝑔) · (𝑔) 𝑈(𝑥,𝑤,𝑣,𝑓,𝑔) 𝐸(𝑥,𝑤,𝑣,𝑓,𝑔,𝑘) 𝐹(𝑥,𝑤,𝑣,𝑔) 𝐺(𝑥,𝑤,𝑣,𝑓) 𝐻(𝑥,𝑤,𝑣,𝑓,𝑔,𝑘) 𝐽(𝑥,𝑤,𝑣) 𝐾(𝑥,𝑤,𝑣,𝑓,𝑔,𝑘) 𝐿(𝑥,𝑤,𝑣,𝑔) ⊥ (𝑔) 𝑉(𝑤,𝑘) 𝑊(𝑥,𝑤,𝑣,𝑓,𝑔,𝑘) 0 (𝑤,𝑣,𝑓,𝑔,𝑘)

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

Colors of variables: wff setvar class

Syntax hints: → wi 4 ∧ wa 395 ∧ w3a 1086 = wceq 1541 ∈ wcel 2113 ≠ wne 2929 ∀wral 3048 ∃wrex 3057 {crab 3396 ∖ cdif 3895 ⊆ wss 3898 {csn 4575 ∪ ciun 4941 ↦ cmpt 5174 ran crn 5620 ‘cfv 6486 ℩crio 7308 (class class class)co 7352 Basecbs 17122 +_gcplusg 17163 Scalarcsca 17166 ·_𝑠 cvsca 17167 0_gc0g 17345 LModclmod 20795 LSubSpclss 20866 LVecclvec 21038 LSAtomsclsa 39093 LFnlclfn 39176 LKerclk 39204 LDualcld 39242 HLchlt 39469 LHypclh 40103 DVecHcdvh 41197 DIsoHcdih 41347 ocHcoch 41466

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1796 ax-4 1810 ax-5 1911 ax-6 1968 ax-7 2009 ax-8 2115 ax-9 2123 ax-10 2146 ax-11 2162 ax-12 2182 ax-ext 2705 ax-rep 5219 ax-sep 5236 ax-nul 5246 ax-pow 5305 ax-pr 5372 ax-un 7674 ax-cnex 11069 ax-resscn 11070 ax-1cn 11071 ax-icn 11072 ax-addcl 11073 ax-addrcl 11074 ax-mulcl 11075 ax-mulrcl 11076 ax-mulcom 11077 ax-addass 11078 ax-mulass 11079 ax-distr 11080 ax-i2m1 11081 ax-1ne0 11082 ax-1rid 11083 ax-rnegex 11084 ax-rrecex 11085 ax-cnre 11086 ax-pre-lttri 11087 ax-pre-lttrn 11088 ax-pre-ltadd 11089 ax-pre-mulgt0 11090 ax-riotaBAD 39072

This theorem depends on definitions: df-bi 207 df-an 396 df-or 848 df-3or 1087 df-3an 1088 df-tru 1544 df-fal 1554 df-ex 1781 df-nf 1785 df-sb 2068 df-mo 2537 df-eu 2566 df-clab 2712 df-cleq 2725 df-clel 2808 df-nfc 2882 df-ne 2930 df-nel 3034 df-ral 3049 df-rex 3058 df-rmo 3347 df-reu 3348 df-rab 3397 df-v 3439 df-sbc 3738 df-csb 3847 df-dif 3901 df-un 3903 df-in 3905 df-ss 3915 df-pss 3918 df-nul 4283 df-if 4475 df-pw 4551 df-sn 4576 df-pr 4578 df-tp 4580 df-op 4582 df-uni 4859 df-int 4898 df-iun 4943 df-iin 4944 df-br 5094 df-opab 5156 df-mpt 5175 df-tr 5201 df-id 5514 df-eprel 5519 df-po 5527 df-so 5528 df-fr 5572 df-we 5574 df-xp 5625 df-rel 5626 df-cnv 5627 df-co 5628 df-dm 5629 df-rn 5630 df-res 5631 df-ima 5632 df-pred 6253 df-ord 6314 df-on 6315 df-lim 6316 df-suc 6317 df-iota 6442 df-fun 6488 df-fn 6489 df-f 6490 df-f1 6491 df-fo 6492 df-f1o 6493 df-fv 6494 df-riota 7309 df-ov 7355 df-oprab 7356 df-mpo 7357 df-of 7616 df-om 7803 df-1st 7927 df-2nd 7928 df-tpos 8162 df-undef 8209 df-frecs 8217 df-wrecs 8248 df-recs 8297 df-rdg 8335 df-1o 8391 df-er 8628 df-map 8758 df-en 8876 df-dom 8877 df-sdom 8878 df-fin 8879 df-pnf 11155 df-mnf 11156 df-xr 11157 df-ltxr 11158 df-le 11159 df-sub 11353 df-neg 11354 df-nn 12133 df-2 12195 df-3 12196 df-4 12197 df-5 12198 df-6 12199 df-n0 12389 df-z 12476 df-uz 12739 df-fz 13410 df-struct 17060 df-sets 17077 df-slot 17095 df-ndx 17107 df-base 17123 df-ress 17144 df-plusg 17176 df-mulr 17177 df-sca 17179 df-vsca 17180 df-0g 17347 df-proset 18202 df-poset 18221 df-plt 18236 df-lub 18252 df-glb 18253 df-join 18254 df-meet 18255 df-p0 18331 df-p1 18332 df-lat 18340 df-clat 18407 df-mgm 18550 df-sgrp 18629 df-mnd 18645 df-submnd 18694 df-grp 18851 df-minusg 18852 df-sbg 18853 df-subg 19038 df-cntz 19231 df-lsm 19550 df-cmn 19696 df-abl 19697 df-mgp 20061 df-rng 20073 df-ur 20102 df-ring 20155 df-oppr 20257 df-dvdsr 20277 df-unit 20278 df-invr 20308 df-dvr 20321 df-drng 20648 df-lmod 20797 df-lss 20867 df-lsp 20907 df-lvec 21039 df-lsatoms 39095 df-lshyp 39096 df-lfl 39177 df-lkr 39205 df-ldual 39243 df-oposet 39295 df-ol 39297 df-oml 39298 df-covers 39385 df-ats 39386 df-atl 39417 df-cvlat 39441 df-hlat 39470 df-llines 39617 df-lplanes 39618 df-lvols 39619 df-lines 39620 df-psubsp 39622 df-pmap 39623 df-padd 39915 df-lhyp 40107 df-laut 40108 df-ldil 40223 df-ltrn 40224 df-trl 40278 df-tgrp 40862 df-tendo 40874 df-edring 40876 df-dveca 41122 df-disoa 41148 df-dvech 41198 df-dib 41258 df-dic 41292 df-dih 41348 df-doch 41467 df-djh 41514

This theorem is referenced by: lcfrlem27 41688 lcfrlem37 41698

W3C validator