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 42063

Description: Lemma for lcfr 42090. (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 3896	. . . 4 ⊢ (𝜑 → 𝑋 ∈ 𝐸)
3		lcfrlem16.m	. . . 4 ⊢ 𝐸 = ∪ 𝑔 ∈ 𝐺 ( ⊥ ‘(𝐿‘𝑔))
4	2, 3	eleqtrdi 2851	. . 3 ⊢ (𝜑 → 𝑋 ∈ ∪ 𝑔 ∈ 𝐺 ( ⊥ ‘(𝐿‘𝑔)))
5		eliun 4927	. . 3 ⊢ (𝑋 ∈ ∪ 𝑔 ∈ 𝐺 ( ⊥ ‘(𝐿‘𝑔)) ↔ ∃𝑔 ∈ 𝐺 𝑋 ∈ ( ⊥ ‘(𝐿‘𝑔)))
6	4, 5	sylib 220	. 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 2741	. . . . 5 ⊢ ( ·_𝑠 ‘𝐷) = ( ·_𝑠 ‘𝐷)
13		lcf1o.h	. . . . . . 7 ⊢ 𝐻 = (LHyp‘𝐾)
14		lcf1o.u	. . . . . . 7 ⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊)
15		lcflo.k	. . . . . . 7 ⊢ (𝜑 → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻))
16	13, 14, 15	dvhlvec 41614	. . . . . 6 ⊢ (𝜑 → 𝑈 ∈ LVec)
17	16	3ad2ant1 1140	. . . . 5 ⊢ ((𝜑 ∧ 𝑔 ∈ 𝐺 ∧ 𝑋 ∈ ( ⊥ ‘(𝐿‘𝑔))) → 𝑈 ∈ LVec)
18		lcfrlem16.g	. . . . . . . 8 ⊢ (𝜑 → 𝐺 ∈ 𝑃)
19		eqid 2741	. . . . . . . . 9 ⊢ (Base‘𝐷) = (Base‘𝐷)
20		lcfrlem16.p	. . . . . . . . 9 ⊢ 𝑃 = (LSubSp‘𝐷)
21	19, 20	lssel 20930	. . . . . . . 8 ⊢ ((𝐺 ∈ 𝑃 ∧ 𝑔 ∈ 𝐺) → 𝑔 ∈ (Base‘𝐷))
22	18, 21	sylan 587	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑔 ∈ 𝐺) → 𝑔 ∈ (Base‘𝐷))
23	13, 14, 15	dvhlmod 41615	. . . . . . . . 9 ⊢ (𝜑 → 𝑈 ∈ LMod)
24	9, 11, 19, 23	ldualvbase 39631	. . . . . . . 8 ⊢ (𝜑 → (Base‘𝐷) = 𝐹)
25	24	adantr 482	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑔 ∈ 𝐺) → (Base‘𝐷) = 𝐹)
26	22, 25	eleqtrd 2843	. . . . . 6 ⊢ ((𝜑 ∧ 𝑔 ∈ 𝐺) → 𝑔 ∈ 𝐹)
27	26	3adant3 1139	. . . . 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 482	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑔 ∈ 𝐺) → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻))
37	23	adantr 482	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑔 ∈ 𝐺) → 𝑈 ∈ LMod)
38	29, 9, 10, 37, 26	lkrssv 39601	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑔 ∈ 𝐺) → (𝐿‘𝑔) ⊆ 𝑉)
39	13, 14, 29, 28	dochssv 41860	. . . . . . . . . . . . 13 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝐿‘𝑔) ⊆ 𝑉) → ( ⊥ ‘(𝐿‘𝑔)) ⊆ 𝑉)
40	36, 38, 39	syl2anc 591	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑔 ∈ 𝐺) → ( ⊥ ‘(𝐿‘𝑔)) ⊆ 𝑉)
41	40	ralrimiva 3133	. . . . . . . . . . 11 ⊢ (𝜑 → ∀𝑔 ∈ 𝐺 ( ⊥ ‘(𝐿‘𝑔)) ⊆ 𝑉)
42		iunss 4976	. . . . . . . . . . 11 ⊢ (∪ 𝑔 ∈ 𝐺 ( ⊥ ‘(𝐿‘𝑔)) ⊆ 𝑉 ↔ ∀𝑔 ∈ 𝐺 ( ⊥ ‘(𝐿‘𝑔)) ⊆ 𝑉)
43	41, 42	sylibr 236	. . . . . . . . . 10 ⊢ (𝜑 → ∪ 𝑔 ∈ 𝐺 ( ⊥ ‘(𝐿‘𝑔)) ⊆ 𝑉)
44	3, 43	eqsstrid 3954	. . . . . . . . 9 ⊢ (𝜑 → 𝐸 ⊆ 𝑉)
45	44	ssdifd 4077	. . . . . . . 8 ⊢ (𝜑 → (𝐸 ∖ { 0 }) ⊆ (𝑉 ∖ { 0 }))
46	45, 1	sseldd 3917	. . . . . . 7 ⊢ (𝜑 → 𝑋 ∈ (𝑉 ∖ { 0 }))
47	13, 28, 14, 29, 30, 31, 7, 8, 32, 9, 10, 11, 33, 34, 35, 15, 46	lcfrlem10 42057	. . . . . 6 ⊢ (𝜑 → (𝐽‘𝑋) ∈ 𝐹)
48	47	3ad2ant1 1140	. . . . 5 ⊢ ((𝜑 ∧ 𝑔 ∈ 𝐺 ∧ 𝑋 ∈ ( ⊥ ‘(𝐿‘𝑔))) → (𝐽‘𝑋) ∈ 𝐹)
49		eqid 2741	. . . . . . 7 ⊢ (LSAtoms‘𝑈) = (LSAtoms‘𝑈)
50	15	3ad2ant1 1140	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑔 ∈ 𝐺 ∧ 𝑋 ∈ ( ⊥ ‘(𝐿‘𝑔))) → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻))
51		simp3 1145	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑔 ∈ 𝐺 ∧ 𝑋 ∈ ( ⊥ ‘(𝐿‘𝑔))) → 𝑋 ∈ ( ⊥ ‘(𝐿‘𝑔)))
52		eldifsni 4725	. . . . . . . . . . 11 ⊢ (𝑋 ∈ (𝐸 ∖ { 0 }) → 𝑋 ≠ 0 )
53	1, 52	syl 17	. . . . . . . . . 10 ⊢ (𝜑 → 𝑋 ≠ 0 )
54	53	3ad2ant1 1140	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑔 ∈ 𝐺 ∧ 𝑋 ∈ ( ⊥ ‘(𝐿‘𝑔))) → 𝑋 ≠ 0 )
55		eldifsn 4721	. . . . . . . . 9 ⊢ (𝑋 ∈ (( ⊥ ‘(𝐿‘𝑔)) ∖ { 0 }) ↔ (𝑋 ∈ ( ⊥ ‘(𝐿‘𝑔)) ∧ 𝑋 ≠ 0 ))
56	51, 54, 55	sylanbrc 590	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑔 ∈ 𝐺 ∧ 𝑋 ∈ ( ⊥ ‘(𝐿‘𝑔))) → 𝑋 ∈ (( ⊥ ‘(𝐿‘𝑔)) ∖ { 0 }))
57	13, 28, 14, 29, 32, 9, 10, 50, 27, 56, 49	dochsnkrlem2 41975	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑔 ∈ 𝐺 ∧ 𝑋 ∈ ( ⊥ ‘(𝐿‘𝑔))) → ( ⊥ ‘(𝐿‘𝑔)) ∈ (LSAtoms‘𝑈))
58	13, 28, 14, 29, 30, 31, 7, 8, 32, 9, 10, 11, 33, 34, 35, 15, 46	lcfrlem15 42062	. . . . . . . . . 10 ⊢ (𝜑 → 𝑋 ∈ ( ⊥ ‘(𝐿‘(𝐽‘𝑋))))
59		eldifsn 4721	. . . . . . . . . 10 ⊢ (𝑋 ∈ (( ⊥ ‘(𝐿‘(𝐽‘𝑋))) ∖ { 0 }) ↔ (𝑋 ∈ ( ⊥ ‘(𝐿‘(𝐽‘𝑋))) ∧ 𝑋 ≠ 0 ))
60	58, 53, 59	sylanbrc 590	. . . . . . . . 9 ⊢ (𝜑 → 𝑋 ∈ (( ⊥ ‘(𝐿‘(𝐽‘𝑋))) ∖ { 0 }))
61	13, 28, 14, 29, 32, 9, 10, 15, 47, 60, 49	dochsnkrlem2 41975	. . . . . . . 8 ⊢ (𝜑 → ( ⊥ ‘(𝐿‘(𝐽‘𝑋))) ∈ (LSAtoms‘𝑈))
62	61	3ad2ant1 1140	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑔 ∈ 𝐺 ∧ 𝑋 ∈ ( ⊥ ‘(𝐿‘𝑔))) → ( ⊥ ‘(𝐿‘(𝐽‘𝑋))) ∈ (LSAtoms‘𝑈))
63	58	3ad2ant1 1140	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑔 ∈ 𝐺 ∧ 𝑋 ∈ ( ⊥ ‘(𝐿‘𝑔))) → 𝑋 ∈ ( ⊥ ‘(𝐿‘(𝐽‘𝑋))))
64	32, 49, 17, 57, 62, 54, 51, 63	lsat2el 39512	. . . . . 6 ⊢ ((𝜑 ∧ 𝑔 ∈ 𝐺 ∧ 𝑋 ∈ ( ⊥ ‘(𝐿‘𝑔))) → ( ⊥ ‘(𝐿‘𝑔)) = ( ⊥ ‘(𝐿‘(𝐽‘𝑋))))
65		eqid 2741	. . . . . . 7 ⊢ ((DIsoH‘𝐾)‘𝑊) = ((DIsoH‘𝐾)‘𝑊)
66		lcfrlem16.gs	. . . . . . . . . 10 ⊢ (𝜑 → 𝐺 ⊆ 𝐶)
67	66	3ad2ant1 1140	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑔 ∈ 𝐺 ∧ 𝑋 ∈ ( ⊥ ‘(𝐿‘𝑔))) → 𝐺 ⊆ 𝐶)
68		simp2 1144	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑔 ∈ 𝐺 ∧ 𝑋 ∈ ( ⊥ ‘(𝐿‘𝑔))) → 𝑔 ∈ 𝐺)
69	67, 68	sseldd 3917	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑔 ∈ 𝐺 ∧ 𝑋 ∈ ( ⊥ ‘(𝐿‘𝑔))) → 𝑔 ∈ 𝐶)
70	13, 65, 28, 14, 9, 10, 34, 50, 27	lcfl5 42001	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑔 ∈ 𝐺 ∧ 𝑋 ∈ ( ⊥ ‘(𝐿‘𝑔))) → (𝑔 ∈ 𝐶 ↔ (𝐿‘𝑔) ∈ ran ((DIsoH‘𝐾)‘𝑊)))
71	69, 70	mpbid 234	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑔 ∈ 𝐺 ∧ 𝑋 ∈ ( ⊥ ‘(𝐿‘𝑔))) → (𝐿‘𝑔) ∈ ran ((DIsoH‘𝐾)‘𝑊))
72	13, 28, 14, 29, 30, 31, 7, 8, 32, 9, 10, 11, 33, 34, 35, 15, 46	lcfrlem13 42060	. . . . . . . . . 10 ⊢ (𝜑 → (𝐽‘𝑋) ∈ (𝐶 ∖ {𝑄}))
73	72	eldifad 3896	. . . . . . . . 9 ⊢ (𝜑 → (𝐽‘𝑋) ∈ 𝐶)
74	13, 65, 28, 14, 9, 10, 34, 15, 47	lcfl5 42001	. . . . . . . . 9 ⊢ (𝜑 → ((𝐽‘𝑋) ∈ 𝐶 ↔ (𝐿‘(𝐽‘𝑋)) ∈ ran ((DIsoH‘𝐾)‘𝑊)))
75	73, 74	mpbid 234	. . . . . . . 8 ⊢ (𝜑 → (𝐿‘(𝐽‘𝑋)) ∈ ran ((DIsoH‘𝐾)‘𝑊))
76	75	3ad2ant1 1140	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑔 ∈ 𝐺 ∧ 𝑋 ∈ ( ⊥ ‘(𝐿‘𝑔))) → (𝐿‘(𝐽‘𝑋)) ∈ ran ((DIsoH‘𝐾)‘𝑊))
77	13, 65, 28, 50, 71, 76	doch11 41878	. . . . . 6 ⊢ ((𝜑 ∧ 𝑔 ∈ 𝐺 ∧ 𝑋 ∈ ( ⊥ ‘(𝐿‘𝑔))) → (( ⊥ ‘(𝐿‘𝑔)) = ( ⊥ ‘(𝐿‘(𝐽‘𝑋))) ↔ (𝐿‘𝑔) = (𝐿‘(𝐽‘𝑋))))
78	64, 77	mpbid 234	. . . . 5 ⊢ ((𝜑 ∧ 𝑔 ∈ 𝐺 ∧ 𝑋 ∈ ( ⊥ ‘(𝐿‘𝑔))) → (𝐿‘𝑔) = (𝐿‘(𝐽‘𝑋)))
79	7, 8, 9, 10, 11, 12, 17, 27, 48, 78	eqlkr4 39670	. . . 4 ⊢ ((𝜑 ∧ 𝑔 ∈ 𝐺 ∧ 𝑋 ∈ ( ⊥ ‘(𝐿‘𝑔))) → ∃𝑘 ∈ 𝑅 (𝐽‘𝑋) = (𝑘( ·_𝑠 ‘𝐷)𝑔))
80	23	3ad2ant1 1140	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑔 ∈ 𝐺 ∧ 𝑋 ∈ ( ⊥ ‘(𝐿‘𝑔))) → 𝑈 ∈ LMod)
81	80	adantr 482	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑔 ∈ 𝐺 ∧ 𝑋 ∈ ( ⊥ ‘(𝐿‘𝑔))) ∧ 𝑘 ∈ 𝑅) → 𝑈 ∈ LMod)
82	18	3ad2ant1 1140	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑔 ∈ 𝐺 ∧ 𝑋 ∈ ( ⊥ ‘(𝐿‘𝑔))) → 𝐺 ∈ 𝑃)
83	82	adantr 482	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑔 ∈ 𝐺 ∧ 𝑋 ∈ ( ⊥ ‘(𝐿‘𝑔))) ∧ 𝑘 ∈ 𝑅) → 𝐺 ∈ 𝑃)
84		simpr 486	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑔 ∈ 𝐺 ∧ 𝑋 ∈ ( ⊥ ‘(𝐿‘𝑔))) ∧ 𝑘 ∈ 𝑅) → 𝑘 ∈ 𝑅)
85		simpl2 1200	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑔 ∈ 𝐺 ∧ 𝑋 ∈ ( ⊥ ‘(𝐿‘𝑔))) ∧ 𝑘 ∈ 𝑅) → 𝑔 ∈ 𝐺)
86	7, 8, 11, 12, 20, 81, 83, 84, 85	ldualssvscl 39663	. . . . . 6 ⊢ (((𝜑 ∧ 𝑔 ∈ 𝐺 ∧ 𝑋 ∈ ( ⊥ ‘(𝐿‘𝑔))) ∧ 𝑘 ∈ 𝑅) → (𝑘( ·_𝑠 ‘𝐷)𝑔) ∈ 𝐺)
87		eleq1 2829	. . . . . 6 ⊢ ((𝐽‘𝑋) = (𝑘( ·_𝑠 ‘𝐷)𝑔) → ((𝐽‘𝑋) ∈ 𝐺 ↔ (𝑘( ·_𝑠 ‘𝐷)𝑔) ∈ 𝐺))
88	86, 87	syl5ibrcom 249	. . . . 5 ⊢ (((𝜑 ∧ 𝑔 ∈ 𝐺 ∧ 𝑋 ∈ ( ⊥ ‘(𝐿‘𝑔))) ∧ 𝑘 ∈ 𝑅) → ((𝐽‘𝑋) = (𝑘( ·_𝑠 ‘𝐷)𝑔) → (𝐽‘𝑋) ∈ 𝐺))
89	88	rexlimdva 3142	. . . 4 ⊢ ((𝜑 ∧ 𝑔 ∈ 𝐺 ∧ 𝑋 ∈ ( ⊥ ‘(𝐿‘𝑔))) → (∃𝑘 ∈ 𝑅 (𝐽‘𝑋) = (𝑘( ·_𝑠 ‘𝐷)𝑔) → (𝐽‘𝑋) ∈ 𝐺))
90	79, 89	mpd 15	. . 3 ⊢ ((𝜑 ∧ 𝑔 ∈ 𝐺 ∧ 𝑋 ∈ ( ⊥ ‘(𝐿‘𝑔))) → (𝐽‘𝑋) ∈ 𝐺)
91	90	rexlimdv3a 3146	. 2 ⊢ (𝜑 → (∃𝑔 ∈ 𝐺 𝑋 ∈ ( ⊥ ‘(𝐿‘𝑔)) → (𝐽‘𝑋) ∈ 𝐺))
92	6, 91	mpd 15	1 ⊢ (𝜑 → (𝐽‘𝑋) ∈ 𝐺)

Colors of variables: wff setvar class

Syntax hints: → wi 4 ∧ wa 397 ∧ w3a 1093 = wceq 1548 ∈ wcel 2121 ≠ wne 2936 ∀wral 3055 ∃wrex 3065 {crab 3393 ∖ cdif 3881 ⊆ wss 3884 {csn 4557 ∪ ciun 4923 ↦ cmpt 5155 ran crn 5621 ‘cfv 6488 ℩crio 7315 (class class class)co 7359 Basecbs 17174 +_gcplusg 17215 Scalarcsca 17218 ·_𝑠 cvsca 17219 0_gc0g 17397 LModclmod 20853 LSubSpclss 20924 LVecclvec 21095 LSAtomsclsa 39479 LFnlclfn 39562 LKerclk 39590 LDualcld 39628 HLchlt 39855 LHypclh 40489 DVecHcdvh 41583 DIsoHcdih 41733 ocHcoch 41852

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1803 ax-4 1817 ax-5 1918 ax-6 1975 ax-7 2016 ax-8 2123 ax-9 2131 ax-10 2154 ax-11 2170 ax-12 2191 ax-ext 2713 ax-rep 5201 ax-sep 5220 ax-nul 5230 ax-pow 5296 ax-pr 5364 ax-un 7681 ax-cnex 11090 ax-resscn 11091 ax-1cn 11092 ax-icn 11093 ax-addcl 11094 ax-addrcl 11095 ax-mulcl 11096 ax-mulrcl 11097 ax-mulcom 11098 ax-addass 11099 ax-mulass 11100 ax-distr 11101 ax-i2m1 11102 ax-1ne0 11103 ax-1rid 11104 ax-rnegex 11105 ax-rrecex 11106 ax-cnre 11107 ax-pre-lttri 11108 ax-pre-lttrn 11109 ax-pre-ltadd 11110 ax-pre-mulgt0 11111 ax-riotaBAD 39458

This theorem depends on definitions: df-bi 209 df-an 398 df-or 855 df-3or 1094 df-3an 1095 df-tru 1551 df-fal 1561 df-ex 1788 df-nf 1792 df-sb 2075 df-mo 2545 df-eu 2575 df-clab 2720 df-cleq 2733 df-clel 2816 df-nfc 2890 df-ne 2937 df-nel 3041 df-ral 3056 df-rex 3066 df-rmo 3346 df-reu 3347 df-rab 3394 df-v 3435 df-sbc 3725 df-csb 3833 df-dif 3887 df-un 3889 df-in 3891 df-ss 3901 df-pss 3904 df-nul 4264 df-if 4457 df-pw 4533 df-sn 4558 df-pr 4560 df-tp 4562 df-op 4564 df-uni 4841 df-int 4880 df-iun 4925 df-iin 4926 df-br 5075 df-opab 5137 df-mpt 5156 df-tr 5182 df-id 5515 df-eprel 5520 df-po 5528 df-so 5529 df-fr 5573 df-we 5575 df-xp 5626 df-rel 5627 df-cnv 5628 df-co 5629 df-dm 5630 df-rn 5631 df-res 5632 df-ima 5633 df-pred 6255 df-ord 6316 df-on 6317 df-lim 6318 df-suc 6319 df-iota 6444 df-fun 6490 df-fn 6491 df-f 6492 df-f1 6493 df-fo 6494 df-f1o 6495 df-fv 6496 df-riota 7316 df-ov 7362 df-oprab 7363 df-mpo 7364 df-of 7623 df-om 7810 df-1st 7933 df-2nd 7934 df-tpos 8168 df-undef 8215 df-frecs 8224 df-wrecs 8255 df-recs 8304 df-rdg 8343 df-1o 8399 df-er 8637 df-map 8769 df-en 8888 df-dom 8889 df-sdom 8890 df-fin 8891 df-pnf 11177 df-mnf 11178 df-xr 11179 df-ltxr 11180 df-le 11181 df-sub 11375 df-neg 11376 df-nn 12170 df-2 12239 df-3 12240 df-4 12241 df-5 12242 df-6 12243 df-n0 12433 df-z 12520 df-uz 12784 df-fz 13457 df-struct 17112 df-sets 17129 df-slot 17147 df-ndx 17159 df-base 17175 df-ress 17196 df-plusg 17228 df-mulr 17229 df-sca 17231 df-vsca 17232 df-0g 17399 df-proset 18255 df-poset 18274 df-plt 18289 df-lub 18305 df-glb 18306 df-join 18307 df-meet 18308 df-p0 18384 df-p1 18385 df-lat 18393 df-clat 18460 df-mgm 18603 df-sgrp 18682 df-mnd 18698 df-submnd 18747 df-grp 18907 df-minusg 18908 df-sbg 18909 df-subg 19094 df-cntz 19286 df-lsm 19605 df-cmn 19751 df-abl 19752 df-mgp 20116 df-rng 20128 df-ur 20157 df-ring 20210 df-oppr 20311 df-dvdsr 20331 df-unit 20332 df-invr 20362 df-dvr 20375 df-drng 20706 df-lmod 20855 df-lss 20925 df-lsp 20965 df-lvec 21096 df-lsatoms 39481 df-lshyp 39482 df-lfl 39563 df-lkr 39591 df-ldual 39629 df-oposet 39681 df-ol 39683 df-oml 39684 df-covers 39771 df-ats 39772 df-atl 39803 df-cvlat 39827 df-hlat 39856 df-llines 40003 df-lplanes 40004 df-lvols 40005 df-lines 40006 df-psubsp 40008 df-pmap 40009 df-padd 40301 df-lhyp 40493 df-laut 40494 df-ldil 40609 df-ltrn 40610 df-trl 40664 df-tgrp 41248 df-tendo 41260 df-edring 41262 df-dveca 41508 df-disoa 41534 df-dvech 41584 df-dib 41644 df-dic 41678 df-dih 41734 df-doch 41853 df-djh 41900

This theorem is referenced by: lcfrlem27 42074 lcfrlem37 42084

W3C validator