lindsadd - Mathbox for Brendan Leahy

	Mathbox for Brendan Leahy		< Previous Next > Nearby theorems
Mirrors > Home > MPE Home > Th. List > Mathboxes > lindsadd		Structured version Visualization version GIF version

Theorem lindsadd 38072

Description: In a vector space, the union of an independent set and a vector not in its span is an independent set. (Contributed by Brendan Leahy, 4-Mar-2023.)

**Assertion**
Ref	Expression
lindsadd	⊢ ((𝑊 ∈ LVec ∧ 𝐹 ∈ (LIndS‘𝑊) ∧ 𝑋 ∈ ((Base‘𝑊) ∖ ((LSpan‘𝑊)‘𝐹))) → (𝐹 ∪ {𝑋}) ∈ (LIndS‘𝑊))

Proof of Theorem lindsadd Dummy variables 𝑥 𝑘 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		eqid 2761	. . . . 5 ⊢ (Base‘𝑊) = (Base‘𝑊)
2	1	linds1 21849	. . . 4 ⊢ (𝐹 ∈ (LIndS‘𝑊) → 𝐹 ⊆ (Base‘𝑊))
3		eldifi 4082	. . . . 5 ⊢ (𝑋 ∈ ((Base‘𝑊) ∖ ((LSpan‘𝑊)‘𝐹)) → 𝑋 ∈ (Base‘𝑊))
4	3	snssd 4742	. . . 4 ⊢ (𝑋 ∈ ((Base‘𝑊) ∖ ((LSpan‘𝑊)‘𝐹)) → {𝑋} ⊆ (Base‘𝑊))
5		unss 4140	. . . . 5 ⊢ ((𝐹 ⊆ (Base‘𝑊) ∧ {𝑋} ⊆ (Base‘𝑊)) ↔ (𝐹 ∪ {𝑋}) ⊆ (Base‘𝑊))
6	5	biimpi 218	. . . 4 ⊢ ((𝐹 ⊆ (Base‘𝑊) ∧ {𝑋} ⊆ (Base‘𝑊)) → (𝐹 ∪ {𝑋}) ⊆ (Base‘𝑊))
7	2, 4, 6	syl2an 605	. . 3 ⊢ ((𝐹 ∈ (LIndS‘𝑊) ∧ 𝑋 ∈ ((Base‘𝑊) ∖ ((LSpan‘𝑊)‘𝐹))) → (𝐹 ∪ {𝑋}) ⊆ (Base‘𝑊))
8	7	3adant1 1142	. 2 ⊢ ((𝑊 ∈ LVec ∧ 𝐹 ∈ (LIndS‘𝑊) ∧ 𝑋 ∈ ((Base‘𝑊) ∖ ((LSpan‘𝑊)‘𝐹))) → (𝐹 ∪ {𝑋}) ⊆ (Base‘𝑊))
9		eldifn 4083	. . . . . . 7 ⊢ (𝑋 ∈ ((Base‘𝑊) ∖ ((LSpan‘𝑊)‘𝐹)) → ¬ 𝑋 ∈ ((LSpan‘𝑊)‘𝐹))
10	9	3ad2ant3 1147	. . . . . 6 ⊢ ((𝑊 ∈ LVec ∧ 𝐹 ∈ (LIndS‘𝑊) ∧ 𝑋 ∈ ((Base‘𝑊) ∖ ((LSpan‘𝑊)‘𝐹))) → ¬ 𝑋 ∈ ((LSpan‘𝑊)‘𝐹))
11	10	adantr 484	. . . . 5 ⊢ (((𝑊 ∈ LVec ∧ 𝐹 ∈ (LIndS‘𝑊) ∧ 𝑋 ∈ ((Base‘𝑊) ∖ ((LSpan‘𝑊)‘𝐹))) ∧ (𝑥 ∈ 𝐹 ∧ 𝑘 ∈ ((Base‘(Scalar‘𝑊)) ∖ {(0_g‘(Scalar‘𝑊))}))) → ¬ 𝑋 ∈ ((LSpan‘𝑊)‘𝐹))
12		simpll1 1225	. . . . . . . 8 ⊢ ((((𝑊 ∈ LVec ∧ 𝐹 ∈ (LIndS‘𝑊) ∧ 𝑋 ∈ ((Base‘𝑊) ∖ ((LSpan‘𝑊)‘𝐹))) ∧ (𝑥 ∈ 𝐹 ∧ 𝑘 ∈ ((Base‘(Scalar‘𝑊)) ∖ {(0_g‘(Scalar‘𝑊))}))) ∧ 𝑥 ∈ ((LSpan‘𝑊)‘((𝐹 ∖ {𝑥}) ∪ {𝑋}))) → 𝑊 ∈ LVec)
13	2	ssdifssd 4098	. . . . . . . . . 10 ⊢ (𝐹 ∈ (LIndS‘𝑊) → (𝐹 ∖ {𝑥}) ⊆ (Base‘𝑊))
14	13	3ad2ant2 1146	. . . . . . . . 9 ⊢ ((𝑊 ∈ LVec ∧ 𝐹 ∈ (LIndS‘𝑊) ∧ 𝑋 ∈ ((Base‘𝑊) ∖ ((LSpan‘𝑊)‘𝐹))) → (𝐹 ∖ {𝑥}) ⊆ (Base‘𝑊))
15	14	ad2antrr 736	. . . . . . . 8 ⊢ ((((𝑊 ∈ LVec ∧ 𝐹 ∈ (LIndS‘𝑊) ∧ 𝑋 ∈ ((Base‘𝑊) ∖ ((LSpan‘𝑊)‘𝐹))) ∧ (𝑥 ∈ 𝐹 ∧ 𝑘 ∈ ((Base‘(Scalar‘𝑊)) ∖ {(0_g‘(Scalar‘𝑊))}))) ∧ 𝑥 ∈ ((LSpan‘𝑊)‘((𝐹 ∖ {𝑥}) ∪ {𝑋}))) → (𝐹 ∖ {𝑥}) ⊆ (Base‘𝑊))
16	3	3ad2ant3 1147	. . . . . . . . 9 ⊢ ((𝑊 ∈ LVec ∧ 𝐹 ∈ (LIndS‘𝑊) ∧ 𝑋 ∈ ((Base‘𝑊) ∖ ((LSpan‘𝑊)‘𝐹))) → 𝑋 ∈ (Base‘𝑊))
17	16	ad2antrr 736	. . . . . . . 8 ⊢ ((((𝑊 ∈ LVec ∧ 𝐹 ∈ (LIndS‘𝑊) ∧ 𝑋 ∈ ((Base‘𝑊) ∖ ((LSpan‘𝑊)‘𝐹))) ∧ (𝑥 ∈ 𝐹 ∧ 𝑘 ∈ ((Base‘(Scalar‘𝑊)) ∖ {(0_g‘(Scalar‘𝑊))}))) ∧ 𝑥 ∈ ((LSpan‘𝑊)‘((𝐹 ∖ {𝑥}) ∪ {𝑋}))) → 𝑋 ∈ (Base‘𝑊))
18		simpr 488	. . . . . . . . 9 ⊢ ((((𝑊 ∈ LVec ∧ 𝐹 ∈ (LIndS‘𝑊) ∧ 𝑋 ∈ ((Base‘𝑊) ∖ ((LSpan‘𝑊)‘𝐹))) ∧ (𝑥 ∈ 𝐹 ∧ 𝑘 ∈ ((Base‘(Scalar‘𝑊)) ∖ {(0_g‘(Scalar‘𝑊))}))) ∧ 𝑥 ∈ ((LSpan‘𝑊)‘((𝐹 ∖ {𝑥}) ∪ {𝑋}))) → 𝑥 ∈ ((LSpan‘𝑊)‘((𝐹 ∖ {𝑥}) ∪ {𝑋})))
19		lveclmod 21160	. . . . . . . . . . . . 13 ⊢ (𝑊 ∈ LVec → 𝑊 ∈ LMod)
20	19	ad2antrr 736	. . . . . . . . . . . 12 ⊢ (((𝑊 ∈ LVec ∧ 𝐹 ∈ (LIndS‘𝑊)) ∧ (𝑥 ∈ 𝐹 ∧ 𝑘 ∈ ((Base‘(Scalar‘𝑊)) ∖ {(0_g‘(Scalar‘𝑊))}))) → 𝑊 ∈ LMod)
21		eqid 2761	. . . . . . . . . . . . . . . 16 ⊢ (Scalar‘𝑊) = (Scalar‘𝑊)
22	21	lmodring 20922	. . . . . . . . . . . . . . 15 ⊢ (𝑊 ∈ LMod → (Scalar‘𝑊) ∈ Ring)
23	19, 22	syl 17	. . . . . . . . . . . . . 14 ⊢ (𝑊 ∈ LVec → (Scalar‘𝑊) ∈ Ring)
24		eqid 2761	. . . . . . . . . . . . . . 15 ⊢ (0_g‘(Scalar‘𝑊)) = (0_g‘(Scalar‘𝑊))
25		eqid 2761	. . . . . . . . . . . . . . 15 ⊢ (Base‘(Scalar‘𝑊)) = (Base‘(Scalar‘𝑊))
26	24, 25	ringelnzr 20559	. . . . . . . . . . . . . 14 ⊢ (((Scalar‘𝑊) ∈ Ring ∧ 𝑘 ∈ ((Base‘(Scalar‘𝑊)) ∖ {(0_g‘(Scalar‘𝑊))})) → (Scalar‘𝑊) ∈ NzRing)
27	23, 26	sylan 589	. . . . . . . . . . . . 13 ⊢ ((𝑊 ∈ LVec ∧ 𝑘 ∈ ((Base‘(Scalar‘𝑊)) ∖ {(0_g‘(Scalar‘𝑊))})) → (Scalar‘𝑊) ∈ NzRing)
28	27	ad2ant2rl 759	. . . . . . . . . . . 12 ⊢ (((𝑊 ∈ LVec ∧ 𝐹 ∈ (LIndS‘𝑊)) ∧ (𝑥 ∈ 𝐹 ∧ 𝑘 ∈ ((Base‘(Scalar‘𝑊)) ∖ {(0_g‘(Scalar‘𝑊))}))) → (Scalar‘𝑊) ∈ NzRing)
29		simplr 778	. . . . . . . . . . . 12 ⊢ (((𝑊 ∈ LVec ∧ 𝐹 ∈ (LIndS‘𝑊)) ∧ (𝑥 ∈ 𝐹 ∧ 𝑘 ∈ ((Base‘(Scalar‘𝑊)) ∖ {(0_g‘(Scalar‘𝑊))}))) → 𝐹 ∈ (LIndS‘𝑊))
30		simprl 780	. . . . . . . . . . . 12 ⊢ (((𝑊 ∈ LVec ∧ 𝐹 ∈ (LIndS‘𝑊)) ∧ (𝑥 ∈ 𝐹 ∧ 𝑘 ∈ ((Base‘(Scalar‘𝑊)) ∖ {(0_g‘(Scalar‘𝑊))}))) → 𝑥 ∈ 𝐹)
31		eqid 2761	. . . . . . . . . . . . 13 ⊢ (LSpan‘𝑊) = (LSpan‘𝑊)
32	31, 21	lindsind2 21858	. . . . . . . . . . . 12 ⊢ (((𝑊 ∈ LMod ∧ (Scalar‘𝑊) ∈ NzRing) ∧ 𝐹 ∈ (LIndS‘𝑊) ∧ 𝑥 ∈ 𝐹) → ¬ 𝑥 ∈ ((LSpan‘𝑊)‘(𝐹 ∖ {𝑥})))
33	20, 28, 29, 30, 32	syl211anc 1394	. . . . . . . . . . 11 ⊢ (((𝑊 ∈ LVec ∧ 𝐹 ∈ (LIndS‘𝑊)) ∧ (𝑥 ∈ 𝐹 ∧ 𝑘 ∈ ((Base‘(Scalar‘𝑊)) ∖ {(0_g‘(Scalar‘𝑊))}))) → ¬ 𝑥 ∈ ((LSpan‘𝑊)‘(𝐹 ∖ {𝑥})))
34	33	3adantl3 1181	. . . . . . . . . 10 ⊢ (((𝑊 ∈ LVec ∧ 𝐹 ∈ (LIndS‘𝑊) ∧ 𝑋 ∈ ((Base‘𝑊) ∖ ((LSpan‘𝑊)‘𝐹))) ∧ (𝑥 ∈ 𝐹 ∧ 𝑘 ∈ ((Base‘(Scalar‘𝑊)) ∖ {(0_g‘(Scalar‘𝑊))}))) → ¬ 𝑥 ∈ ((LSpan‘𝑊)‘(𝐹 ∖ {𝑥})))
35	34	adantr 484	. . . . . . . . 9 ⊢ ((((𝑊 ∈ LVec ∧ 𝐹 ∈ (LIndS‘𝑊) ∧ 𝑋 ∈ ((Base‘𝑊) ∖ ((LSpan‘𝑊)‘𝐹))) ∧ (𝑥 ∈ 𝐹 ∧ 𝑘 ∈ ((Base‘(Scalar‘𝑊)) ∖ {(0_g‘(Scalar‘𝑊))}))) ∧ 𝑥 ∈ ((LSpan‘𝑊)‘((𝐹 ∖ {𝑥}) ∪ {𝑋}))) → ¬ 𝑥 ∈ ((LSpan‘𝑊)‘(𝐹 ∖ {𝑥})))
36	18, 35	eldifd 3913	. . . . . . . 8 ⊢ ((((𝑊 ∈ LVec ∧ 𝐹 ∈ (LIndS‘𝑊) ∧ 𝑋 ∈ ((Base‘𝑊) ∖ ((LSpan‘𝑊)‘𝐹))) ∧ (𝑥 ∈ 𝐹 ∧ 𝑘 ∈ ((Base‘(Scalar‘𝑊)) ∖ {(0_g‘(Scalar‘𝑊))}))) ∧ 𝑥 ∈ ((LSpan‘𝑊)‘((𝐹 ∖ {𝑥}) ∪ {𝑋}))) → 𝑥 ∈ (((LSpan‘𝑊)‘((𝐹 ∖ {𝑥}) ∪ {𝑋})) ∖ ((LSpan‘𝑊)‘(𝐹 ∖ {𝑥}))))
37		eqid 2761	. . . . . . . . 9 ⊢ (LSubSp‘𝑊) = (LSubSp‘𝑊)
38	1, 37, 31	lspsolv 21200	. . . . . . . 8 ⊢ ((𝑊 ∈ LVec ∧ ((𝐹 ∖ {𝑥}) ⊆ (Base‘𝑊) ∧ 𝑋 ∈ (Base‘𝑊) ∧ 𝑥 ∈ (((LSpan‘𝑊)‘((𝐹 ∖ {𝑥}) ∪ {𝑋})) ∖ ((LSpan‘𝑊)‘(𝐹 ∖ {𝑥}))))) → 𝑋 ∈ ((LSpan‘𝑊)‘((𝐹 ∖ {𝑥}) ∪ {𝑥})))
39	12, 15, 17, 36, 38	syl13anc 1390	. . . . . . 7 ⊢ ((((𝑊 ∈ LVec ∧ 𝐹 ∈ (LIndS‘𝑊) ∧ 𝑋 ∈ ((Base‘𝑊) ∖ ((LSpan‘𝑊)‘𝐹))) ∧ (𝑥 ∈ 𝐹 ∧ 𝑘 ∈ ((Base‘(Scalar‘𝑊)) ∖ {(0_g‘(Scalar‘𝑊))}))) ∧ 𝑥 ∈ ((LSpan‘𝑊)‘((𝐹 ∖ {𝑥}) ∪ {𝑋}))) → 𝑋 ∈ ((LSpan‘𝑊)‘((𝐹 ∖ {𝑥}) ∪ {𝑥})))
40	39	ex 416	. . . . . 6 ⊢ (((𝑊 ∈ LVec ∧ 𝐹 ∈ (LIndS‘𝑊) ∧ 𝑋 ∈ ((Base‘𝑊) ∖ ((LSpan‘𝑊)‘𝐹))) ∧ (𝑥 ∈ 𝐹 ∧ 𝑘 ∈ ((Base‘(Scalar‘𝑊)) ∖ {(0_g‘(Scalar‘𝑊))}))) → (𝑥 ∈ ((LSpan‘𝑊)‘((𝐹 ∖ {𝑥}) ∪ {𝑋})) → 𝑋 ∈ ((LSpan‘𝑊)‘((𝐹 ∖ {𝑥}) ∪ {𝑥}))))
41		eldif 3912	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑋 ∈ ((Base‘𝑊) ∖ ((LSpan‘𝑊)‘𝐹)) ↔ (𝑋 ∈ (Base‘𝑊) ∧ ¬ 𝑋 ∈ ((LSpan‘𝑊)‘𝐹)))
42		snssi 4741	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝑋 ∈ 𝐹 → {𝑋} ⊆ 𝐹)
43	1, 31	lspss 21038	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((𝑊 ∈ LMod ∧ 𝐹 ⊆ (Base‘𝑊) ∧ {𝑋} ⊆ 𝐹) → ((LSpan‘𝑊)‘{𝑋}) ⊆ ((LSpan‘𝑊)‘𝐹))
44	19, 2, 42, 43	syl3an 1172	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝑊 ∈ LVec ∧ 𝐹 ∈ (LIndS‘𝑊) ∧ 𝑋 ∈ 𝐹) → ((LSpan‘𝑊)‘{𝑋}) ⊆ ((LSpan‘𝑊)‘𝐹))
45	44	ad4ant124 1186	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((((𝑊 ∈ LVec ∧ 𝐹 ∈ (LIndS‘𝑊)) ∧ 𝑋 ∈ (Base‘𝑊)) ∧ 𝑋 ∈ 𝐹) → ((LSpan‘𝑊)‘{𝑋}) ⊆ ((LSpan‘𝑊)‘𝐹))
46	1, 31	lspsnid 21047	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((𝑊 ∈ LMod ∧ 𝑋 ∈ (Base‘𝑊)) → 𝑋 ∈ ((LSpan‘𝑊)‘{𝑋}))
47	19, 46	sylan 589	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝑊 ∈ LVec ∧ 𝑋 ∈ (Base‘𝑊)) → 𝑋 ∈ ((LSpan‘𝑊)‘{𝑋}))
48	47	ad4ant13 761	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((((𝑊 ∈ LVec ∧ 𝐹 ∈ (LIndS‘𝑊)) ∧ 𝑋 ∈ (Base‘𝑊)) ∧ 𝑋 ∈ 𝐹) → 𝑋 ∈ ((LSpan‘𝑊)‘{𝑋}))
49	45, 48	sseldd 3935	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((((𝑊 ∈ LVec ∧ 𝐹 ∈ (LIndS‘𝑊)) ∧ 𝑋 ∈ (Base‘𝑊)) ∧ 𝑋 ∈ 𝐹) → 𝑋 ∈ ((LSpan‘𝑊)‘𝐹))
50	49	ex 416	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝑊 ∈ LVec ∧ 𝐹 ∈ (LIndS‘𝑊)) ∧ 𝑋 ∈ (Base‘𝑊)) → (𝑋 ∈ 𝐹 → 𝑋 ∈ ((LSpan‘𝑊)‘𝐹)))
51	50	con3d 152	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝑊 ∈ LVec ∧ 𝐹 ∈ (LIndS‘𝑊)) ∧ 𝑋 ∈ (Base‘𝑊)) → (¬ 𝑋 ∈ ((LSpan‘𝑊)‘𝐹) → ¬ 𝑋 ∈ 𝐹))
52	51	expimpd 457	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑊 ∈ LVec ∧ 𝐹 ∈ (LIndS‘𝑊)) → ((𝑋 ∈ (Base‘𝑊) ∧ ¬ 𝑋 ∈ ((LSpan‘𝑊)‘𝐹)) → ¬ 𝑋 ∈ 𝐹))
53	52	3impia 1129	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑊 ∈ LVec ∧ 𝐹 ∈ (LIndS‘𝑊) ∧ (𝑋 ∈ (Base‘𝑊) ∧ ¬ 𝑋 ∈ ((LSpan‘𝑊)‘𝐹))) → ¬ 𝑋 ∈ 𝐹)
54	41, 53	syl3an3b 1423	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑊 ∈ LVec ∧ 𝐹 ∈ (LIndS‘𝑊) ∧ 𝑋 ∈ ((Base‘𝑊) ∖ ((LSpan‘𝑊)‘𝐹))) → ¬ 𝑋 ∈ 𝐹)
55		eleq1 2849	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑋 = 𝑥 → (𝑋 ∈ 𝐹 ↔ 𝑥 ∈ 𝐹))
56	55	notbid 320	. . . . . . . . . . . . . . . . 17 ⊢ (𝑋 = 𝑥 → (¬ 𝑋 ∈ 𝐹 ↔ ¬ 𝑥 ∈ 𝐹))
57	54, 56	syl5ibcom 247	. . . . . . . . . . . . . . . 16 ⊢ ((𝑊 ∈ LVec ∧ 𝐹 ∈ (LIndS‘𝑊) ∧ 𝑋 ∈ ((Base‘𝑊) ∖ ((LSpan‘𝑊)‘𝐹))) → (𝑋 = 𝑥 → ¬ 𝑥 ∈ 𝐹))
58	57	necon2ad 2971	. . . . . . . . . . . . . . 15 ⊢ ((𝑊 ∈ LVec ∧ 𝐹 ∈ (LIndS‘𝑊) ∧ 𝑋 ∈ ((Base‘𝑊) ∖ ((LSpan‘𝑊)‘𝐹))) → (𝑥 ∈ 𝐹 → 𝑋 ≠ 𝑥))
59	58	imp 410	. . . . . . . . . . . . . 14 ⊢ (((𝑊 ∈ LVec ∧ 𝐹 ∈ (LIndS‘𝑊) ∧ 𝑋 ∈ ((Base‘𝑊) ∖ ((LSpan‘𝑊)‘𝐹))) ∧ 𝑥 ∈ 𝐹) → 𝑋 ≠ 𝑥)
60		disjsn2 4668	. . . . . . . . . . . . . 14 ⊢ (𝑋 ≠ 𝑥 → ({𝑋} ∩ {𝑥}) = ∅)
61	59, 60	syl 17	. . . . . . . . . . . . 13 ⊢ (((𝑊 ∈ LVec ∧ 𝐹 ∈ (LIndS‘𝑊) ∧ 𝑋 ∈ ((Base‘𝑊) ∖ ((LSpan‘𝑊)‘𝐹))) ∧ 𝑥 ∈ 𝐹) → ({𝑋} ∩ {𝑥}) = ∅)
62		disj3 4405	. . . . . . . . . . . . 13 ⊢ (({𝑋} ∩ {𝑥}) = ∅ ↔ {𝑋} = ({𝑋} ∖ {𝑥}))
63	61, 62	sylib 220	. . . . . . . . . . . 12 ⊢ (((𝑊 ∈ LVec ∧ 𝐹 ∈ (LIndS‘𝑊) ∧ 𝑋 ∈ ((Base‘𝑊) ∖ ((LSpan‘𝑊)‘𝐹))) ∧ 𝑥 ∈ 𝐹) → {𝑋} = ({𝑋} ∖ {𝑥}))
64	63	uneq2d 4119	. . . . . . . . . . 11 ⊢ (((𝑊 ∈ LVec ∧ 𝐹 ∈ (LIndS‘𝑊) ∧ 𝑋 ∈ ((Base‘𝑊) ∖ ((LSpan‘𝑊)‘𝐹))) ∧ 𝑥 ∈ 𝐹) → ((𝐹 ∖ {𝑥}) ∪ {𝑋}) = ((𝐹 ∖ {𝑥}) ∪ ({𝑋} ∖ {𝑥})))
65		difundir 4241	. . . . . . . . . . 11 ⊢ ((𝐹 ∪ {𝑋}) ∖ {𝑥}) = ((𝐹 ∖ {𝑥}) ∪ ({𝑋} ∖ {𝑥}))
66	64, 65	eqtr4di 2814	. . . . . . . . . 10 ⊢ (((𝑊 ∈ LVec ∧ 𝐹 ∈ (LIndS‘𝑊) ∧ 𝑋 ∈ ((Base‘𝑊) ∖ ((LSpan‘𝑊)‘𝐹))) ∧ 𝑥 ∈ 𝐹) → ((𝐹 ∖ {𝑥}) ∪ {𝑋}) = ((𝐹 ∪ {𝑋}) ∖ {𝑥}))
67	66	fveq2d 6865	. . . . . . . . 9 ⊢ (((𝑊 ∈ LVec ∧ 𝐹 ∈ (LIndS‘𝑊) ∧ 𝑋 ∈ ((Base‘𝑊) ∖ ((LSpan‘𝑊)‘𝐹))) ∧ 𝑥 ∈ 𝐹) → ((LSpan‘𝑊)‘((𝐹 ∖ {𝑥}) ∪ {𝑋})) = ((LSpan‘𝑊)‘((𝐹 ∪ {𝑋}) ∖ {𝑥})))
68	67	eleq2d 2847	. . . . . . . 8 ⊢ (((𝑊 ∈ LVec ∧ 𝐹 ∈ (LIndS‘𝑊) ∧ 𝑋 ∈ ((Base‘𝑊) ∖ ((LSpan‘𝑊)‘𝐹))) ∧ 𝑥 ∈ 𝐹) → (𝑥 ∈ ((LSpan‘𝑊)‘((𝐹 ∖ {𝑥}) ∪ {𝑋})) ↔ 𝑥 ∈ ((LSpan‘𝑊)‘((𝐹 ∪ {𝑋}) ∖ {𝑥}))))
69	68	adantrr 727	. . . . . . 7 ⊢ (((𝑊 ∈ LVec ∧ 𝐹 ∈ (LIndS‘𝑊) ∧ 𝑋 ∈ ((Base‘𝑊) ∖ ((LSpan‘𝑊)‘𝐹))) ∧ (𝑥 ∈ 𝐹 ∧ 𝑘 ∈ ((Base‘(Scalar‘𝑊)) ∖ {(0_g‘(Scalar‘𝑊))}))) → (𝑥 ∈ ((LSpan‘𝑊)‘((𝐹 ∖ {𝑥}) ∪ {𝑋})) ↔ 𝑥 ∈ ((LSpan‘𝑊)‘((𝐹 ∪ {𝑋}) ∖ {𝑥}))))
70		simpl 486	. . . . . . . . . . . . 13 ⊢ ((𝑊 ∈ LVec ∧ 𝑘 ∈ ((Base‘(Scalar‘𝑊)) ∖ {(0_g‘(Scalar‘𝑊))})) → 𝑊 ∈ LVec)
71		eldifsn 4743	. . . . . . . . . . . . . 14 ⊢ (𝑘 ∈ ((Base‘(Scalar‘𝑊)) ∖ {(0_g‘(Scalar‘𝑊))}) ↔ (𝑘 ∈ (Base‘(Scalar‘𝑊)) ∧ 𝑘 ≠ (0_g‘(Scalar‘𝑊))))
72	71	bilani 508	. . . . . . . . . . . . 13 ⊢ ((𝑊 ∈ LVec ∧ 𝑘 ∈ ((Base‘(Scalar‘𝑊)) ∖ {(0_g‘(Scalar‘𝑊))})) → (𝑘 ∈ (Base‘(Scalar‘𝑊)) ∧ 𝑘 ≠ (0_g‘(Scalar‘𝑊))))
73	2	sselda 3934	. . . . . . . . . . . . 13 ⊢ ((𝐹 ∈ (LIndS‘𝑊) ∧ 𝑥 ∈ 𝐹) → 𝑥 ∈ (Base‘𝑊))
74		eqid 2761	. . . . . . . . . . . . . 14 ⊢ ( ·_𝑠 ‘𝑊) = ( ·_𝑠 ‘𝑊)
75	1, 21, 74, 25, 24, 31	lspsnvs 21171	. . . . . . . . . . . . 13 ⊢ ((𝑊 ∈ LVec ∧ (𝑘 ∈ (Base‘(Scalar‘𝑊)) ∧ 𝑘 ≠ (0_g‘(Scalar‘𝑊))) ∧ 𝑥 ∈ (Base‘𝑊)) → ((LSpan‘𝑊)‘{(𝑘( ·_𝑠 ‘𝑊)𝑥)}) = ((LSpan‘𝑊)‘{𝑥}))
76	70, 72, 73, 75	syl2an3an 1440	. . . . . . . . . . . 12 ⊢ (((𝑊 ∈ LVec ∧ 𝑘 ∈ ((Base‘(Scalar‘𝑊)) ∖ {(0_g‘(Scalar‘𝑊))})) ∧ (𝐹 ∈ (LIndS‘𝑊) ∧ 𝑥 ∈ 𝐹)) → ((LSpan‘𝑊)‘{(𝑘( ·_𝑠 ‘𝑊)𝑥)}) = ((LSpan‘𝑊)‘{𝑥}))
77	76	an42s 671	. . . . . . . . . . 11 ⊢ (((𝑊 ∈ LVec ∧ 𝐹 ∈ (LIndS‘𝑊)) ∧ (𝑥 ∈ 𝐹 ∧ 𝑘 ∈ ((Base‘(Scalar‘𝑊)) ∖ {(0_g‘(Scalar‘𝑊))}))) → ((LSpan‘𝑊)‘{(𝑘( ·_𝑠 ‘𝑊)𝑥)}) = ((LSpan‘𝑊)‘{𝑥}))
78	77	sseq1d 3965	. . . . . . . . . 10 ⊢ (((𝑊 ∈ LVec ∧ 𝐹 ∈ (LIndS‘𝑊)) ∧ (𝑥 ∈ 𝐹 ∧ 𝑘 ∈ ((Base‘(Scalar‘𝑊)) ∖ {(0_g‘(Scalar‘𝑊))}))) → (((LSpan‘𝑊)‘{(𝑘( ·_𝑠 ‘𝑊)𝑥)}) ⊆ ((LSpan‘𝑊)‘((𝐹 ∪ {𝑋}) ∖ {𝑥})) ↔ ((LSpan‘𝑊)‘{𝑥}) ⊆ ((LSpan‘𝑊)‘((𝐹 ∪ {𝑋}) ∖ {𝑥}))))
79	78	3adantl3 1181	. . . . . . . . 9 ⊢ (((𝑊 ∈ LVec ∧ 𝐹 ∈ (LIndS‘𝑊) ∧ 𝑋 ∈ (Base‘𝑊)) ∧ (𝑥 ∈ 𝐹 ∧ 𝑘 ∈ ((Base‘(Scalar‘𝑊)) ∖ {(0_g‘(Scalar‘𝑊))}))) → (((LSpan‘𝑊)‘{(𝑘( ·_𝑠 ‘𝑊)𝑥)}) ⊆ ((LSpan‘𝑊)‘((𝐹 ∪ {𝑋}) ∖ {𝑥})) ↔ ((LSpan‘𝑊)‘{𝑥}) ⊆ ((LSpan‘𝑊)‘((𝐹 ∪ {𝑋}) ∖ {𝑥}))))
80		eldifi 4082	. . . . . . . . . 10 ⊢ (𝑘 ∈ ((Base‘(Scalar‘𝑊)) ∖ {(0_g‘(Scalar‘𝑊))}) → 𝑘 ∈ (Base‘(Scalar‘𝑊)))
81	19	3ad2ant1 1145	. . . . . . . . . . . 12 ⊢ ((𝑊 ∈ LVec ∧ 𝐹 ∈ (LIndS‘𝑊) ∧ 𝑋 ∈ (Base‘𝑊)) → 𝑊 ∈ LMod)
82	81	adantr 484	. . . . . . . . . . 11 ⊢ (((𝑊 ∈ LVec ∧ 𝐹 ∈ (LIndS‘𝑊) ∧ 𝑋 ∈ (Base‘𝑊)) ∧ (𝑥 ∈ 𝐹 ∧ 𝑘 ∈ (Base‘(Scalar‘𝑊)))) → 𝑊 ∈ LMod)
83		snssi 4741	. . . . . . . . . . . . . . . 16 ⊢ (𝑋 ∈ (Base‘𝑊) → {𝑋} ⊆ (Base‘𝑊))
84	2, 83, 6	syl2an 605	. . . . . . . . . . . . . . 15 ⊢ ((𝐹 ∈ (LIndS‘𝑊) ∧ 𝑋 ∈ (Base‘𝑊)) → (𝐹 ∪ {𝑋}) ⊆ (Base‘𝑊))
85	84	ssdifssd 4098	. . . . . . . . . . . . . 14 ⊢ ((𝐹 ∈ (LIndS‘𝑊) ∧ 𝑋 ∈ (Base‘𝑊)) → ((𝐹 ∪ {𝑋}) ∖ {𝑥}) ⊆ (Base‘𝑊))
86	1, 37, 31	lspcl 21030	. . . . . . . . . . . . . 14 ⊢ ((𝑊 ∈ LMod ∧ ((𝐹 ∪ {𝑋}) ∖ {𝑥}) ⊆ (Base‘𝑊)) → ((LSpan‘𝑊)‘((𝐹 ∪ {𝑋}) ∖ {𝑥})) ∈ (LSubSp‘𝑊))
87	19, 85, 86	syl2an 605	. . . . . . . . . . . . 13 ⊢ ((𝑊 ∈ LVec ∧ (𝐹 ∈ (LIndS‘𝑊) ∧ 𝑋 ∈ (Base‘𝑊))) → ((LSpan‘𝑊)‘((𝐹 ∪ {𝑋}) ∖ {𝑥})) ∈ (LSubSp‘𝑊))
88	87	3impb 1126	. . . . . . . . . . . 12 ⊢ ((𝑊 ∈ LVec ∧ 𝐹 ∈ (LIndS‘𝑊) ∧ 𝑋 ∈ (Base‘𝑊)) → ((LSpan‘𝑊)‘((𝐹 ∪ {𝑋}) ∖ {𝑥})) ∈ (LSubSp‘𝑊))
89	88	adantr 484	. . . . . . . . . . 11 ⊢ (((𝑊 ∈ LVec ∧ 𝐹 ∈ (LIndS‘𝑊) ∧ 𝑋 ∈ (Base‘𝑊)) ∧ (𝑥 ∈ 𝐹 ∧ 𝑘 ∈ (Base‘(Scalar‘𝑊)))) → ((LSpan‘𝑊)‘((𝐹 ∪ {𝑋}) ∖ {𝑥})) ∈ (LSubSp‘𝑊))
90	19	anim1i 624	. . . . . . . . . . . . . 14 ⊢ ((𝑊 ∈ LVec ∧ 𝑘 ∈ (Base‘(Scalar‘𝑊))) → (𝑊 ∈ LMod ∧ 𝑘 ∈ (Base‘(Scalar‘𝑊))))
91	1, 21, 74, 25	lmodvscl 20932	. . . . . . . . . . . . . . 15 ⊢ ((𝑊 ∈ LMod ∧ 𝑘 ∈ (Base‘(Scalar‘𝑊)) ∧ 𝑥 ∈ (Base‘𝑊)) → (𝑘( ·_𝑠 ‘𝑊)𝑥) ∈ (Base‘𝑊))
92	91	3expa 1130	. . . . . . . . . . . . . 14 ⊢ (((𝑊 ∈ LMod ∧ 𝑘 ∈ (Base‘(Scalar‘𝑊))) ∧ 𝑥 ∈ (Base‘𝑊)) → (𝑘( ·_𝑠 ‘𝑊)𝑥) ∈ (Base‘𝑊))
93	90, 73, 92	syl2an 605	. . . . . . . . . . . . 13 ⊢ (((𝑊 ∈ LVec ∧ 𝑘 ∈ (Base‘(Scalar‘𝑊))) ∧ (𝐹 ∈ (LIndS‘𝑊) ∧ 𝑥 ∈ 𝐹)) → (𝑘( ·_𝑠 ‘𝑊)𝑥) ∈ (Base‘𝑊))
94	93	an42s 671	. . . . . . . . . . . 12 ⊢ (((𝑊 ∈ LVec ∧ 𝐹 ∈ (LIndS‘𝑊)) ∧ (𝑥 ∈ 𝐹 ∧ 𝑘 ∈ (Base‘(Scalar‘𝑊)))) → (𝑘( ·_𝑠 ‘𝑊)𝑥) ∈ (Base‘𝑊))
95	94	3adantl3 1181	. . . . . . . . . . 11 ⊢ (((𝑊 ∈ LVec ∧ 𝐹 ∈ (LIndS‘𝑊) ∧ 𝑋 ∈ (Base‘𝑊)) ∧ (𝑥 ∈ 𝐹 ∧ 𝑘 ∈ (Base‘(Scalar‘𝑊)))) → (𝑘( ·_𝑠 ‘𝑊)𝑥) ∈ (Base‘𝑊))
96	1, 37, 31, 82, 89, 95	ellspsn5b 21049	. . . . . . . . . 10 ⊢ (((𝑊 ∈ LVec ∧ 𝐹 ∈ (LIndS‘𝑊) ∧ 𝑋 ∈ (Base‘𝑊)) ∧ (𝑥 ∈ 𝐹 ∧ 𝑘 ∈ (Base‘(Scalar‘𝑊)))) → ((𝑘( ·_𝑠 ‘𝑊)𝑥) ∈ ((LSpan‘𝑊)‘((𝐹 ∪ {𝑋}) ∖ {𝑥})) ↔ ((LSpan‘𝑊)‘{(𝑘( ·_𝑠 ‘𝑊)𝑥)}) ⊆ ((LSpan‘𝑊)‘((𝐹 ∪ {𝑋}) ∖ {𝑥}))))
97	80, 96	sylanr2 693	. . . . . . . . 9 ⊢ (((𝑊 ∈ LVec ∧ 𝐹 ∈ (LIndS‘𝑊) ∧ 𝑋 ∈ (Base‘𝑊)) ∧ (𝑥 ∈ 𝐹 ∧ 𝑘 ∈ ((Base‘(Scalar‘𝑊)) ∖ {(0_g‘(Scalar‘𝑊))}))) → ((𝑘( ·_𝑠 ‘𝑊)𝑥) ∈ ((LSpan‘𝑊)‘((𝐹 ∪ {𝑋}) ∖ {𝑥})) ↔ ((LSpan‘𝑊)‘{(𝑘( ·_𝑠 ‘𝑊)𝑥)}) ⊆ ((LSpan‘𝑊)‘((𝐹 ∪ {𝑋}) ∖ {𝑥}))))
98	81	adantr 484	. . . . . . . . . . 11 ⊢ (((𝑊 ∈ LVec ∧ 𝐹 ∈ (LIndS‘𝑊) ∧ 𝑋 ∈ (Base‘𝑊)) ∧ 𝑥 ∈ 𝐹) → 𝑊 ∈ LMod)
99	88	adantr 484	. . . . . . . . . . 11 ⊢ (((𝑊 ∈ LVec ∧ 𝐹 ∈ (LIndS‘𝑊) ∧ 𝑋 ∈ (Base‘𝑊)) ∧ 𝑥 ∈ 𝐹) → ((LSpan‘𝑊)‘((𝐹 ∪ {𝑋}) ∖ {𝑥})) ∈ (LSubSp‘𝑊))
100	73	3ad2antl2 1199	. . . . . . . . . . 11 ⊢ (((𝑊 ∈ LVec ∧ 𝐹 ∈ (LIndS‘𝑊) ∧ 𝑋 ∈ (Base‘𝑊)) ∧ 𝑥 ∈ 𝐹) → 𝑥 ∈ (Base‘𝑊))
101	1, 37, 31, 98, 99, 100	ellspsn5b 21049	. . . . . . . . . 10 ⊢ (((𝑊 ∈ LVec ∧ 𝐹 ∈ (LIndS‘𝑊) ∧ 𝑋 ∈ (Base‘𝑊)) ∧ 𝑥 ∈ 𝐹) → (𝑥 ∈ ((LSpan‘𝑊)‘((𝐹 ∪ {𝑋}) ∖ {𝑥})) ↔ ((LSpan‘𝑊)‘{𝑥}) ⊆ ((LSpan‘𝑊)‘((𝐹 ∪ {𝑋}) ∖ {𝑥}))))
102	101	adantrr 727	. . . . . . . . 9 ⊢ (((𝑊 ∈ LVec ∧ 𝐹 ∈ (LIndS‘𝑊) ∧ 𝑋 ∈ (Base‘𝑊)) ∧ (𝑥 ∈ 𝐹 ∧ 𝑘 ∈ ((Base‘(Scalar‘𝑊)) ∖ {(0_g‘(Scalar‘𝑊))}))) → (𝑥 ∈ ((LSpan‘𝑊)‘((𝐹 ∪ {𝑋}) ∖ {𝑥})) ↔ ((LSpan‘𝑊)‘{𝑥}) ⊆ ((LSpan‘𝑊)‘((𝐹 ∪ {𝑋}) ∖ {𝑥}))))
103	79, 97, 102	3bitr4rd 314	. . . . . . . 8 ⊢ (((𝑊 ∈ LVec ∧ 𝐹 ∈ (LIndS‘𝑊) ∧ 𝑋 ∈ (Base‘𝑊)) ∧ (𝑥 ∈ 𝐹 ∧ 𝑘 ∈ ((Base‘(Scalar‘𝑊)) ∖ {(0_g‘(Scalar‘𝑊))}))) → (𝑥 ∈ ((LSpan‘𝑊)‘((𝐹 ∪ {𝑋}) ∖ {𝑥})) ↔ (𝑘( ·_𝑠 ‘𝑊)𝑥) ∈ ((LSpan‘𝑊)‘((𝐹 ∪ {𝑋}) ∖ {𝑥}))))
104	3, 103	syl3anl3 1432	. . . . . . 7 ⊢ (((𝑊 ∈ LVec ∧ 𝐹 ∈ (LIndS‘𝑊) ∧ 𝑋 ∈ ((Base‘𝑊) ∖ ((LSpan‘𝑊)‘𝐹))) ∧ (𝑥 ∈ 𝐹 ∧ 𝑘 ∈ ((Base‘(Scalar‘𝑊)) ∖ {(0_g‘(Scalar‘𝑊))}))) → (𝑥 ∈ ((LSpan‘𝑊)‘((𝐹 ∪ {𝑋}) ∖ {𝑥})) ↔ (𝑘( ·_𝑠 ‘𝑊)𝑥) ∈ ((LSpan‘𝑊)‘((𝐹 ∪ {𝑋}) ∖ {𝑥}))))
105	69, 104	bitrd 281	. . . . . 6 ⊢ (((𝑊 ∈ LVec ∧ 𝐹 ∈ (LIndS‘𝑊) ∧ 𝑋 ∈ ((Base‘𝑊) ∖ ((LSpan‘𝑊)‘𝐹))) ∧ (𝑥 ∈ 𝐹 ∧ 𝑘 ∈ ((Base‘(Scalar‘𝑊)) ∖ {(0_g‘(Scalar‘𝑊))}))) → (𝑥 ∈ ((LSpan‘𝑊)‘((𝐹 ∖ {𝑥}) ∪ {𝑋})) ↔ (𝑘( ·_𝑠 ‘𝑊)𝑥) ∈ ((LSpan‘𝑊)‘((𝐹 ∪ {𝑋}) ∖ {𝑥}))))
106		difsnid 4765	. . . . . . . . 9 ⊢ (𝑥 ∈ 𝐹 → ((𝐹 ∖ {𝑥}) ∪ {𝑥}) = 𝐹)
107	106	fveq2d 6865	. . . . . . . 8 ⊢ (𝑥 ∈ 𝐹 → ((LSpan‘𝑊)‘((𝐹 ∖ {𝑥}) ∪ {𝑥})) = ((LSpan‘𝑊)‘𝐹))
108	107	eleq2d 2847	. . . . . . 7 ⊢ (𝑥 ∈ 𝐹 → (𝑋 ∈ ((LSpan‘𝑊)‘((𝐹 ∖ {𝑥}) ∪ {𝑥})) ↔ 𝑋 ∈ ((LSpan‘𝑊)‘𝐹)))
109	108	ad2antrl 738	. . . . . 6 ⊢ (((𝑊 ∈ LVec ∧ 𝐹 ∈ (LIndS‘𝑊) ∧ 𝑋 ∈ ((Base‘𝑊) ∖ ((LSpan‘𝑊)‘𝐹))) ∧ (𝑥 ∈ 𝐹 ∧ 𝑘 ∈ ((Base‘(Scalar‘𝑊)) ∖ {(0_g‘(Scalar‘𝑊))}))) → (𝑋 ∈ ((LSpan‘𝑊)‘((𝐹 ∖ {𝑥}) ∪ {𝑥})) ↔ 𝑋 ∈ ((LSpan‘𝑊)‘𝐹)))
110	40, 105, 109	3imtr3d 295	. . . . 5 ⊢ (((𝑊 ∈ LVec ∧ 𝐹 ∈ (LIndS‘𝑊) ∧ 𝑋 ∈ ((Base‘𝑊) ∖ ((LSpan‘𝑊)‘𝐹))) ∧ (𝑥 ∈ 𝐹 ∧ 𝑘 ∈ ((Base‘(Scalar‘𝑊)) ∖ {(0_g‘(Scalar‘𝑊))}))) → ((𝑘( ·_𝑠 ‘𝑊)𝑥) ∈ ((LSpan‘𝑊)‘((𝐹 ∪ {𝑋}) ∖ {𝑥})) → 𝑋 ∈ ((LSpan‘𝑊)‘𝐹)))
111	11, 110	mtod 200	. . . 4 ⊢ (((𝑊 ∈ LVec ∧ 𝐹 ∈ (LIndS‘𝑊) ∧ 𝑋 ∈ ((Base‘𝑊) ∖ ((LSpan‘𝑊)‘𝐹))) ∧ (𝑥 ∈ 𝐹 ∧ 𝑘 ∈ ((Base‘(Scalar‘𝑊)) ∖ {(0_g‘(Scalar‘𝑊))}))) → ¬ (𝑘( ·_𝑠 ‘𝑊)𝑥) ∈ ((LSpan‘𝑊)‘((𝐹 ∪ {𝑋}) ∖ {𝑥})))
112	111	ralrimivva 3204	. . 3 ⊢ ((𝑊 ∈ LVec ∧ 𝐹 ∈ (LIndS‘𝑊) ∧ 𝑋 ∈ ((Base‘𝑊) ∖ ((LSpan‘𝑊)‘𝐹))) → ∀𝑥 ∈ 𝐹 ∀𝑘 ∈ ((Base‘(Scalar‘𝑊)) ∖ {(0_g‘(Scalar‘𝑊))}) ¬ (𝑘( ·_𝑠 ‘𝑊)𝑥) ∈ ((LSpan‘𝑊)‘((𝐹 ∪ {𝑋}) ∖ {𝑥})))
113	10	adantr 484	. . . . . 6 ⊢ (((𝑊 ∈ LVec ∧ 𝐹 ∈ (LIndS‘𝑊) ∧ 𝑋 ∈ ((Base‘𝑊) ∖ ((LSpan‘𝑊)‘𝐹))) ∧ 𝑘 ∈ ((Base‘(Scalar‘𝑊)) ∖ {(0_g‘(Scalar‘𝑊))})) → ¬ 𝑋 ∈ ((LSpan‘𝑊)‘𝐹))
114		difsn 4755	. . . . . . . . . . 11 ⊢ (¬ 𝑋 ∈ 𝐹 → (𝐹 ∖ {𝑋}) = 𝐹)
115	54, 114	syl 17	. . . . . . . . . 10 ⊢ ((𝑊 ∈ LVec ∧ 𝐹 ∈ (LIndS‘𝑊) ∧ 𝑋 ∈ ((Base‘𝑊) ∖ ((LSpan‘𝑊)‘𝐹))) → (𝐹 ∖ {𝑋}) = 𝐹)
116	115	fveq2d 6865	. . . . . . . . 9 ⊢ ((𝑊 ∈ LVec ∧ 𝐹 ∈ (LIndS‘𝑊) ∧ 𝑋 ∈ ((Base‘𝑊) ∖ ((LSpan‘𝑊)‘𝐹))) → ((LSpan‘𝑊)‘(𝐹 ∖ {𝑋})) = ((LSpan‘𝑊)‘𝐹))
117	116	eleq2d 2847	. . . . . . . 8 ⊢ ((𝑊 ∈ LVec ∧ 𝐹 ∈ (LIndS‘𝑊) ∧ 𝑋 ∈ ((Base‘𝑊) ∖ ((LSpan‘𝑊)‘𝐹))) → ((𝑘( ·_𝑠 ‘𝑊)𝑋) ∈ ((LSpan‘𝑊)‘(𝐹 ∖ {𝑋})) ↔ (𝑘( ·_𝑠 ‘𝑊)𝑋) ∈ ((LSpan‘𝑊)‘𝐹)))
118	117	adantr 484	. . . . . . 7 ⊢ (((𝑊 ∈ LVec ∧ 𝐹 ∈ (LIndS‘𝑊) ∧ 𝑋 ∈ ((Base‘𝑊) ∖ ((LSpan‘𝑊)‘𝐹))) ∧ 𝑘 ∈ ((Base‘(Scalar‘𝑊)) ∖ {(0_g‘(Scalar‘𝑊))})) → ((𝑘( ·_𝑠 ‘𝑊)𝑋) ∈ ((LSpan‘𝑊)‘(𝐹 ∖ {𝑋})) ↔ (𝑘( ·_𝑠 ‘𝑊)𝑋) ∈ ((LSpan‘𝑊)‘𝐹)))
119	1, 21, 74, 25, 24, 31	lspsnvs 21171	. . . . . . . . . . . . . 14 ⊢ ((𝑊 ∈ LVec ∧ (𝑘 ∈ (Base‘(Scalar‘𝑊)) ∧ 𝑘 ≠ (0_g‘(Scalar‘𝑊))) ∧ 𝑋 ∈ (Base‘𝑊)) → ((LSpan‘𝑊)‘{(𝑘( ·_𝑠 ‘𝑊)𝑋)}) = ((LSpan‘𝑊)‘{𝑋}))
120	119	3expa 1130	. . . . . . . . . . . . 13 ⊢ (((𝑊 ∈ LVec ∧ (𝑘 ∈ (Base‘(Scalar‘𝑊)) ∧ 𝑘 ≠ (0_g‘(Scalar‘𝑊)))) ∧ 𝑋 ∈ (Base‘𝑊)) → ((LSpan‘𝑊)‘{(𝑘( ·_𝑠 ‘𝑊)𝑋)}) = ((LSpan‘𝑊)‘{𝑋}))
121	120	an32s 662	. . . . . . . . . . . 12 ⊢ (((𝑊 ∈ LVec ∧ 𝑋 ∈ (Base‘𝑊)) ∧ (𝑘 ∈ (Base‘(Scalar‘𝑊)) ∧ 𝑘 ≠ (0_g‘(Scalar‘𝑊)))) → ((LSpan‘𝑊)‘{(𝑘( ·_𝑠 ‘𝑊)𝑋)}) = ((LSpan‘𝑊)‘{𝑋}))
122	71, 121	sylan2b 603	. . . . . . . . . . 11 ⊢ (((𝑊 ∈ LVec ∧ 𝑋 ∈ (Base‘𝑊)) ∧ 𝑘 ∈ ((Base‘(Scalar‘𝑊)) ∖ {(0_g‘(Scalar‘𝑊))})) → ((LSpan‘𝑊)‘{(𝑘( ·_𝑠 ‘𝑊)𝑋)}) = ((LSpan‘𝑊)‘{𝑋}))
123	122	sseq1d 3965	. . . . . . . . . 10 ⊢ (((𝑊 ∈ LVec ∧ 𝑋 ∈ (Base‘𝑊)) ∧ 𝑘 ∈ ((Base‘(Scalar‘𝑊)) ∖ {(0_g‘(Scalar‘𝑊))})) → (((LSpan‘𝑊)‘{(𝑘( ·_𝑠 ‘𝑊)𝑋)}) ⊆ ((LSpan‘𝑊)‘𝐹) ↔ ((LSpan‘𝑊)‘{𝑋}) ⊆ ((LSpan‘𝑊)‘𝐹)))
124	123	3adantl2 1180	. . . . . . . . 9 ⊢ (((𝑊 ∈ LVec ∧ 𝐹 ∈ (LIndS‘𝑊) ∧ 𝑋 ∈ (Base‘𝑊)) ∧ 𝑘 ∈ ((Base‘(Scalar‘𝑊)) ∖ {(0_g‘(Scalar‘𝑊))})) → (((LSpan‘𝑊)‘{(𝑘( ·_𝑠 ‘𝑊)𝑋)}) ⊆ ((LSpan‘𝑊)‘𝐹) ↔ ((LSpan‘𝑊)‘{𝑋}) ⊆ ((LSpan‘𝑊)‘𝐹)))
125	81	adantr 484	. . . . . . . . . . 11 ⊢ (((𝑊 ∈ LVec ∧ 𝐹 ∈ (LIndS‘𝑊) ∧ 𝑋 ∈ (Base‘𝑊)) ∧ 𝑘 ∈ (Base‘(Scalar‘𝑊))) → 𝑊 ∈ LMod)
126	1, 37, 31	lspcl 21030	. . . . . . . . . . . . . 14 ⊢ ((𝑊 ∈ LMod ∧ 𝐹 ⊆ (Base‘𝑊)) → ((LSpan‘𝑊)‘𝐹) ∈ (LSubSp‘𝑊))
127	19, 2, 126	syl2an 605	. . . . . . . . . . . . 13 ⊢ ((𝑊 ∈ LVec ∧ 𝐹 ∈ (LIndS‘𝑊)) → ((LSpan‘𝑊)‘𝐹) ∈ (LSubSp‘𝑊))
128	127	3adant3 1144	. . . . . . . . . . . 12 ⊢ ((𝑊 ∈ LVec ∧ 𝐹 ∈ (LIndS‘𝑊) ∧ 𝑋 ∈ (Base‘𝑊)) → ((LSpan‘𝑊)‘𝐹) ∈ (LSubSp‘𝑊))
129	128	adantr 484	. . . . . . . . . . 11 ⊢ (((𝑊 ∈ LVec ∧ 𝐹 ∈ (LIndS‘𝑊) ∧ 𝑋 ∈ (Base‘𝑊)) ∧ 𝑘 ∈ (Base‘(Scalar‘𝑊))) → ((LSpan‘𝑊)‘𝐹) ∈ (LSubSp‘𝑊))
130	1, 21, 74, 25	lmodvscl 20932	. . . . . . . . . . . . . . 15 ⊢ ((𝑊 ∈ LMod ∧ 𝑘 ∈ (Base‘(Scalar‘𝑊)) ∧ 𝑋 ∈ (Base‘𝑊)) → (𝑘( ·_𝑠 ‘𝑊)𝑋) ∈ (Base‘𝑊))
131	130	3expa 1130	. . . . . . . . . . . . . 14 ⊢ (((𝑊 ∈ LMod ∧ 𝑘 ∈ (Base‘(Scalar‘𝑊))) ∧ 𝑋 ∈ (Base‘𝑊)) → (𝑘( ·_𝑠 ‘𝑊)𝑋) ∈ (Base‘𝑊))
132	131	an32s 662	. . . . . . . . . . . . 13 ⊢ (((𝑊 ∈ LMod ∧ 𝑋 ∈ (Base‘𝑊)) ∧ 𝑘 ∈ (Base‘(Scalar‘𝑊))) → (𝑘( ·_𝑠 ‘𝑊)𝑋) ∈ (Base‘𝑊))
133	19, 132	sylanl1 690	. . . . . . . . . . . 12 ⊢ (((𝑊 ∈ LVec ∧ 𝑋 ∈ (Base‘𝑊)) ∧ 𝑘 ∈ (Base‘(Scalar‘𝑊))) → (𝑘( ·_𝑠 ‘𝑊)𝑋) ∈ (Base‘𝑊))
134	133	3adantl2 1180	. . . . . . . . . . 11 ⊢ (((𝑊 ∈ LVec ∧ 𝐹 ∈ (LIndS‘𝑊) ∧ 𝑋 ∈ (Base‘𝑊)) ∧ 𝑘 ∈ (Base‘(Scalar‘𝑊))) → (𝑘( ·_𝑠 ‘𝑊)𝑋) ∈ (Base‘𝑊))
135	1, 37, 31, 125, 129, 134	ellspsn5b 21049	. . . . . . . . . 10 ⊢ (((𝑊 ∈ LVec ∧ 𝐹 ∈ (LIndS‘𝑊) ∧ 𝑋 ∈ (Base‘𝑊)) ∧ 𝑘 ∈ (Base‘(Scalar‘𝑊))) → ((𝑘( ·_𝑠 ‘𝑊)𝑋) ∈ ((LSpan‘𝑊)‘𝐹) ↔ ((LSpan‘𝑊)‘{(𝑘( ·_𝑠 ‘𝑊)𝑋)}) ⊆ ((LSpan‘𝑊)‘𝐹)))
136	80, 135	sylan2 602	. . . . . . . . 9 ⊢ (((𝑊 ∈ LVec ∧ 𝐹 ∈ (LIndS‘𝑊) ∧ 𝑋 ∈ (Base‘𝑊)) ∧ 𝑘 ∈ ((Base‘(Scalar‘𝑊)) ∖ {(0_g‘(Scalar‘𝑊))})) → ((𝑘( ·_𝑠 ‘𝑊)𝑋) ∈ ((LSpan‘𝑊)‘𝐹) ↔ ((LSpan‘𝑊)‘{(𝑘( ·_𝑠 ‘𝑊)𝑋)}) ⊆ ((LSpan‘𝑊)‘𝐹)))
137		simp3 1150	. . . . . . . . . . 11 ⊢ ((𝑊 ∈ LVec ∧ 𝐹 ∈ (LIndS‘𝑊) ∧ 𝑋 ∈ (Base‘𝑊)) → 𝑋 ∈ (Base‘𝑊))
138	1, 37, 31, 81, 128, 137	ellspsn5b 21049	. . . . . . . . . 10 ⊢ ((𝑊 ∈ LVec ∧ 𝐹 ∈ (LIndS‘𝑊) ∧ 𝑋 ∈ (Base‘𝑊)) → (𝑋 ∈ ((LSpan‘𝑊)‘𝐹) ↔ ((LSpan‘𝑊)‘{𝑋}) ⊆ ((LSpan‘𝑊)‘𝐹)))
139	138	adantr 484	. . . . . . . . 9 ⊢ (((𝑊 ∈ LVec ∧ 𝐹 ∈ (LIndS‘𝑊) ∧ 𝑋 ∈ (Base‘𝑊)) ∧ 𝑘 ∈ ((Base‘(Scalar‘𝑊)) ∖ {(0_g‘(Scalar‘𝑊))})) → (𝑋 ∈ ((LSpan‘𝑊)‘𝐹) ↔ ((LSpan‘𝑊)‘{𝑋}) ⊆ ((LSpan‘𝑊)‘𝐹)))
140	124, 136, 139	3bitr4d 313	. . . . . . . 8 ⊢ (((𝑊 ∈ LVec ∧ 𝐹 ∈ (LIndS‘𝑊) ∧ 𝑋 ∈ (Base‘𝑊)) ∧ 𝑘 ∈ ((Base‘(Scalar‘𝑊)) ∖ {(0_g‘(Scalar‘𝑊))})) → ((𝑘( ·_𝑠 ‘𝑊)𝑋) ∈ ((LSpan‘𝑊)‘𝐹) ↔ 𝑋 ∈ ((LSpan‘𝑊)‘𝐹)))
141	3, 140	syl3anl3 1432	. . . . . . 7 ⊢ (((𝑊 ∈ LVec ∧ 𝐹 ∈ (LIndS‘𝑊) ∧ 𝑋 ∈ ((Base‘𝑊) ∖ ((LSpan‘𝑊)‘𝐹))) ∧ 𝑘 ∈ ((Base‘(Scalar‘𝑊)) ∖ {(0_g‘(Scalar‘𝑊))})) → ((𝑘( ·_𝑠 ‘𝑊)𝑋) ∈ ((LSpan‘𝑊)‘𝐹) ↔ 𝑋 ∈ ((LSpan‘𝑊)‘𝐹)))
142	118, 141	bitrd 281	. . . . . 6 ⊢ (((𝑊 ∈ LVec ∧ 𝐹 ∈ (LIndS‘𝑊) ∧ 𝑋 ∈ ((Base‘𝑊) ∖ ((LSpan‘𝑊)‘𝐹))) ∧ 𝑘 ∈ ((Base‘(Scalar‘𝑊)) ∖ {(0_g‘(Scalar‘𝑊))})) → ((𝑘( ·_𝑠 ‘𝑊)𝑋) ∈ ((LSpan‘𝑊)‘(𝐹 ∖ {𝑋})) ↔ 𝑋 ∈ ((LSpan‘𝑊)‘𝐹)))
143	113, 142	mtbird 327	. . . . 5 ⊢ (((𝑊 ∈ LVec ∧ 𝐹 ∈ (LIndS‘𝑊) ∧ 𝑋 ∈ ((Base‘𝑊) ∖ ((LSpan‘𝑊)‘𝐹))) ∧ 𝑘 ∈ ((Base‘(Scalar‘𝑊)) ∖ {(0_g‘(Scalar‘𝑊))})) → ¬ (𝑘( ·_𝑠 ‘𝑊)𝑋) ∈ ((LSpan‘𝑊)‘(𝐹 ∖ {𝑋})))
144	143	ralrimiva 3153	. . . 4 ⊢ ((𝑊 ∈ LVec ∧ 𝐹 ∈ (LIndS‘𝑊) ∧ 𝑋 ∈ ((Base‘𝑊) ∖ ((LSpan‘𝑊)‘𝐹))) → ∀𝑘 ∈ ((Base‘(Scalar‘𝑊)) ∖ {(0_g‘(Scalar‘𝑊))}) ¬ (𝑘( ·_𝑠 ‘𝑊)𝑋) ∈ ((LSpan‘𝑊)‘(𝐹 ∖ {𝑋})))
145		oveq2 7398	. . . . . . . . 9 ⊢ (𝑥 = 𝑋 → (𝑘( ·_𝑠 ‘𝑊)𝑥) = (𝑘( ·_𝑠 ‘𝑊)𝑋))
146		sneq 4589	. . . . . . . . . . . 12 ⊢ (𝑥 = 𝑋 → {𝑥} = {𝑋})
147	146	difeq2d 4078	. . . . . . . . . . 11 ⊢ (𝑥 = 𝑋 → ((𝐹 ∪ {𝑋}) ∖ {𝑥}) = ((𝐹 ∪ {𝑋}) ∖ {𝑋}))
148		difun2 4432	. . . . . . . . . . 11 ⊢ ((𝐹 ∪ {𝑋}) ∖ {𝑋}) = (𝐹 ∖ {𝑋})
149	147, 148	eqtrdi 2812	. . . . . . . . . 10 ⊢ (𝑥 = 𝑋 → ((𝐹 ∪ {𝑋}) ∖ {𝑥}) = (𝐹 ∖ {𝑋}))
150	149	fveq2d 6865	. . . . . . . . 9 ⊢ (𝑥 = 𝑋 → ((LSpan‘𝑊)‘((𝐹 ∪ {𝑋}) ∖ {𝑥})) = ((LSpan‘𝑊)‘(𝐹 ∖ {𝑋})))
151	145, 150	eleq12d 2855	. . . . . . . 8 ⊢ (𝑥 = 𝑋 → ((𝑘( ·_𝑠 ‘𝑊)𝑥) ∈ ((LSpan‘𝑊)‘((𝐹 ∪ {𝑋}) ∖ {𝑥})) ↔ (𝑘( ·_𝑠 ‘𝑊)𝑋) ∈ ((LSpan‘𝑊)‘(𝐹 ∖ {𝑋}))))
152	151	notbid 320	. . . . . . 7 ⊢ (𝑥 = 𝑋 → (¬ (𝑘( ·_𝑠 ‘𝑊)𝑥) ∈ ((LSpan‘𝑊)‘((𝐹 ∪ {𝑋}) ∖ {𝑥})) ↔ ¬ (𝑘( ·_𝑠 ‘𝑊)𝑋) ∈ ((LSpan‘𝑊)‘(𝐹 ∖ {𝑋}))))
153	152	ralbidv 3184	. . . . . 6 ⊢ (𝑥 = 𝑋 → (∀𝑘 ∈ ((Base‘(Scalar‘𝑊)) ∖ {(0_g‘(Scalar‘𝑊))}) ¬ (𝑘( ·_𝑠 ‘𝑊)𝑥) ∈ ((LSpan‘𝑊)‘((𝐹 ∪ {𝑋}) ∖ {𝑥})) ↔ ∀𝑘 ∈ ((Base‘(Scalar‘𝑊)) ∖ {(0_g‘(Scalar‘𝑊))}) ¬ (𝑘( ·_𝑠 ‘𝑊)𝑋) ∈ ((LSpan‘𝑊)‘(𝐹 ∖ {𝑋}))))
154	153	ralsng 4631	. . . . 5 ⊢ (𝑋 ∈ ((Base‘𝑊) ∖ ((LSpan‘𝑊)‘𝐹)) → (∀𝑥 ∈ {𝑋}∀𝑘 ∈ ((Base‘(Scalar‘𝑊)) ∖ {(0_g‘(Scalar‘𝑊))}) ¬ (𝑘( ·_𝑠 ‘𝑊)𝑥) ∈ ((LSpan‘𝑊)‘((𝐹 ∪ {𝑋}) ∖ {𝑥})) ↔ ∀𝑘 ∈ ((Base‘(Scalar‘𝑊)) ∖ {(0_g‘(Scalar‘𝑊))}) ¬ (𝑘( ·_𝑠 ‘𝑊)𝑋) ∈ ((LSpan‘𝑊)‘(𝐹 ∖ {𝑋}))))
155	154	3ad2ant3 1147	. . . 4 ⊢ ((𝑊 ∈ LVec ∧ 𝐹 ∈ (LIndS‘𝑊) ∧ 𝑋 ∈ ((Base‘𝑊) ∖ ((LSpan‘𝑊)‘𝐹))) → (∀𝑥 ∈ {𝑋}∀𝑘 ∈ ((Base‘(Scalar‘𝑊)) ∖ {(0_g‘(Scalar‘𝑊))}) ¬ (𝑘( ·_𝑠 ‘𝑊)𝑥) ∈ ((LSpan‘𝑊)‘((𝐹 ∪ {𝑋}) ∖ {𝑥})) ↔ ∀𝑘 ∈ ((Base‘(Scalar‘𝑊)) ∖ {(0_g‘(Scalar‘𝑊))}) ¬ (𝑘( ·_𝑠 ‘𝑊)𝑋) ∈ ((LSpan‘𝑊)‘(𝐹 ∖ {𝑋}))))
156	144, 155	mpbird 259	. . 3 ⊢ ((𝑊 ∈ LVec ∧ 𝐹 ∈ (LIndS‘𝑊) ∧ 𝑋 ∈ ((Base‘𝑊) ∖ ((LSpan‘𝑊)‘𝐹))) → ∀𝑥 ∈ {𝑋}∀𝑘 ∈ ((Base‘(Scalar‘𝑊)) ∖ {(0_g‘(Scalar‘𝑊))}) ¬ (𝑘( ·_𝑠 ‘𝑊)𝑥) ∈ ((LSpan‘𝑊)‘((𝐹 ∪ {𝑋}) ∖ {𝑥})))
157		ralunb 4147	. . 3 ⊢ (∀𝑥 ∈ (𝐹 ∪ {𝑋})∀𝑘 ∈ ((Base‘(Scalar‘𝑊)) ∖ {(0_g‘(Scalar‘𝑊))}) ¬ (𝑘( ·_𝑠 ‘𝑊)𝑥) ∈ ((LSpan‘𝑊)‘((𝐹 ∪ {𝑋}) ∖ {𝑥})) ↔ (∀𝑥 ∈ 𝐹 ∀𝑘 ∈ ((Base‘(Scalar‘𝑊)) ∖ {(0_g‘(Scalar‘𝑊))}) ¬ (𝑘( ·_𝑠 ‘𝑊)𝑥) ∈ ((LSpan‘𝑊)‘((𝐹 ∪ {𝑋}) ∖ {𝑥})) ∧ ∀𝑥 ∈ {𝑋}∀𝑘 ∈ ((Base‘(Scalar‘𝑊)) ∖ {(0_g‘(Scalar‘𝑊))}) ¬ (𝑘( ·_𝑠 ‘𝑊)𝑥) ∈ ((LSpan‘𝑊)‘((𝐹 ∪ {𝑋}) ∖ {𝑥}))))
158	112, 156, 157	sylanbrc 592	. 2 ⊢ ((𝑊 ∈ LVec ∧ 𝐹 ∈ (LIndS‘𝑊) ∧ 𝑋 ∈ ((Base‘𝑊) ∖ ((LSpan‘𝑊)‘𝐹))) → ∀𝑥 ∈ (𝐹 ∪ {𝑋})∀𝑘 ∈ ((Base‘(Scalar‘𝑊)) ∖ {(0_g‘(Scalar‘𝑊))}) ¬ (𝑘( ·_𝑠 ‘𝑊)𝑥) ∈ ((LSpan‘𝑊)‘((𝐹 ∪ {𝑋}) ∖ {𝑥})))
159	1, 74, 31, 21, 25, 24	islinds2 21852	. . 3 ⊢ (𝑊 ∈ LVec → ((𝐹 ∪ {𝑋}) ∈ (LIndS‘𝑊) ↔ ((𝐹 ∪ {𝑋}) ⊆ (Base‘𝑊) ∧ ∀𝑥 ∈ (𝐹 ∪ {𝑋})∀𝑘 ∈ ((Base‘(Scalar‘𝑊)) ∖ {(0_g‘(Scalar‘𝑊))}) ¬ (𝑘( ·_𝑠 ‘𝑊)𝑥) ∈ ((LSpan‘𝑊)‘((𝐹 ∪ {𝑋}) ∖ {𝑥})))))
160	159	3ad2ant1 1145	. 2 ⊢ ((𝑊 ∈ LVec ∧ 𝐹 ∈ (LIndS‘𝑊) ∧ 𝑋 ∈ ((Base‘𝑊) ∖ ((LSpan‘𝑊)‘𝐹))) → ((𝐹 ∪ {𝑋}) ∈ (LIndS‘𝑊) ↔ ((𝐹 ∪ {𝑋}) ⊆ (Base‘𝑊) ∧ ∀𝑥 ∈ (𝐹 ∪ {𝑋})∀𝑘 ∈ ((Base‘(Scalar‘𝑊)) ∖ {(0_g‘(Scalar‘𝑊))}) ¬ (𝑘( ·_𝑠 ‘𝑊)𝑥) ∈ ((LSpan‘𝑊)‘((𝐹 ∪ {𝑋}) ∖ {𝑥})))))
161	8, 158, 160	mpbir2and 723	1 ⊢ ((𝑊 ∈ LVec ∧ 𝐹 ∈ (LIndS‘𝑊) ∧ 𝑋 ∈ ((Base‘𝑊) ∖ ((LSpan‘𝑊)‘𝐹))) → (𝐹 ∪ {𝑋}) ∈ (LIndS‘𝑊))

Colors of variables: wff setvar class

Syntax hints: ¬ wn 3 → wi 4 ↔ wb 208 ∧ wa 399 ∧ w3a 1097 = wceq 1559 ∈ wcel 2141 ≠ wne 2956 ∀wral 3075 ∖ cdif 3899 ∪ cun 3900 ∩ cin 3901 ⊆ wss 3902 ∅c0 4283 {csn 4579 ‘cfv 6515 (class class class)co 7390 Basecbs 17235 Scalarcsca 17279 ·_𝑠 cvsca 17280 0_gc0g 17458 Ringcrg 20269 NzRingcnzr 20548 LModclmod 20914 LSubSpclss 20985 LSpanclspn 21025 LVecclvec 21156 LIndSclinds 21844

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1814 ax-4 1828 ax-5 1929 ax-6 1986 ax-7 2027 ax-8 2143 ax-9 2151 ax-10 2174 ax-11 2190 ax-12 2211 ax-ext 2733 ax-rep 5224 ax-sep 5243 ax-nul 5253 ax-pow 5319 ax-pr 5387 ax-un 7712 ax-cnex 11122 ax-resscn 11123 ax-1cn 11124 ax-icn 11125 ax-addcl 11126 ax-addrcl 11127 ax-mulcl 11128 ax-mulrcl 11129 ax-mulcom 11130 ax-addass 11131 ax-mulass 11132 ax-distr 11133 ax-i2m1 11134 ax-1ne0 11135 ax-1rid 11136 ax-rnegex 11137 ax-rrecex 11138 ax-cnre 11139 ax-pre-lttri 11140 ax-pre-lttrn 11141 ax-pre-ltadd 11142 ax-pre-mulgt0 11143

This theorem depends on definitions: df-bi 209 df-an 400 df-or 859 df-3or 1098 df-3an 1099 df-tru 1562 df-fal 1572 df-ex 1799 df-nf 1803 df-sb 2090 df-mo 2565 df-eu 2595 df-clab 2740 df-cleq 2753 df-clel 2836 df-nfc 2910 df-ne 2957 df-nel 3061 df-ral 3076 df-rex 3086 df-rmo 3366 df-reu 3367 df-rab 3414 df-v 3455 df-sbc 3743 df-csb 3851 df-dif 3905 df-un 3907 df-in 3909 df-ss 3919 df-pss 3922 df-nul 4284 df-if 4478 df-pw 4554 df-sn 4580 df-pr 4582 df-op 4586 df-uni 4863 df-int 4903 df-iun 4948 df-br 5098 df-opab 5160 df-mpt 5179 df-tr 5205 df-id 5538 df-eprel 5543 df-po 5551 df-so 5552 df-fr 5596 df-we 5598 df-xp 5649 df-rel 5650 df-cnv 5651 df-co 5652 df-dm 5653 df-rn 5654 df-res 5655 df-ima 5656 df-pred 6282 df-ord 6343 df-on 6344 df-lim 6345 df-suc 6346 df-iota 6471 df-fun 6517 df-fn 6518 df-f 6519 df-f1 6520 df-fo 6521 df-f1o 6522 df-fv 6523 df-riota 7347 df-ov 7393 df-oprab 7394 df-mpo 7395 df-om 7841 df-1st 7964 df-2nd 7965 df-tpos 8199 df-frecs 8255 df-wrecs 8286 df-recs 8335 df-rdg 8374 df-er 8671 df-en 8921 df-dom 8922 df-sdom 8923 df-pnf 11211 df-mnf 11212 df-xr 11213 df-ltxr 11214 df-le 11215 df-sub 11409 df-neg 11410 df-nn 12204 df-2 12273 df-3 12274 df-sets 17190 df-slot 17208 df-ndx 17220 df-base 17236 df-ress 17257 df-plusg 17289 df-mulr 17290 df-0g 17460 df-mgm 18664 df-sgrp 18743 df-mnd 18759 df-grp 18968 df-minusg 18969 df-sbg 18970 df-cmn 19812 df-abl 19813 df-mgp 20177 df-rng 20189 df-ur 20218 df-ring 20271 df-oppr 20372 df-dvdsr 20392 df-unit 20393 df-invr 20423 df-nzr 20549 df-drng 20767 df-lmod 20916 df-lss 20986 df-lsp 21026 df-lvec 21157 df-lindf 21845 df-linds 21846

This theorem is referenced by: (None)

W3C validator