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 41814

Description: Lemma for lcfr 41841. (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 3913	. . . 4 ⊢ (𝜑 → 𝑋 ∈ 𝐸)
3		lcfrlem16.m	. . . 4 ⊢ 𝐸 = ∪ 𝑔 ∈ 𝐺 ( ⊥ ‘(𝐿‘𝑔))
4	2, 3	eleqtrdi 2846	. . 3 ⊢ (𝜑 → 𝑋 ∈ ∪ 𝑔 ∈ 𝐺 ( ⊥ ‘(𝐿‘𝑔)))
5		eliun 4950	. . 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 2736	. . . . 5 ⊢ ( ·_𝑠 ‘𝐷) = ( ·_𝑠 ‘𝐷)
13		lcf1o.h	. . . . . . 7 ⊢ 𝐻 = (LHyp‘𝐾)
14		lcf1o.u	. . . . . . 7 ⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊)
15		lcflo.k	. . . . . . 7 ⊢ (𝜑 → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻))
16	13, 14, 15	dvhlvec 41365	. . . . . 6 ⊢ (𝜑 → 𝑈 ∈ LVec)
17	16	3ad2ant1 1133	. . . . 5 ⊢ ((𝜑 ∧ 𝑔 ∈ 𝐺 ∧ 𝑋 ∈ ( ⊥ ‘(𝐿‘𝑔))) → 𝑈 ∈ LVec)
18		lcfrlem16.g	. . . . . . . 8 ⊢ (𝜑 → 𝐺 ∈ 𝑃)
19		eqid 2736	. . . . . . . . 9 ⊢ (Base‘𝐷) = (Base‘𝐷)
20		lcfrlem16.p	. . . . . . . . 9 ⊢ 𝑃 = (LSubSp‘𝐷)
21	19, 20	lssel 20888	. . . . . . . 8 ⊢ ((𝐺 ∈ 𝑃 ∧ 𝑔 ∈ 𝐺) → 𝑔 ∈ (Base‘𝐷))
22	18, 21	sylan 580	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑔 ∈ 𝐺) → 𝑔 ∈ (Base‘𝐷))
23	13, 14, 15	dvhlmod 41366	. . . . . . . . 9 ⊢ (𝜑 → 𝑈 ∈ LMod)
24	9, 11, 19, 23	ldualvbase 39382	. . . . . . . 8 ⊢ (𝜑 → (Base‘𝐷) = 𝐹)
25	24	adantr 480	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑔 ∈ 𝐺) → (Base‘𝐷) = 𝐹)
26	22, 25	eleqtrd 2838	. . . . . 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 39352	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑔 ∈ 𝐺) → (𝐿‘𝑔) ⊆ 𝑉)
39	13, 14, 29, 28	dochssv 41611	. . . . . . . . . . . . 13 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝐿‘𝑔) ⊆ 𝑉) → ( ⊥ ‘(𝐿‘𝑔)) ⊆ 𝑉)
40	36, 38, 39	syl2anc 584	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑔 ∈ 𝐺) → ( ⊥ ‘(𝐿‘𝑔)) ⊆ 𝑉)
41	40	ralrimiva 3128	. . . . . . . . . . 11 ⊢ (𝜑 → ∀𝑔 ∈ 𝐺 ( ⊥ ‘(𝐿‘𝑔)) ⊆ 𝑉)
42		iunss 5000	. . . . . . . . . . 11 ⊢ (∪ 𝑔 ∈ 𝐺 ( ⊥ ‘(𝐿‘𝑔)) ⊆ 𝑉 ↔ ∀𝑔 ∈ 𝐺 ( ⊥ ‘(𝐿‘𝑔)) ⊆ 𝑉)
43	41, 42	sylibr 234	. . . . . . . . . 10 ⊢ (𝜑 → ∪ 𝑔 ∈ 𝐺 ( ⊥ ‘(𝐿‘𝑔)) ⊆ 𝑉)
44	3, 43	eqsstrid 3972	. . . . . . . . 9 ⊢ (𝜑 → 𝐸 ⊆ 𝑉)
45	44	ssdifd 4097	. . . . . . . 8 ⊢ (𝜑 → (𝐸 ∖ { 0 }) ⊆ (𝑉 ∖ { 0 }))
46	45, 1	sseldd 3934	. . . . . . 7 ⊢ (𝜑 → 𝑋 ∈ (𝑉 ∖ { 0 }))
47	13, 28, 14, 29, 30, 31, 7, 8, 32, 9, 10, 11, 33, 34, 35, 15, 46	lcfrlem10 41808	. . . . . 6 ⊢ (𝜑 → (𝐽‘𝑋) ∈ 𝐹)
48	47	3ad2ant1 1133	. . . . 5 ⊢ ((𝜑 ∧ 𝑔 ∈ 𝐺 ∧ 𝑋 ∈ ( ⊥ ‘(𝐿‘𝑔))) → (𝐽‘𝑋) ∈ 𝐹)
49		eqid 2736	. . . . . . 7 ⊢ (LSAtoms‘𝑈) = (LSAtoms‘𝑈)
50	15	3ad2ant1 1133	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑔 ∈ 𝐺 ∧ 𝑋 ∈ ( ⊥ ‘(𝐿‘𝑔))) → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻))
51		simp3 1138	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑔 ∈ 𝐺 ∧ 𝑋 ∈ ( ⊥ ‘(𝐿‘𝑔))) → 𝑋 ∈ ( ⊥ ‘(𝐿‘𝑔)))
52		eldifsni 4746	. . . . . . . . . . 11 ⊢ (𝑋 ∈ (𝐸 ∖ { 0 }) → 𝑋 ≠ 0 )
53	1, 52	syl 17	. . . . . . . . . 10 ⊢ (𝜑 → 𝑋 ≠ 0 )
54	53	3ad2ant1 1133	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑔 ∈ 𝐺 ∧ 𝑋 ∈ ( ⊥ ‘(𝐿‘𝑔))) → 𝑋 ≠ 0 )
55		eldifsn 4742	. . . . . . . . 9 ⊢ (𝑋 ∈ (( ⊥ ‘(𝐿‘𝑔)) ∖ { 0 }) ↔ (𝑋 ∈ ( ⊥ ‘(𝐿‘𝑔)) ∧ 𝑋 ≠ 0 ))
56	51, 54, 55	sylanbrc 583	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑔 ∈ 𝐺 ∧ 𝑋 ∈ ( ⊥ ‘(𝐿‘𝑔))) → 𝑋 ∈ (( ⊥ ‘(𝐿‘𝑔)) ∖ { 0 }))
57	13, 28, 14, 29, 32, 9, 10, 50, 27, 56, 49	dochsnkrlem2 41726	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑔 ∈ 𝐺 ∧ 𝑋 ∈ ( ⊥ ‘(𝐿‘𝑔))) → ( ⊥ ‘(𝐿‘𝑔)) ∈ (LSAtoms‘𝑈))
58	13, 28, 14, 29, 30, 31, 7, 8, 32, 9, 10, 11, 33, 34, 35, 15, 46	lcfrlem15 41813	. . . . . . . . . 10 ⊢ (𝜑 → 𝑋 ∈ ( ⊥ ‘(𝐿‘(𝐽‘𝑋))))
59		eldifsn 4742	. . . . . . . . . 10 ⊢ (𝑋 ∈ (( ⊥ ‘(𝐿‘(𝐽‘𝑋))) ∖ { 0 }) ↔ (𝑋 ∈ ( ⊥ ‘(𝐿‘(𝐽‘𝑋))) ∧ 𝑋 ≠ 0 ))
60	58, 53, 59	sylanbrc 583	. . . . . . . . 9 ⊢ (𝜑 → 𝑋 ∈ (( ⊥ ‘(𝐿‘(𝐽‘𝑋))) ∖ { 0 }))
61	13, 28, 14, 29, 32, 9, 10, 15, 47, 60, 49	dochsnkrlem2 41726	. . . . . . . 8 ⊢ (𝜑 → ( ⊥ ‘(𝐿‘(𝐽‘𝑋))) ∈ (LSAtoms‘𝑈))
62	61	3ad2ant1 1133	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑔 ∈ 𝐺 ∧ 𝑋 ∈ ( ⊥ ‘(𝐿‘𝑔))) → ( ⊥ ‘(𝐿‘(𝐽‘𝑋))) ∈ (LSAtoms‘𝑈))
63	58	3ad2ant1 1133	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑔 ∈ 𝐺 ∧ 𝑋 ∈ ( ⊥ ‘(𝐿‘𝑔))) → 𝑋 ∈ ( ⊥ ‘(𝐿‘(𝐽‘𝑋))))
64	32, 49, 17, 57, 62, 54, 51, 63	lsat2el 39263	. . . . . 6 ⊢ ((𝜑 ∧ 𝑔 ∈ 𝐺 ∧ 𝑋 ∈ ( ⊥ ‘(𝐿‘𝑔))) → ( ⊥ ‘(𝐿‘𝑔)) = ( ⊥ ‘(𝐿‘(𝐽‘𝑋))))
65		eqid 2736	. . . . . . 7 ⊢ ((DIsoH‘𝐾)‘𝑊) = ((DIsoH‘𝐾)‘𝑊)
66		lcfrlem16.gs	. . . . . . . . . 10 ⊢ (𝜑 → 𝐺 ⊆ 𝐶)
67	66	3ad2ant1 1133	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑔 ∈ 𝐺 ∧ 𝑋 ∈ ( ⊥ ‘(𝐿‘𝑔))) → 𝐺 ⊆ 𝐶)
68		simp2 1137	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑔 ∈ 𝐺 ∧ 𝑋 ∈ ( ⊥ ‘(𝐿‘𝑔))) → 𝑔 ∈ 𝐺)
69	67, 68	sseldd 3934	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑔 ∈ 𝐺 ∧ 𝑋 ∈ ( ⊥ ‘(𝐿‘𝑔))) → 𝑔 ∈ 𝐶)
70	13, 65, 28, 14, 9, 10, 34, 50, 27	lcfl5 41752	. . . . . . . 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 41811	. . . . . . . . . 10 ⊢ (𝜑 → (𝐽‘𝑋) ∈ (𝐶 ∖ {𝑄}))
73	72	eldifad 3913	. . . . . . . . 9 ⊢ (𝜑 → (𝐽‘𝑋) ∈ 𝐶)
74	13, 65, 28, 14, 9, 10, 34, 15, 47	lcfl5 41752	. . . . . . . . 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 41629	. . . . . 6 ⊢ ((𝜑 ∧ 𝑔 ∈ 𝐺 ∧ 𝑋 ∈ ( ⊥ ‘(𝐿‘𝑔))) → (( ⊥ ‘(𝐿‘𝑔)) = ( ⊥ ‘(𝐿‘(𝐽‘𝑋))) ↔ (𝐿‘𝑔) = (𝐿‘(𝐽‘𝑋))))
78	64, 77	mpbid 232	. . . . 5 ⊢ ((𝜑 ∧ 𝑔 ∈ 𝐺 ∧ 𝑋 ∈ ( ⊥ ‘(𝐿‘𝑔))) → (𝐿‘𝑔) = (𝐿‘(𝐽‘𝑋)))
79	7, 8, 9, 10, 11, 12, 17, 27, 48, 78	eqlkr4 39421	. . . 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 39414	. . . . . 6 ⊢ (((𝜑 ∧ 𝑔 ∈ 𝐺 ∧ 𝑋 ∈ ( ⊥ ‘(𝐿‘𝑔))) ∧ 𝑘 ∈ 𝑅) → (𝑘( ·_𝑠 ‘𝐷)𝑔) ∈ 𝐺)
87		eleq1 2824	. . . . . 6 ⊢ ((𝐽‘𝑋) = (𝑘( ·_𝑠 ‘𝐷)𝑔) → ((𝐽‘𝑋) ∈ 𝐺 ↔ (𝑘( ·_𝑠 ‘𝐷)𝑔) ∈ 𝐺))
88	86, 87	syl5ibrcom 247	. . . . 5 ⊢ (((𝜑 ∧ 𝑔 ∈ 𝐺 ∧ 𝑋 ∈ ( ⊥ ‘(𝐿‘𝑔))) ∧ 𝑘 ∈ 𝑅) → ((𝐽‘𝑋) = (𝑘( ·_𝑠 ‘𝐷)𝑔) → (𝐽‘𝑋) ∈ 𝐺))
89	88	rexlimdva 3137	. . . 4 ⊢ ((𝜑 ∧ 𝑔 ∈ 𝐺 ∧ 𝑋 ∈ ( ⊥ ‘(𝐿‘𝑔))) → (∃𝑘 ∈ 𝑅 (𝐽‘𝑋) = (𝑘( ·_𝑠 ‘𝐷)𝑔) → (𝐽‘𝑋) ∈ 𝐺))
90	79, 89	mpd 15	. . 3 ⊢ ((𝜑 ∧ 𝑔 ∈ 𝐺 ∧ 𝑋 ∈ ( ⊥ ‘(𝐿‘𝑔))) → (𝐽‘𝑋) ∈ 𝐺)
91	90	rexlimdv3a 3141	. 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 2932 ∀wral 3051 ∃wrex 3060 {crab 3399 ∖ cdif 3898 ⊆ wss 3901 {csn 4580 ∪ ciun 4946 ↦ cmpt 5179 ran crn 5625 ‘cfv 6492 ℩crio 7314 (class class class)co 7358 Basecbs 17136 +_gcplusg 17177 Scalarcsca 17180 ·_𝑠 cvsca 17181 0_gc0g 17359 LModclmod 20811 LSubSpclss 20882 LVecclvec 21054 LSAtomsclsa 39230 LFnlclfn 39313 LKerclk 39341 LDualcld 39379 HLchlt 39606 LHypclh 40240 DVecHcdvh 41334 DIsoHcdih 41484 ocHcoch 41603

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 2184 ax-ext 2708 ax-rep 5224 ax-sep 5241 ax-nul 5251 ax-pow 5310 ax-pr 5377 ax-un 7680 ax-cnex 11082 ax-resscn 11083 ax-1cn 11084 ax-icn 11085 ax-addcl 11086 ax-addrcl 11087 ax-mulcl 11088 ax-mulrcl 11089 ax-mulcom 11090 ax-addass 11091 ax-mulass 11092 ax-distr 11093 ax-i2m1 11094 ax-1ne0 11095 ax-1rid 11096 ax-rnegex 11097 ax-rrecex 11098 ax-cnre 11099 ax-pre-lttri 11100 ax-pre-lttrn 11101 ax-pre-ltadd 11102 ax-pre-mulgt0 11103 ax-riotaBAD 39209

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 2539 df-eu 2569 df-clab 2715 df-cleq 2728 df-clel 2811 df-nfc 2885 df-ne 2933 df-nel 3037 df-ral 3052 df-rex 3061 df-rmo 3350 df-reu 3351 df-rab 3400 df-v 3442 df-sbc 3741 df-csb 3850 df-dif 3904 df-un 3906 df-in 3908 df-ss 3918 df-pss 3921 df-nul 4286 df-if 4480 df-pw 4556 df-sn 4581 df-pr 4583 df-tp 4585 df-op 4587 df-uni 4864 df-int 4903 df-iun 4948 df-iin 4949 df-br 5099 df-opab 5161 df-mpt 5180 df-tr 5206 df-id 5519 df-eprel 5524 df-po 5532 df-so 5533 df-fr 5577 df-we 5579 df-xp 5630 df-rel 5631 df-cnv 5632 df-co 5633 df-dm 5634 df-rn 5635 df-res 5636 df-ima 5637 df-pred 6259 df-ord 6320 df-on 6321 df-lim 6322 df-suc 6323 df-iota 6448 df-fun 6494 df-fn 6495 df-f 6496 df-f1 6497 df-fo 6498 df-f1o 6499 df-fv 6500 df-riota 7315 df-ov 7361 df-oprab 7362 df-mpo 7363 df-of 7622 df-om 7809 df-1st 7933 df-2nd 7934 df-tpos 8168 df-undef 8215 df-frecs 8223 df-wrecs 8254 df-recs 8303 df-rdg 8341 df-1o 8397 df-er 8635 df-map 8765 df-en 8884 df-dom 8885 df-sdom 8886 df-fin 8887 df-pnf 11168 df-mnf 11169 df-xr 11170 df-ltxr 11171 df-le 11172 df-sub 11366 df-neg 11367 df-nn 12146 df-2 12208 df-3 12209 df-4 12210 df-5 12211 df-6 12212 df-n0 12402 df-z 12489 df-uz 12752 df-fz 13424 df-struct 17074 df-sets 17091 df-slot 17109 df-ndx 17121 df-base 17137 df-ress 17158 df-plusg 17190 df-mulr 17191 df-sca 17193 df-vsca 17194 df-0g 17361 df-proset 18217 df-poset 18236 df-plt 18251 df-lub 18267 df-glb 18268 df-join 18269 df-meet 18270 df-p0 18346 df-p1 18347 df-lat 18355 df-clat 18422 df-mgm 18565 df-sgrp 18644 df-mnd 18660 df-submnd 18709 df-grp 18866 df-minusg 18867 df-sbg 18868 df-subg 19053 df-cntz 19246 df-lsm 19565 df-cmn 19711 df-abl 19712 df-mgp 20076 df-rng 20088 df-ur 20117 df-ring 20170 df-oppr 20273 df-dvdsr 20293 df-unit 20294 df-invr 20324 df-dvr 20337 df-drng 20664 df-lmod 20813 df-lss 20883 df-lsp 20923 df-lvec 21055 df-lsatoms 39232 df-lshyp 39233 df-lfl 39314 df-lkr 39342 df-ldual 39380 df-oposet 39432 df-ol 39434 df-oml 39435 df-covers 39522 df-ats 39523 df-atl 39554 df-cvlat 39578 df-hlat 39607 df-llines 39754 df-lplanes 39755 df-lvols 39756 df-lines 39757 df-psubsp 39759 df-pmap 39760 df-padd 40052 df-lhyp 40244 df-laut 40245 df-ldil 40360 df-ltrn 40361 df-trl 40415 df-tgrp 40999 df-tendo 41011 df-edring 41013 df-dveca 41259 df-disoa 41285 df-dvech 41335 df-dib 41395 df-dic 41429 df-dih 41485 df-doch 41604 df-djh 41651

This theorem is referenced by: lcfrlem27 41825 lcfrlem37 41835

W3C validator