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 37621

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 2736	. . . . 5 ⊢ (Base‘𝑊) = (Base‘𝑊)
2	1	linds1 21831	. . . 4 ⊢ (𝐹 ∈ (LIndS‘𝑊) → 𝐹 ⊆ (Base‘𝑊))
3		eldifi 4130	. . . . 5 ⊢ (𝑋 ∈ ((Base‘𝑊) ∖ ((LSpan‘𝑊)‘𝐹)) → 𝑋 ∈ (Base‘𝑊))
4	3	snssd 4808	. . . 4 ⊢ (𝑋 ∈ ((Base‘𝑊) ∖ ((LSpan‘𝑊)‘𝐹)) → {𝑋} ⊆ (Base‘𝑊))
5		unss 4189	. . . . 5 ⊢ ((𝐹 ⊆ (Base‘𝑊) ∧ {𝑋} ⊆ (Base‘𝑊)) ↔ (𝐹 ∪ {𝑋}) ⊆ (Base‘𝑊))
6	5	biimpi 216	. . . 4 ⊢ ((𝐹 ⊆ (Base‘𝑊) ∧ {𝑋} ⊆ (Base‘𝑊)) → (𝐹 ∪ {𝑋}) ⊆ (Base‘𝑊))
7	2, 4, 6	syl2an 596	. . 3 ⊢ ((𝐹 ∈ (LIndS‘𝑊) ∧ 𝑋 ∈ ((Base‘𝑊) ∖ ((LSpan‘𝑊)‘𝐹))) → (𝐹 ∪ {𝑋}) ⊆ (Base‘𝑊))
8	7	3adant1 1130	. 2 ⊢ ((𝑊 ∈ LVec ∧ 𝐹 ∈ (LIndS‘𝑊) ∧ 𝑋 ∈ ((Base‘𝑊) ∖ ((LSpan‘𝑊)‘𝐹))) → (𝐹 ∪ {𝑋}) ⊆ (Base‘𝑊))
9		eldifn 4131	. . . . . . 7 ⊢ (𝑋 ∈ ((Base‘𝑊) ∖ ((LSpan‘𝑊)‘𝐹)) → ¬ 𝑋 ∈ ((LSpan‘𝑊)‘𝐹))
10	9	3ad2ant3 1135	. . . . . 6 ⊢ ((𝑊 ∈ LVec ∧ 𝐹 ∈ (LIndS‘𝑊) ∧ 𝑋 ∈ ((Base‘𝑊) ∖ ((LSpan‘𝑊)‘𝐹))) → ¬ 𝑋 ∈ ((LSpan‘𝑊)‘𝐹))
11	10	adantr 480	. . . . 5 ⊢ (((𝑊 ∈ LVec ∧ 𝐹 ∈ (LIndS‘𝑊) ∧ 𝑋 ∈ ((Base‘𝑊) ∖ ((LSpan‘𝑊)‘𝐹))) ∧ (𝑥 ∈ 𝐹 ∧ 𝑘 ∈ ((Base‘(Scalar‘𝑊)) ∖ {(0_g‘(Scalar‘𝑊))}))) → ¬ 𝑋 ∈ ((LSpan‘𝑊)‘𝐹))
12		simpll1 1212	. . . . . . . 8 ⊢ ((((𝑊 ∈ LVec ∧ 𝐹 ∈ (LIndS‘𝑊) ∧ 𝑋 ∈ ((Base‘𝑊) ∖ ((LSpan‘𝑊)‘𝐹))) ∧ (𝑥 ∈ 𝐹 ∧ 𝑘 ∈ ((Base‘(Scalar‘𝑊)) ∖ {(0_g‘(Scalar‘𝑊))}))) ∧ 𝑥 ∈ ((LSpan‘𝑊)‘((𝐹 ∖ {𝑥}) ∪ {𝑋}))) → 𝑊 ∈ LVec)
13	2	ssdifssd 4146	. . . . . . . . . 10 ⊢ (𝐹 ∈ (LIndS‘𝑊) → (𝐹 ∖ {𝑥}) ⊆ (Base‘𝑊))
14	13	3ad2ant2 1134	. . . . . . . . 9 ⊢ ((𝑊 ∈ LVec ∧ 𝐹 ∈ (LIndS‘𝑊) ∧ 𝑋 ∈ ((Base‘𝑊) ∖ ((LSpan‘𝑊)‘𝐹))) → (𝐹 ∖ {𝑥}) ⊆ (Base‘𝑊))
15	14	ad2antrr 726	. . . . . . . 8 ⊢ ((((𝑊 ∈ LVec ∧ 𝐹 ∈ (LIndS‘𝑊) ∧ 𝑋 ∈ ((Base‘𝑊) ∖ ((LSpan‘𝑊)‘𝐹))) ∧ (𝑥 ∈ 𝐹 ∧ 𝑘 ∈ ((Base‘(Scalar‘𝑊)) ∖ {(0_g‘(Scalar‘𝑊))}))) ∧ 𝑥 ∈ ((LSpan‘𝑊)‘((𝐹 ∖ {𝑥}) ∪ {𝑋}))) → (𝐹 ∖ {𝑥}) ⊆ (Base‘𝑊))
16	3	3ad2ant3 1135	. . . . . . . . 9 ⊢ ((𝑊 ∈ LVec ∧ 𝐹 ∈ (LIndS‘𝑊) ∧ 𝑋 ∈ ((Base‘𝑊) ∖ ((LSpan‘𝑊)‘𝐹))) → 𝑋 ∈ (Base‘𝑊))
17	16	ad2antrr 726	. . . . . . . 8 ⊢ ((((𝑊 ∈ LVec ∧ 𝐹 ∈ (LIndS‘𝑊) ∧ 𝑋 ∈ ((Base‘𝑊) ∖ ((LSpan‘𝑊)‘𝐹))) ∧ (𝑥 ∈ 𝐹 ∧ 𝑘 ∈ ((Base‘(Scalar‘𝑊)) ∖ {(0_g‘(Scalar‘𝑊))}))) ∧ 𝑥 ∈ ((LSpan‘𝑊)‘((𝐹 ∖ {𝑥}) ∪ {𝑋}))) → 𝑋 ∈ (Base‘𝑊))
18		simpr 484	. . . . . . . . 9 ⊢ ((((𝑊 ∈ LVec ∧ 𝐹 ∈ (LIndS‘𝑊) ∧ 𝑋 ∈ ((Base‘𝑊) ∖ ((LSpan‘𝑊)‘𝐹))) ∧ (𝑥 ∈ 𝐹 ∧ 𝑘 ∈ ((Base‘(Scalar‘𝑊)) ∖ {(0_g‘(Scalar‘𝑊))}))) ∧ 𝑥 ∈ ((LSpan‘𝑊)‘((𝐹 ∖ {𝑥}) ∪ {𝑋}))) → 𝑥 ∈ ((LSpan‘𝑊)‘((𝐹 ∖ {𝑥}) ∪ {𝑋})))
19		lveclmod 21106	. . . . . . . . . . . . 13 ⊢ (𝑊 ∈ LVec → 𝑊 ∈ LMod)
20	19	ad2antrr 726	. . . . . . . . . . . 12 ⊢ (((𝑊 ∈ LVec ∧ 𝐹 ∈ (LIndS‘𝑊)) ∧ (𝑥 ∈ 𝐹 ∧ 𝑘 ∈ ((Base‘(Scalar‘𝑊)) ∖ {(0_g‘(Scalar‘𝑊))}))) → 𝑊 ∈ LMod)
21		eqid 2736	. . . . . . . . . . . . . . . 16 ⊢ (Scalar‘𝑊) = (Scalar‘𝑊)
22	21	lmodring 20867	. . . . . . . . . . . . . . 15 ⊢ (𝑊 ∈ LMod → (Scalar‘𝑊) ∈ Ring)
23	19, 22	syl 17	. . . . . . . . . . . . . 14 ⊢ (𝑊 ∈ LVec → (Scalar‘𝑊) ∈ Ring)
24		eqid 2736	. . . . . . . . . . . . . . 15 ⊢ (0_g‘(Scalar‘𝑊)) = (0_g‘(Scalar‘𝑊))
25		eqid 2736	. . . . . . . . . . . . . . 15 ⊢ (Base‘(Scalar‘𝑊)) = (Base‘(Scalar‘𝑊))
26	24, 25	ringelnzr 20524	. . . . . . . . . . . . . 14 ⊢ (((Scalar‘𝑊) ∈ Ring ∧ 𝑘 ∈ ((Base‘(Scalar‘𝑊)) ∖ {(0_g‘(Scalar‘𝑊))})) → (Scalar‘𝑊) ∈ NzRing)
27	23, 26	sylan 580	. . . . . . . . . . . . 13 ⊢ ((𝑊 ∈ LVec ∧ 𝑘 ∈ ((Base‘(Scalar‘𝑊)) ∖ {(0_g‘(Scalar‘𝑊))})) → (Scalar‘𝑊) ∈ NzRing)
28	27	ad2ant2rl 749	. . . . . . . . . . . 12 ⊢ (((𝑊 ∈ LVec ∧ 𝐹 ∈ (LIndS‘𝑊)) ∧ (𝑥 ∈ 𝐹 ∧ 𝑘 ∈ ((Base‘(Scalar‘𝑊)) ∖ {(0_g‘(Scalar‘𝑊))}))) → (Scalar‘𝑊) ∈ NzRing)
29		simplr 768	. . . . . . . . . . . 12 ⊢ (((𝑊 ∈ LVec ∧ 𝐹 ∈ (LIndS‘𝑊)) ∧ (𝑥 ∈ 𝐹 ∧ 𝑘 ∈ ((Base‘(Scalar‘𝑊)) ∖ {(0_g‘(Scalar‘𝑊))}))) → 𝐹 ∈ (LIndS‘𝑊))
30		simprl 770	. . . . . . . . . . . 12 ⊢ (((𝑊 ∈ LVec ∧ 𝐹 ∈ (LIndS‘𝑊)) ∧ (𝑥 ∈ 𝐹 ∧ 𝑘 ∈ ((Base‘(Scalar‘𝑊)) ∖ {(0_g‘(Scalar‘𝑊))}))) → 𝑥 ∈ 𝐹)
31		eqid 2736	. . . . . . . . . . . . 13 ⊢ (LSpan‘𝑊) = (LSpan‘𝑊)
32	31, 21	lindsind2 21840	. . . . . . . . . . . 12 ⊢ (((𝑊 ∈ LMod ∧ (Scalar‘𝑊) ∈ NzRing) ∧ 𝐹 ∈ (LIndS‘𝑊) ∧ 𝑥 ∈ 𝐹) → ¬ 𝑥 ∈ ((LSpan‘𝑊)‘(𝐹 ∖ {𝑥})))
33	20, 28, 29, 30, 32	syl211anc 1377	. . . . . . . . . . 11 ⊢ (((𝑊 ∈ LVec ∧ 𝐹 ∈ (LIndS‘𝑊)) ∧ (𝑥 ∈ 𝐹 ∧ 𝑘 ∈ ((Base‘(Scalar‘𝑊)) ∖ {(0_g‘(Scalar‘𝑊))}))) → ¬ 𝑥 ∈ ((LSpan‘𝑊)‘(𝐹 ∖ {𝑥})))
34	33	3adantl3 1168	. . . . . . . . . 10 ⊢ (((𝑊 ∈ LVec ∧ 𝐹 ∈ (LIndS‘𝑊) ∧ 𝑋 ∈ ((Base‘𝑊) ∖ ((LSpan‘𝑊)‘𝐹))) ∧ (𝑥 ∈ 𝐹 ∧ 𝑘 ∈ ((Base‘(Scalar‘𝑊)) ∖ {(0_g‘(Scalar‘𝑊))}))) → ¬ 𝑥 ∈ ((LSpan‘𝑊)‘(𝐹 ∖ {𝑥})))
35	34	adantr 480	. . . . . . . . 9 ⊢ ((((𝑊 ∈ LVec ∧ 𝐹 ∈ (LIndS‘𝑊) ∧ 𝑋 ∈ ((Base‘𝑊) ∖ ((LSpan‘𝑊)‘𝐹))) ∧ (𝑥 ∈ 𝐹 ∧ 𝑘 ∈ ((Base‘(Scalar‘𝑊)) ∖ {(0_g‘(Scalar‘𝑊))}))) ∧ 𝑥 ∈ ((LSpan‘𝑊)‘((𝐹 ∖ {𝑥}) ∪ {𝑋}))) → ¬ 𝑥 ∈ ((LSpan‘𝑊)‘(𝐹 ∖ {𝑥})))
36	18, 35	eldifd 3961	. . . . . . . 8 ⊢ ((((𝑊 ∈ LVec ∧ 𝐹 ∈ (LIndS‘𝑊) ∧ 𝑋 ∈ ((Base‘𝑊) ∖ ((LSpan‘𝑊)‘𝐹))) ∧ (𝑥 ∈ 𝐹 ∧ 𝑘 ∈ ((Base‘(Scalar‘𝑊)) ∖ {(0_g‘(Scalar‘𝑊))}))) ∧ 𝑥 ∈ ((LSpan‘𝑊)‘((𝐹 ∖ {𝑥}) ∪ {𝑋}))) → 𝑥 ∈ (((LSpan‘𝑊)‘((𝐹 ∖ {𝑥}) ∪ {𝑋})) ∖ ((LSpan‘𝑊)‘(𝐹 ∖ {𝑥}))))
37		eqid 2736	. . . . . . . . 9 ⊢ (LSubSp‘𝑊) = (LSubSp‘𝑊)
38	1, 37, 31	lspsolv 21146	. . . . . . . 8 ⊢ ((𝑊 ∈ LVec ∧ ((𝐹 ∖ {𝑥}) ⊆ (Base‘𝑊) ∧ 𝑋 ∈ (Base‘𝑊) ∧ 𝑥 ∈ (((LSpan‘𝑊)‘((𝐹 ∖ {𝑥}) ∪ {𝑋})) ∖ ((LSpan‘𝑊)‘(𝐹 ∖ {𝑥}))))) → 𝑋 ∈ ((LSpan‘𝑊)‘((𝐹 ∖ {𝑥}) ∪ {𝑥})))
39	12, 15, 17, 36, 38	syl13anc 1373	. . . . . . 7 ⊢ ((((𝑊 ∈ LVec ∧ 𝐹 ∈ (LIndS‘𝑊) ∧ 𝑋 ∈ ((Base‘𝑊) ∖ ((LSpan‘𝑊)‘𝐹))) ∧ (𝑥 ∈ 𝐹 ∧ 𝑘 ∈ ((Base‘(Scalar‘𝑊)) ∖ {(0_g‘(Scalar‘𝑊))}))) ∧ 𝑥 ∈ ((LSpan‘𝑊)‘((𝐹 ∖ {𝑥}) ∪ {𝑋}))) → 𝑋 ∈ ((LSpan‘𝑊)‘((𝐹 ∖ {𝑥}) ∪ {𝑥})))
40	39	ex 412	. . . . . 6 ⊢ (((𝑊 ∈ LVec ∧ 𝐹 ∈ (LIndS‘𝑊) ∧ 𝑋 ∈ ((Base‘𝑊) ∖ ((LSpan‘𝑊)‘𝐹))) ∧ (𝑥 ∈ 𝐹 ∧ 𝑘 ∈ ((Base‘(Scalar‘𝑊)) ∖ {(0_g‘(Scalar‘𝑊))}))) → (𝑥 ∈ ((LSpan‘𝑊)‘((𝐹 ∖ {𝑥}) ∪ {𝑋})) → 𝑋 ∈ ((LSpan‘𝑊)‘((𝐹 ∖ {𝑥}) ∪ {𝑥}))))
41		eldif 3960	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑋 ∈ ((Base‘𝑊) ∖ ((LSpan‘𝑊)‘𝐹)) ↔ (𝑋 ∈ (Base‘𝑊) ∧ ¬ 𝑋 ∈ ((LSpan‘𝑊)‘𝐹)))
42		snssi 4807	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝑋 ∈ 𝐹 → {𝑋} ⊆ 𝐹)
43	1, 31	lspss 20983	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((𝑊 ∈ LMod ∧ 𝐹 ⊆ (Base‘𝑊) ∧ {𝑋} ⊆ 𝐹) → ((LSpan‘𝑊)‘{𝑋}) ⊆ ((LSpan‘𝑊)‘𝐹))
44	19, 2, 42, 43	syl3an 1160	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝑊 ∈ LVec ∧ 𝐹 ∈ (LIndS‘𝑊) ∧ 𝑋 ∈ 𝐹) → ((LSpan‘𝑊)‘{𝑋}) ⊆ ((LSpan‘𝑊)‘𝐹))
45	44	ad4ant124 1173	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((((𝑊 ∈ LVec ∧ 𝐹 ∈ (LIndS‘𝑊)) ∧ 𝑋 ∈ (Base‘𝑊)) ∧ 𝑋 ∈ 𝐹) → ((LSpan‘𝑊)‘{𝑋}) ⊆ ((LSpan‘𝑊)‘𝐹))
46	1, 31	lspsnid 20992	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((𝑊 ∈ LMod ∧ 𝑋 ∈ (Base‘𝑊)) → 𝑋 ∈ ((LSpan‘𝑊)‘{𝑋}))
47	19, 46	sylan 580	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝑊 ∈ LVec ∧ 𝑋 ∈ (Base‘𝑊)) → 𝑋 ∈ ((LSpan‘𝑊)‘{𝑋}))
48	47	ad4ant13 751	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((((𝑊 ∈ LVec ∧ 𝐹 ∈ (LIndS‘𝑊)) ∧ 𝑋 ∈ (Base‘𝑊)) ∧ 𝑋 ∈ 𝐹) → 𝑋 ∈ ((LSpan‘𝑊)‘{𝑋}))
49	45, 48	sseldd 3983	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((((𝑊 ∈ LVec ∧ 𝐹 ∈ (LIndS‘𝑊)) ∧ 𝑋 ∈ (Base‘𝑊)) ∧ 𝑋 ∈ 𝐹) → 𝑋 ∈ ((LSpan‘𝑊)‘𝐹))
50	49	ex 412	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝑊 ∈ LVec ∧ 𝐹 ∈ (LIndS‘𝑊)) ∧ 𝑋 ∈ (Base‘𝑊)) → (𝑋 ∈ 𝐹 → 𝑋 ∈ ((LSpan‘𝑊)‘𝐹)))
51	50	con3d 152	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝑊 ∈ LVec ∧ 𝐹 ∈ (LIndS‘𝑊)) ∧ 𝑋 ∈ (Base‘𝑊)) → (¬ 𝑋 ∈ ((LSpan‘𝑊)‘𝐹) → ¬ 𝑋 ∈ 𝐹))
52	51	expimpd 453	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑊 ∈ LVec ∧ 𝐹 ∈ (LIndS‘𝑊)) → ((𝑋 ∈ (Base‘𝑊) ∧ ¬ 𝑋 ∈ ((LSpan‘𝑊)‘𝐹)) → ¬ 𝑋 ∈ 𝐹))
53	52	3impia 1117	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑊 ∈ LVec ∧ 𝐹 ∈ (LIndS‘𝑊) ∧ (𝑋 ∈ (Base‘𝑊) ∧ ¬ 𝑋 ∈ ((LSpan‘𝑊)‘𝐹))) → ¬ 𝑋 ∈ 𝐹)
54	41, 53	syl3an3b 1406	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑊 ∈ LVec ∧ 𝐹 ∈ (LIndS‘𝑊) ∧ 𝑋 ∈ ((Base‘𝑊) ∖ ((LSpan‘𝑊)‘𝐹))) → ¬ 𝑋 ∈ 𝐹)
55		eleq1 2828	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑋 = 𝑥 → (𝑋 ∈ 𝐹 ↔ 𝑥 ∈ 𝐹))
56	55	notbid 318	. . . . . . . . . . . . . . . . 17 ⊢ (𝑋 = 𝑥 → (¬ 𝑋 ∈ 𝐹 ↔ ¬ 𝑥 ∈ 𝐹))
57	54, 56	syl5ibcom 245	. . . . . . . . . . . . . . . 16 ⊢ ((𝑊 ∈ LVec ∧ 𝐹 ∈ (LIndS‘𝑊) ∧ 𝑋 ∈ ((Base‘𝑊) ∖ ((LSpan‘𝑊)‘𝐹))) → (𝑋 = 𝑥 → ¬ 𝑥 ∈ 𝐹))
58	57	necon2ad 2954	. . . . . . . . . . . . . . 15 ⊢ ((𝑊 ∈ LVec ∧ 𝐹 ∈ (LIndS‘𝑊) ∧ 𝑋 ∈ ((Base‘𝑊) ∖ ((LSpan‘𝑊)‘𝐹))) → (𝑥 ∈ 𝐹 → 𝑋 ≠ 𝑥))
59	58	imp 406	. . . . . . . . . . . . . 14 ⊢ (((𝑊 ∈ LVec ∧ 𝐹 ∈ (LIndS‘𝑊) ∧ 𝑋 ∈ ((Base‘𝑊) ∖ ((LSpan‘𝑊)‘𝐹))) ∧ 𝑥 ∈ 𝐹) → 𝑋 ≠ 𝑥)
60		disjsn2 4711	. . . . . . . . . . . . . 14 ⊢ (𝑋 ≠ 𝑥 → ({𝑋} ∩ {𝑥}) = ∅)
61	59, 60	syl 17	. . . . . . . . . . . . 13 ⊢ (((𝑊 ∈ LVec ∧ 𝐹 ∈ (LIndS‘𝑊) ∧ 𝑋 ∈ ((Base‘𝑊) ∖ ((LSpan‘𝑊)‘𝐹))) ∧ 𝑥 ∈ 𝐹) → ({𝑋} ∩ {𝑥}) = ∅)
62		disj3 4453	. . . . . . . . . . . . 13 ⊢ (({𝑋} ∩ {𝑥}) = ∅ ↔ {𝑋} = ({𝑋} ∖ {𝑥}))
63	61, 62	sylib 218	. . . . . . . . . . . 12 ⊢ (((𝑊 ∈ LVec ∧ 𝐹 ∈ (LIndS‘𝑊) ∧ 𝑋 ∈ ((Base‘𝑊) ∖ ((LSpan‘𝑊)‘𝐹))) ∧ 𝑥 ∈ 𝐹) → {𝑋} = ({𝑋} ∖ {𝑥}))
64	63	uneq2d 4167	. . . . . . . . . . 11 ⊢ (((𝑊 ∈ LVec ∧ 𝐹 ∈ (LIndS‘𝑊) ∧ 𝑋 ∈ ((Base‘𝑊) ∖ ((LSpan‘𝑊)‘𝐹))) ∧ 𝑥 ∈ 𝐹) → ((𝐹 ∖ {𝑥}) ∪ {𝑋}) = ((𝐹 ∖ {𝑥}) ∪ ({𝑋} ∖ {𝑥})))
65		difundir 4290	. . . . . . . . . . 11 ⊢ ((𝐹 ∪ {𝑋}) ∖ {𝑥}) = ((𝐹 ∖ {𝑥}) ∪ ({𝑋} ∖ {𝑥}))
66	64, 65	eqtr4di 2794	. . . . . . . . . 10 ⊢ (((𝑊 ∈ LVec ∧ 𝐹 ∈ (LIndS‘𝑊) ∧ 𝑋 ∈ ((Base‘𝑊) ∖ ((LSpan‘𝑊)‘𝐹))) ∧ 𝑥 ∈ 𝐹) → ((𝐹 ∖ {𝑥}) ∪ {𝑋}) = ((𝐹 ∪ {𝑋}) ∖ {𝑥}))
67	66	fveq2d 6909	. . . . . . . . 9 ⊢ (((𝑊 ∈ LVec ∧ 𝐹 ∈ (LIndS‘𝑊) ∧ 𝑋 ∈ ((Base‘𝑊) ∖ ((LSpan‘𝑊)‘𝐹))) ∧ 𝑥 ∈ 𝐹) → ((LSpan‘𝑊)‘((𝐹 ∖ {𝑥}) ∪ {𝑋})) = ((LSpan‘𝑊)‘((𝐹 ∪ {𝑋}) ∖ {𝑥})))
68	67	eleq2d 2826	. . . . . . . 8 ⊢ (((𝑊 ∈ LVec ∧ 𝐹 ∈ (LIndS‘𝑊) ∧ 𝑋 ∈ ((Base‘𝑊) ∖ ((LSpan‘𝑊)‘𝐹))) ∧ 𝑥 ∈ 𝐹) → (𝑥 ∈ ((LSpan‘𝑊)‘((𝐹 ∖ {𝑥}) ∪ {𝑋})) ↔ 𝑥 ∈ ((LSpan‘𝑊)‘((𝐹 ∪ {𝑋}) ∖ {𝑥}))))
69	68	adantrr 717	. . . . . . 7 ⊢ (((𝑊 ∈ LVec ∧ 𝐹 ∈ (LIndS‘𝑊) ∧ 𝑋 ∈ ((Base‘𝑊) ∖ ((LSpan‘𝑊)‘𝐹))) ∧ (𝑥 ∈ 𝐹 ∧ 𝑘 ∈ ((Base‘(Scalar‘𝑊)) ∖ {(0_g‘(Scalar‘𝑊))}))) → (𝑥 ∈ ((LSpan‘𝑊)‘((𝐹 ∖ {𝑥}) ∪ {𝑋})) ↔ 𝑥 ∈ ((LSpan‘𝑊)‘((𝐹 ∪ {𝑋}) ∖ {𝑥}))))
70		simpl 482	. . . . . . . . . . . . 13 ⊢ ((𝑊 ∈ LVec ∧ 𝑘 ∈ ((Base‘(Scalar‘𝑊)) ∖ {(0_g‘(Scalar‘𝑊))})) → 𝑊 ∈ LVec)
71		eldifsn 4785	. . . . . . . . . . . . . . 15 ⊢ (𝑘 ∈ ((Base‘(Scalar‘𝑊)) ∖ {(0_g‘(Scalar‘𝑊))}) ↔ (𝑘 ∈ (Base‘(Scalar‘𝑊)) ∧ 𝑘 ≠ (0_g‘(Scalar‘𝑊))))
72	71	biimpi 216	. . . . . . . . . . . . . 14 ⊢ (𝑘 ∈ ((Base‘(Scalar‘𝑊)) ∖ {(0_g‘(Scalar‘𝑊))}) → (𝑘 ∈ (Base‘(Scalar‘𝑊)) ∧ 𝑘 ≠ (0_g‘(Scalar‘𝑊))))
73	72	adantl 481	. . . . . . . . . . . . 13 ⊢ ((𝑊 ∈ LVec ∧ 𝑘 ∈ ((Base‘(Scalar‘𝑊)) ∖ {(0_g‘(Scalar‘𝑊))})) → (𝑘 ∈ (Base‘(Scalar‘𝑊)) ∧ 𝑘 ≠ (0_g‘(Scalar‘𝑊))))
74	2	sselda 3982	. . . . . . . . . . . . 13 ⊢ ((𝐹 ∈ (LIndS‘𝑊) ∧ 𝑥 ∈ 𝐹) → 𝑥 ∈ (Base‘𝑊))
75		eqid 2736	. . . . . . . . . . . . . 14 ⊢ ( ·_𝑠 ‘𝑊) = ( ·_𝑠 ‘𝑊)
76	1, 21, 75, 25, 24, 31	lspsnvs 21117	. . . . . . . . . . . . 13 ⊢ ((𝑊 ∈ LVec ∧ (𝑘 ∈ (Base‘(Scalar‘𝑊)) ∧ 𝑘 ≠ (0_g‘(Scalar‘𝑊))) ∧ 𝑥 ∈ (Base‘𝑊)) → ((LSpan‘𝑊)‘{(𝑘( ·_𝑠 ‘𝑊)𝑥)}) = ((LSpan‘𝑊)‘{𝑥}))
77	70, 73, 74, 76	syl2an3an 1423	. . . . . . . . . . . 12 ⊢ (((𝑊 ∈ LVec ∧ 𝑘 ∈ ((Base‘(Scalar‘𝑊)) ∖ {(0_g‘(Scalar‘𝑊))})) ∧ (𝐹 ∈ (LIndS‘𝑊) ∧ 𝑥 ∈ 𝐹)) → ((LSpan‘𝑊)‘{(𝑘( ·_𝑠 ‘𝑊)𝑥)}) = ((LSpan‘𝑊)‘{𝑥}))
78	77	an42s 661	. . . . . . . . . . 11 ⊢ (((𝑊 ∈ LVec ∧ 𝐹 ∈ (LIndS‘𝑊)) ∧ (𝑥 ∈ 𝐹 ∧ 𝑘 ∈ ((Base‘(Scalar‘𝑊)) ∖ {(0_g‘(Scalar‘𝑊))}))) → ((LSpan‘𝑊)‘{(𝑘( ·_𝑠 ‘𝑊)𝑥)}) = ((LSpan‘𝑊)‘{𝑥}))
79	78	sseq1d 4014	. . . . . . . . . 10 ⊢ (((𝑊 ∈ LVec ∧ 𝐹 ∈ (LIndS‘𝑊)) ∧ (𝑥 ∈ 𝐹 ∧ 𝑘 ∈ ((Base‘(Scalar‘𝑊)) ∖ {(0_g‘(Scalar‘𝑊))}))) → (((LSpan‘𝑊)‘{(𝑘( ·_𝑠 ‘𝑊)𝑥)}) ⊆ ((LSpan‘𝑊)‘((𝐹 ∪ {𝑋}) ∖ {𝑥})) ↔ ((LSpan‘𝑊)‘{𝑥}) ⊆ ((LSpan‘𝑊)‘((𝐹 ∪ {𝑋}) ∖ {𝑥}))))
80	79	3adantl3 1168	. . . . . . . . 9 ⊢ (((𝑊 ∈ LVec ∧ 𝐹 ∈ (LIndS‘𝑊) ∧ 𝑋 ∈ (Base‘𝑊)) ∧ (𝑥 ∈ 𝐹 ∧ 𝑘 ∈ ((Base‘(Scalar‘𝑊)) ∖ {(0_g‘(Scalar‘𝑊))}))) → (((LSpan‘𝑊)‘{(𝑘( ·_𝑠 ‘𝑊)𝑥)}) ⊆ ((LSpan‘𝑊)‘((𝐹 ∪ {𝑋}) ∖ {𝑥})) ↔ ((LSpan‘𝑊)‘{𝑥}) ⊆ ((LSpan‘𝑊)‘((𝐹 ∪ {𝑋}) ∖ {𝑥}))))
81		eldifi 4130	. . . . . . . . . 10 ⊢ (𝑘 ∈ ((Base‘(Scalar‘𝑊)) ∖ {(0_g‘(Scalar‘𝑊))}) → 𝑘 ∈ (Base‘(Scalar‘𝑊)))
82	19	3ad2ant1 1133	. . . . . . . . . . . 12 ⊢ ((𝑊 ∈ LVec ∧ 𝐹 ∈ (LIndS‘𝑊) ∧ 𝑋 ∈ (Base‘𝑊)) → 𝑊 ∈ LMod)
83	82	adantr 480	. . . . . . . . . . 11 ⊢ (((𝑊 ∈ LVec ∧ 𝐹 ∈ (LIndS‘𝑊) ∧ 𝑋 ∈ (Base‘𝑊)) ∧ (𝑥 ∈ 𝐹 ∧ 𝑘 ∈ (Base‘(Scalar‘𝑊)))) → 𝑊 ∈ LMod)
84		snssi 4807	. . . . . . . . . . . . . . . 16 ⊢ (𝑋 ∈ (Base‘𝑊) → {𝑋} ⊆ (Base‘𝑊))
85	2, 84, 6	syl2an 596	. . . . . . . . . . . . . . 15 ⊢ ((𝐹 ∈ (LIndS‘𝑊) ∧ 𝑋 ∈ (Base‘𝑊)) → (𝐹 ∪ {𝑋}) ⊆ (Base‘𝑊))
86	85	ssdifssd 4146	. . . . . . . . . . . . . 14 ⊢ ((𝐹 ∈ (LIndS‘𝑊) ∧ 𝑋 ∈ (Base‘𝑊)) → ((𝐹 ∪ {𝑋}) ∖ {𝑥}) ⊆ (Base‘𝑊))
87	1, 37, 31	lspcl 20975	. . . . . . . . . . . . . 14 ⊢ ((𝑊 ∈ LMod ∧ ((𝐹 ∪ {𝑋}) ∖ {𝑥}) ⊆ (Base‘𝑊)) → ((LSpan‘𝑊)‘((𝐹 ∪ {𝑋}) ∖ {𝑥})) ∈ (LSubSp‘𝑊))
88	19, 86, 87	syl2an 596	. . . . . . . . . . . . 13 ⊢ ((𝑊 ∈ LVec ∧ (𝐹 ∈ (LIndS‘𝑊) ∧ 𝑋 ∈ (Base‘𝑊))) → ((LSpan‘𝑊)‘((𝐹 ∪ {𝑋}) ∖ {𝑥})) ∈ (LSubSp‘𝑊))
89	88	3impb 1114	. . . . . . . . . . . 12 ⊢ ((𝑊 ∈ LVec ∧ 𝐹 ∈ (LIndS‘𝑊) ∧ 𝑋 ∈ (Base‘𝑊)) → ((LSpan‘𝑊)‘((𝐹 ∪ {𝑋}) ∖ {𝑥})) ∈ (LSubSp‘𝑊))
90	89	adantr 480	. . . . . . . . . . 11 ⊢ (((𝑊 ∈ LVec ∧ 𝐹 ∈ (LIndS‘𝑊) ∧ 𝑋 ∈ (Base‘𝑊)) ∧ (𝑥 ∈ 𝐹 ∧ 𝑘 ∈ (Base‘(Scalar‘𝑊)))) → ((LSpan‘𝑊)‘((𝐹 ∪ {𝑋}) ∖ {𝑥})) ∈ (LSubSp‘𝑊))
91	19	anim1i 615	. . . . . . . . . . . . . 14 ⊢ ((𝑊 ∈ LVec ∧ 𝑘 ∈ (Base‘(Scalar‘𝑊))) → (𝑊 ∈ LMod ∧ 𝑘 ∈ (Base‘(Scalar‘𝑊))))
92	1, 21, 75, 25	lmodvscl 20877	. . . . . . . . . . . . . . 15 ⊢ ((𝑊 ∈ LMod ∧ 𝑘 ∈ (Base‘(Scalar‘𝑊)) ∧ 𝑥 ∈ (Base‘𝑊)) → (𝑘( ·_𝑠 ‘𝑊)𝑥) ∈ (Base‘𝑊))
93	92	3expa 1118	. . . . . . . . . . . . . 14 ⊢ (((𝑊 ∈ LMod ∧ 𝑘 ∈ (Base‘(Scalar‘𝑊))) ∧ 𝑥 ∈ (Base‘𝑊)) → (𝑘( ·_𝑠 ‘𝑊)𝑥) ∈ (Base‘𝑊))
94	91, 74, 93	syl2an 596	. . . . . . . . . . . . 13 ⊢ (((𝑊 ∈ LVec ∧ 𝑘 ∈ (Base‘(Scalar‘𝑊))) ∧ (𝐹 ∈ (LIndS‘𝑊) ∧ 𝑥 ∈ 𝐹)) → (𝑘( ·_𝑠 ‘𝑊)𝑥) ∈ (Base‘𝑊))
95	94	an42s 661	. . . . . . . . . . . 12 ⊢ (((𝑊 ∈ LVec ∧ 𝐹 ∈ (LIndS‘𝑊)) ∧ (𝑥 ∈ 𝐹 ∧ 𝑘 ∈ (Base‘(Scalar‘𝑊)))) → (𝑘( ·_𝑠 ‘𝑊)𝑥) ∈ (Base‘𝑊))
96	95	3adantl3 1168	. . . . . . . . . . 11 ⊢ (((𝑊 ∈ LVec ∧ 𝐹 ∈ (LIndS‘𝑊) ∧ 𝑋 ∈ (Base‘𝑊)) ∧ (𝑥 ∈ 𝐹 ∧ 𝑘 ∈ (Base‘(Scalar‘𝑊)))) → (𝑘( ·_𝑠 ‘𝑊)𝑥) ∈ (Base‘𝑊))
97	1, 37, 31, 83, 90, 96	ellspsn5b 20994	. . . . . . . . . 10 ⊢ (((𝑊 ∈ LVec ∧ 𝐹 ∈ (LIndS‘𝑊) ∧ 𝑋 ∈ (Base‘𝑊)) ∧ (𝑥 ∈ 𝐹 ∧ 𝑘 ∈ (Base‘(Scalar‘𝑊)))) → ((𝑘( ·_𝑠 ‘𝑊)𝑥) ∈ ((LSpan‘𝑊)‘((𝐹 ∪ {𝑋}) ∖ {𝑥})) ↔ ((LSpan‘𝑊)‘{(𝑘( ·_𝑠 ‘𝑊)𝑥)}) ⊆ ((LSpan‘𝑊)‘((𝐹 ∪ {𝑋}) ∖ {𝑥}))))
98	81, 97	sylanr2 683	. . . . . . . . 9 ⊢ (((𝑊 ∈ LVec ∧ 𝐹 ∈ (LIndS‘𝑊) ∧ 𝑋 ∈ (Base‘𝑊)) ∧ (𝑥 ∈ 𝐹 ∧ 𝑘 ∈ ((Base‘(Scalar‘𝑊)) ∖ {(0_g‘(Scalar‘𝑊))}))) → ((𝑘( ·_𝑠 ‘𝑊)𝑥) ∈ ((LSpan‘𝑊)‘((𝐹 ∪ {𝑋}) ∖ {𝑥})) ↔ ((LSpan‘𝑊)‘{(𝑘( ·_𝑠 ‘𝑊)𝑥)}) ⊆ ((LSpan‘𝑊)‘((𝐹 ∪ {𝑋}) ∖ {𝑥}))))
99	82	adantr 480	. . . . . . . . . . 11 ⊢ (((𝑊 ∈ LVec ∧ 𝐹 ∈ (LIndS‘𝑊) ∧ 𝑋 ∈ (Base‘𝑊)) ∧ 𝑥 ∈ 𝐹) → 𝑊 ∈ LMod)
100	89	adantr 480	. . . . . . . . . . 11 ⊢ (((𝑊 ∈ LVec ∧ 𝐹 ∈ (LIndS‘𝑊) ∧ 𝑋 ∈ (Base‘𝑊)) ∧ 𝑥 ∈ 𝐹) → ((LSpan‘𝑊)‘((𝐹 ∪ {𝑋}) ∖ {𝑥})) ∈ (LSubSp‘𝑊))
101	74	3ad2antl2 1186	. . . . . . . . . . 11 ⊢ (((𝑊 ∈ LVec ∧ 𝐹 ∈ (LIndS‘𝑊) ∧ 𝑋 ∈ (Base‘𝑊)) ∧ 𝑥 ∈ 𝐹) → 𝑥 ∈ (Base‘𝑊))
102	1, 37, 31, 99, 100, 101	ellspsn5b 20994	. . . . . . . . . 10 ⊢ (((𝑊 ∈ LVec ∧ 𝐹 ∈ (LIndS‘𝑊) ∧ 𝑋 ∈ (Base‘𝑊)) ∧ 𝑥 ∈ 𝐹) → (𝑥 ∈ ((LSpan‘𝑊)‘((𝐹 ∪ {𝑋}) ∖ {𝑥})) ↔ ((LSpan‘𝑊)‘{𝑥}) ⊆ ((LSpan‘𝑊)‘((𝐹 ∪ {𝑋}) ∖ {𝑥}))))
103	102	adantrr 717	. . . . . . . . 9 ⊢ (((𝑊 ∈ LVec ∧ 𝐹 ∈ (LIndS‘𝑊) ∧ 𝑋 ∈ (Base‘𝑊)) ∧ (𝑥 ∈ 𝐹 ∧ 𝑘 ∈ ((Base‘(Scalar‘𝑊)) ∖ {(0_g‘(Scalar‘𝑊))}))) → (𝑥 ∈ ((LSpan‘𝑊)‘((𝐹 ∪ {𝑋}) ∖ {𝑥})) ↔ ((LSpan‘𝑊)‘{𝑥}) ⊆ ((LSpan‘𝑊)‘((𝐹 ∪ {𝑋}) ∖ {𝑥}))))
104	80, 98, 103	3bitr4rd 312	. . . . . . . 8 ⊢ (((𝑊 ∈ LVec ∧ 𝐹 ∈ (LIndS‘𝑊) ∧ 𝑋 ∈ (Base‘𝑊)) ∧ (𝑥 ∈ 𝐹 ∧ 𝑘 ∈ ((Base‘(Scalar‘𝑊)) ∖ {(0_g‘(Scalar‘𝑊))}))) → (𝑥 ∈ ((LSpan‘𝑊)‘((𝐹 ∪ {𝑋}) ∖ {𝑥})) ↔ (𝑘( ·_𝑠 ‘𝑊)𝑥) ∈ ((LSpan‘𝑊)‘((𝐹 ∪ {𝑋}) ∖ {𝑥}))))
105	3, 104	syl3anl3 1415	. . . . . . 7 ⊢ (((𝑊 ∈ LVec ∧ 𝐹 ∈ (LIndS‘𝑊) ∧ 𝑋 ∈ ((Base‘𝑊) ∖ ((LSpan‘𝑊)‘𝐹))) ∧ (𝑥 ∈ 𝐹 ∧ 𝑘 ∈ ((Base‘(Scalar‘𝑊)) ∖ {(0_g‘(Scalar‘𝑊))}))) → (𝑥 ∈ ((LSpan‘𝑊)‘((𝐹 ∪ {𝑋}) ∖ {𝑥})) ↔ (𝑘( ·_𝑠 ‘𝑊)𝑥) ∈ ((LSpan‘𝑊)‘((𝐹 ∪ {𝑋}) ∖ {𝑥}))))
106	69, 105	bitrd 279	. . . . . 6 ⊢ (((𝑊 ∈ LVec ∧ 𝐹 ∈ (LIndS‘𝑊) ∧ 𝑋 ∈ ((Base‘𝑊) ∖ ((LSpan‘𝑊)‘𝐹))) ∧ (𝑥 ∈ 𝐹 ∧ 𝑘 ∈ ((Base‘(Scalar‘𝑊)) ∖ {(0_g‘(Scalar‘𝑊))}))) → (𝑥 ∈ ((LSpan‘𝑊)‘((𝐹 ∖ {𝑥}) ∪ {𝑋})) ↔ (𝑘( ·_𝑠 ‘𝑊)𝑥) ∈ ((LSpan‘𝑊)‘((𝐹 ∪ {𝑋}) ∖ {𝑥}))))
107		difsnid 4809	. . . . . . . . 9 ⊢ (𝑥 ∈ 𝐹 → ((𝐹 ∖ {𝑥}) ∪ {𝑥}) = 𝐹)
108	107	fveq2d 6909	. . . . . . . 8 ⊢ (𝑥 ∈ 𝐹 → ((LSpan‘𝑊)‘((𝐹 ∖ {𝑥}) ∪ {𝑥})) = ((LSpan‘𝑊)‘𝐹))
109	108	eleq2d 2826	. . . . . . 7 ⊢ (𝑥 ∈ 𝐹 → (𝑋 ∈ ((LSpan‘𝑊)‘((𝐹 ∖ {𝑥}) ∪ {𝑥})) ↔ 𝑋 ∈ ((LSpan‘𝑊)‘𝐹)))
110	109	ad2antrl 728	. . . . . 6 ⊢ (((𝑊 ∈ LVec ∧ 𝐹 ∈ (LIndS‘𝑊) ∧ 𝑋 ∈ ((Base‘𝑊) ∖ ((LSpan‘𝑊)‘𝐹))) ∧ (𝑥 ∈ 𝐹 ∧ 𝑘 ∈ ((Base‘(Scalar‘𝑊)) ∖ {(0_g‘(Scalar‘𝑊))}))) → (𝑋 ∈ ((LSpan‘𝑊)‘((𝐹 ∖ {𝑥}) ∪ {𝑥})) ↔ 𝑋 ∈ ((LSpan‘𝑊)‘𝐹)))
111	40, 106, 110	3imtr3d 293	. . . . 5 ⊢ (((𝑊 ∈ LVec ∧ 𝐹 ∈ (LIndS‘𝑊) ∧ 𝑋 ∈ ((Base‘𝑊) ∖ ((LSpan‘𝑊)‘𝐹))) ∧ (𝑥 ∈ 𝐹 ∧ 𝑘 ∈ ((Base‘(Scalar‘𝑊)) ∖ {(0_g‘(Scalar‘𝑊))}))) → ((𝑘( ·_𝑠 ‘𝑊)𝑥) ∈ ((LSpan‘𝑊)‘((𝐹 ∪ {𝑋}) ∖ {𝑥})) → 𝑋 ∈ ((LSpan‘𝑊)‘𝐹)))
112	11, 111	mtod 198	. . . 4 ⊢ (((𝑊 ∈ LVec ∧ 𝐹 ∈ (LIndS‘𝑊) ∧ 𝑋 ∈ ((Base‘𝑊) ∖ ((LSpan‘𝑊)‘𝐹))) ∧ (𝑥 ∈ 𝐹 ∧ 𝑘 ∈ ((Base‘(Scalar‘𝑊)) ∖ {(0_g‘(Scalar‘𝑊))}))) → ¬ (𝑘( ·_𝑠 ‘𝑊)𝑥) ∈ ((LSpan‘𝑊)‘((𝐹 ∪ {𝑋}) ∖ {𝑥})))
113	112	ralrimivva 3201	. . 3 ⊢ ((𝑊 ∈ LVec ∧ 𝐹 ∈ (LIndS‘𝑊) ∧ 𝑋 ∈ ((Base‘𝑊) ∖ ((LSpan‘𝑊)‘𝐹))) → ∀𝑥 ∈ 𝐹 ∀𝑘 ∈ ((Base‘(Scalar‘𝑊)) ∖ {(0_g‘(Scalar‘𝑊))}) ¬ (𝑘( ·_𝑠 ‘𝑊)𝑥) ∈ ((LSpan‘𝑊)‘((𝐹 ∪ {𝑋}) ∖ {𝑥})))
114	10	adantr 480	. . . . . 6 ⊢ (((𝑊 ∈ LVec ∧ 𝐹 ∈ (LIndS‘𝑊) ∧ 𝑋 ∈ ((Base‘𝑊) ∖ ((LSpan‘𝑊)‘𝐹))) ∧ 𝑘 ∈ ((Base‘(Scalar‘𝑊)) ∖ {(0_g‘(Scalar‘𝑊))})) → ¬ 𝑋 ∈ ((LSpan‘𝑊)‘𝐹))
115		difsn 4797	. . . . . . . . . . 11 ⊢ (¬ 𝑋 ∈ 𝐹 → (𝐹 ∖ {𝑋}) = 𝐹)
116	54, 115	syl 17	. . . . . . . . . 10 ⊢ ((𝑊 ∈ LVec ∧ 𝐹 ∈ (LIndS‘𝑊) ∧ 𝑋 ∈ ((Base‘𝑊) ∖ ((LSpan‘𝑊)‘𝐹))) → (𝐹 ∖ {𝑋}) = 𝐹)
117	116	fveq2d 6909	. . . . . . . . 9 ⊢ ((𝑊 ∈ LVec ∧ 𝐹 ∈ (LIndS‘𝑊) ∧ 𝑋 ∈ ((Base‘𝑊) ∖ ((LSpan‘𝑊)‘𝐹))) → ((LSpan‘𝑊)‘(𝐹 ∖ {𝑋})) = ((LSpan‘𝑊)‘𝐹))
118	117	eleq2d 2826	. . . . . . . 8 ⊢ ((𝑊 ∈ LVec ∧ 𝐹 ∈ (LIndS‘𝑊) ∧ 𝑋 ∈ ((Base‘𝑊) ∖ ((LSpan‘𝑊)‘𝐹))) → ((𝑘( ·_𝑠 ‘𝑊)𝑋) ∈ ((LSpan‘𝑊)‘(𝐹 ∖ {𝑋})) ↔ (𝑘( ·_𝑠 ‘𝑊)𝑋) ∈ ((LSpan‘𝑊)‘𝐹)))
119	118	adantr 480	. . . . . . 7 ⊢ (((𝑊 ∈ LVec ∧ 𝐹 ∈ (LIndS‘𝑊) ∧ 𝑋 ∈ ((Base‘𝑊) ∖ ((LSpan‘𝑊)‘𝐹))) ∧ 𝑘 ∈ ((Base‘(Scalar‘𝑊)) ∖ {(0_g‘(Scalar‘𝑊))})) → ((𝑘( ·_𝑠 ‘𝑊)𝑋) ∈ ((LSpan‘𝑊)‘(𝐹 ∖ {𝑋})) ↔ (𝑘( ·_𝑠 ‘𝑊)𝑋) ∈ ((LSpan‘𝑊)‘𝐹)))
120	1, 21, 75, 25, 24, 31	lspsnvs 21117	. . . . . . . . . . . . . 14 ⊢ ((𝑊 ∈ LVec ∧ (𝑘 ∈ (Base‘(Scalar‘𝑊)) ∧ 𝑘 ≠ (0_g‘(Scalar‘𝑊))) ∧ 𝑋 ∈ (Base‘𝑊)) → ((LSpan‘𝑊)‘{(𝑘( ·_𝑠 ‘𝑊)𝑋)}) = ((LSpan‘𝑊)‘{𝑋}))
121	120	3expa 1118	. . . . . . . . . . . . 13 ⊢ (((𝑊 ∈ LVec ∧ (𝑘 ∈ (Base‘(Scalar‘𝑊)) ∧ 𝑘 ≠ (0_g‘(Scalar‘𝑊)))) ∧ 𝑋 ∈ (Base‘𝑊)) → ((LSpan‘𝑊)‘{(𝑘( ·_𝑠 ‘𝑊)𝑋)}) = ((LSpan‘𝑊)‘{𝑋}))
122	121	an32s 652	. . . . . . . . . . . 12 ⊢ (((𝑊 ∈ LVec ∧ 𝑋 ∈ (Base‘𝑊)) ∧ (𝑘 ∈ (Base‘(Scalar‘𝑊)) ∧ 𝑘 ≠ (0_g‘(Scalar‘𝑊)))) → ((LSpan‘𝑊)‘{(𝑘( ·_𝑠 ‘𝑊)𝑋)}) = ((LSpan‘𝑊)‘{𝑋}))
123	71, 122	sylan2b 594	. . . . . . . . . . 11 ⊢ (((𝑊 ∈ LVec ∧ 𝑋 ∈ (Base‘𝑊)) ∧ 𝑘 ∈ ((Base‘(Scalar‘𝑊)) ∖ {(0_g‘(Scalar‘𝑊))})) → ((LSpan‘𝑊)‘{(𝑘( ·_𝑠 ‘𝑊)𝑋)}) = ((LSpan‘𝑊)‘{𝑋}))
124	123	sseq1d 4014	. . . . . . . . . 10 ⊢ (((𝑊 ∈ LVec ∧ 𝑋 ∈ (Base‘𝑊)) ∧ 𝑘 ∈ ((Base‘(Scalar‘𝑊)) ∖ {(0_g‘(Scalar‘𝑊))})) → (((LSpan‘𝑊)‘{(𝑘( ·_𝑠 ‘𝑊)𝑋)}) ⊆ ((LSpan‘𝑊)‘𝐹) ↔ ((LSpan‘𝑊)‘{𝑋}) ⊆ ((LSpan‘𝑊)‘𝐹)))
125	124	3adantl2 1167	. . . . . . . . 9 ⊢ (((𝑊 ∈ LVec ∧ 𝐹 ∈ (LIndS‘𝑊) ∧ 𝑋 ∈ (Base‘𝑊)) ∧ 𝑘 ∈ ((Base‘(Scalar‘𝑊)) ∖ {(0_g‘(Scalar‘𝑊))})) → (((LSpan‘𝑊)‘{(𝑘( ·_𝑠 ‘𝑊)𝑋)}) ⊆ ((LSpan‘𝑊)‘𝐹) ↔ ((LSpan‘𝑊)‘{𝑋}) ⊆ ((LSpan‘𝑊)‘𝐹)))
126	82	adantr 480	. . . . . . . . . . 11 ⊢ (((𝑊 ∈ LVec ∧ 𝐹 ∈ (LIndS‘𝑊) ∧ 𝑋 ∈ (Base‘𝑊)) ∧ 𝑘 ∈ (Base‘(Scalar‘𝑊))) → 𝑊 ∈ LMod)
127	1, 37, 31	lspcl 20975	. . . . . . . . . . . . . 14 ⊢ ((𝑊 ∈ LMod ∧ 𝐹 ⊆ (Base‘𝑊)) → ((LSpan‘𝑊)‘𝐹) ∈ (LSubSp‘𝑊))
128	19, 2, 127	syl2an 596	. . . . . . . . . . . . 13 ⊢ ((𝑊 ∈ LVec ∧ 𝐹 ∈ (LIndS‘𝑊)) → ((LSpan‘𝑊)‘𝐹) ∈ (LSubSp‘𝑊))
129	128	3adant3 1132	. . . . . . . . . . . 12 ⊢ ((𝑊 ∈ LVec ∧ 𝐹 ∈ (LIndS‘𝑊) ∧ 𝑋 ∈ (Base‘𝑊)) → ((LSpan‘𝑊)‘𝐹) ∈ (LSubSp‘𝑊))
130	129	adantr 480	. . . . . . . . . . 11 ⊢ (((𝑊 ∈ LVec ∧ 𝐹 ∈ (LIndS‘𝑊) ∧ 𝑋 ∈ (Base‘𝑊)) ∧ 𝑘 ∈ (Base‘(Scalar‘𝑊))) → ((LSpan‘𝑊)‘𝐹) ∈ (LSubSp‘𝑊))
131	1, 21, 75, 25	lmodvscl 20877	. . . . . . . . . . . . . . 15 ⊢ ((𝑊 ∈ LMod ∧ 𝑘 ∈ (Base‘(Scalar‘𝑊)) ∧ 𝑋 ∈ (Base‘𝑊)) → (𝑘( ·_𝑠 ‘𝑊)𝑋) ∈ (Base‘𝑊))
132	131	3expa 1118	. . . . . . . . . . . . . 14 ⊢ (((𝑊 ∈ LMod ∧ 𝑘 ∈ (Base‘(Scalar‘𝑊))) ∧ 𝑋 ∈ (Base‘𝑊)) → (𝑘( ·_𝑠 ‘𝑊)𝑋) ∈ (Base‘𝑊))
133	132	an32s 652	. . . . . . . . . . . . 13 ⊢ (((𝑊 ∈ LMod ∧ 𝑋 ∈ (Base‘𝑊)) ∧ 𝑘 ∈ (Base‘(Scalar‘𝑊))) → (𝑘( ·_𝑠 ‘𝑊)𝑋) ∈ (Base‘𝑊))
134	19, 133	sylanl1 680	. . . . . . . . . . . 12 ⊢ (((𝑊 ∈ LVec ∧ 𝑋 ∈ (Base‘𝑊)) ∧ 𝑘 ∈ (Base‘(Scalar‘𝑊))) → (𝑘( ·_𝑠 ‘𝑊)𝑋) ∈ (Base‘𝑊))
135	134	3adantl2 1167	. . . . . . . . . . 11 ⊢ (((𝑊 ∈ LVec ∧ 𝐹 ∈ (LIndS‘𝑊) ∧ 𝑋 ∈ (Base‘𝑊)) ∧ 𝑘 ∈ (Base‘(Scalar‘𝑊))) → (𝑘( ·_𝑠 ‘𝑊)𝑋) ∈ (Base‘𝑊))
136	1, 37, 31, 126, 130, 135	ellspsn5b 20994	. . . . . . . . . 10 ⊢ (((𝑊 ∈ LVec ∧ 𝐹 ∈ (LIndS‘𝑊) ∧ 𝑋 ∈ (Base‘𝑊)) ∧ 𝑘 ∈ (Base‘(Scalar‘𝑊))) → ((𝑘( ·_𝑠 ‘𝑊)𝑋) ∈ ((LSpan‘𝑊)‘𝐹) ↔ ((LSpan‘𝑊)‘{(𝑘( ·_𝑠 ‘𝑊)𝑋)}) ⊆ ((LSpan‘𝑊)‘𝐹)))
137	81, 136	sylan2 593	. . . . . . . . 9 ⊢ (((𝑊 ∈ LVec ∧ 𝐹 ∈ (LIndS‘𝑊) ∧ 𝑋 ∈ (Base‘𝑊)) ∧ 𝑘 ∈ ((Base‘(Scalar‘𝑊)) ∖ {(0_g‘(Scalar‘𝑊))})) → ((𝑘( ·_𝑠 ‘𝑊)𝑋) ∈ ((LSpan‘𝑊)‘𝐹) ↔ ((LSpan‘𝑊)‘{(𝑘( ·_𝑠 ‘𝑊)𝑋)}) ⊆ ((LSpan‘𝑊)‘𝐹)))
138		simp3 1138	. . . . . . . . . . 11 ⊢ ((𝑊 ∈ LVec ∧ 𝐹 ∈ (LIndS‘𝑊) ∧ 𝑋 ∈ (Base‘𝑊)) → 𝑋 ∈ (Base‘𝑊))
139	1, 37, 31, 82, 129, 138	ellspsn5b 20994	. . . . . . . . . 10 ⊢ ((𝑊 ∈ LVec ∧ 𝐹 ∈ (LIndS‘𝑊) ∧ 𝑋 ∈ (Base‘𝑊)) → (𝑋 ∈ ((LSpan‘𝑊)‘𝐹) ↔ ((LSpan‘𝑊)‘{𝑋}) ⊆ ((LSpan‘𝑊)‘𝐹)))
140	139	adantr 480	. . . . . . . . 9 ⊢ (((𝑊 ∈ LVec ∧ 𝐹 ∈ (LIndS‘𝑊) ∧ 𝑋 ∈ (Base‘𝑊)) ∧ 𝑘 ∈ ((Base‘(Scalar‘𝑊)) ∖ {(0_g‘(Scalar‘𝑊))})) → (𝑋 ∈ ((LSpan‘𝑊)‘𝐹) ↔ ((LSpan‘𝑊)‘{𝑋}) ⊆ ((LSpan‘𝑊)‘𝐹)))
141	125, 137, 140	3bitr4d 311	. . . . . . . 8 ⊢ (((𝑊 ∈ LVec ∧ 𝐹 ∈ (LIndS‘𝑊) ∧ 𝑋 ∈ (Base‘𝑊)) ∧ 𝑘 ∈ ((Base‘(Scalar‘𝑊)) ∖ {(0_g‘(Scalar‘𝑊))})) → ((𝑘( ·_𝑠 ‘𝑊)𝑋) ∈ ((LSpan‘𝑊)‘𝐹) ↔ 𝑋 ∈ ((LSpan‘𝑊)‘𝐹)))
142	3, 141	syl3anl3 1415	. . . . . . 7 ⊢ (((𝑊 ∈ LVec ∧ 𝐹 ∈ (LIndS‘𝑊) ∧ 𝑋 ∈ ((Base‘𝑊) ∖ ((LSpan‘𝑊)‘𝐹))) ∧ 𝑘 ∈ ((Base‘(Scalar‘𝑊)) ∖ {(0_g‘(Scalar‘𝑊))})) → ((𝑘( ·_𝑠 ‘𝑊)𝑋) ∈ ((LSpan‘𝑊)‘𝐹) ↔ 𝑋 ∈ ((LSpan‘𝑊)‘𝐹)))
143	119, 142	bitrd 279	. . . . . 6 ⊢ (((𝑊 ∈ LVec ∧ 𝐹 ∈ (LIndS‘𝑊) ∧ 𝑋 ∈ ((Base‘𝑊) ∖ ((LSpan‘𝑊)‘𝐹))) ∧ 𝑘 ∈ ((Base‘(Scalar‘𝑊)) ∖ {(0_g‘(Scalar‘𝑊))})) → ((𝑘( ·_𝑠 ‘𝑊)𝑋) ∈ ((LSpan‘𝑊)‘(𝐹 ∖ {𝑋})) ↔ 𝑋 ∈ ((LSpan‘𝑊)‘𝐹)))
144	114, 143	mtbird 325	. . . . 5 ⊢ (((𝑊 ∈ LVec ∧ 𝐹 ∈ (LIndS‘𝑊) ∧ 𝑋 ∈ ((Base‘𝑊) ∖ ((LSpan‘𝑊)‘𝐹))) ∧ 𝑘 ∈ ((Base‘(Scalar‘𝑊)) ∖ {(0_g‘(Scalar‘𝑊))})) → ¬ (𝑘( ·_𝑠 ‘𝑊)𝑋) ∈ ((LSpan‘𝑊)‘(𝐹 ∖ {𝑋})))
145	144	ralrimiva 3145	. . . 4 ⊢ ((𝑊 ∈ LVec ∧ 𝐹 ∈ (LIndS‘𝑊) ∧ 𝑋 ∈ ((Base‘𝑊) ∖ ((LSpan‘𝑊)‘𝐹))) → ∀𝑘 ∈ ((Base‘(Scalar‘𝑊)) ∖ {(0_g‘(Scalar‘𝑊))}) ¬ (𝑘( ·_𝑠 ‘𝑊)𝑋) ∈ ((LSpan‘𝑊)‘(𝐹 ∖ {𝑋})))
146		oveq2 7440	. . . . . . . . 9 ⊢ (𝑥 = 𝑋 → (𝑘( ·_𝑠 ‘𝑊)𝑥) = (𝑘( ·_𝑠 ‘𝑊)𝑋))
147		sneq 4635	. . . . . . . . . . . 12 ⊢ (𝑥 = 𝑋 → {𝑥} = {𝑋})
148	147	difeq2d 4125	. . . . . . . . . . 11 ⊢ (𝑥 = 𝑋 → ((𝐹 ∪ {𝑋}) ∖ {𝑥}) = ((𝐹 ∪ {𝑋}) ∖ {𝑋}))
149		difun2 4480	. . . . . . . . . . 11 ⊢ ((𝐹 ∪ {𝑋}) ∖ {𝑋}) = (𝐹 ∖ {𝑋})
150	148, 149	eqtrdi 2792	. . . . . . . . . 10 ⊢ (𝑥 = 𝑋 → ((𝐹 ∪ {𝑋}) ∖ {𝑥}) = (𝐹 ∖ {𝑋}))
151	150	fveq2d 6909	. . . . . . . . 9 ⊢ (𝑥 = 𝑋 → ((LSpan‘𝑊)‘((𝐹 ∪ {𝑋}) ∖ {𝑥})) = ((LSpan‘𝑊)‘(𝐹 ∖ {𝑋})))
152	146, 151	eleq12d 2834	. . . . . . . 8 ⊢ (𝑥 = 𝑋 → ((𝑘( ·_𝑠 ‘𝑊)𝑥) ∈ ((LSpan‘𝑊)‘((𝐹 ∪ {𝑋}) ∖ {𝑥})) ↔ (𝑘( ·_𝑠 ‘𝑊)𝑋) ∈ ((LSpan‘𝑊)‘(𝐹 ∖ {𝑋}))))
153	152	notbid 318	. . . . . . 7 ⊢ (𝑥 = 𝑋 → (¬ (𝑘( ·_𝑠 ‘𝑊)𝑥) ∈ ((LSpan‘𝑊)‘((𝐹 ∪ {𝑋}) ∖ {𝑥})) ↔ ¬ (𝑘( ·_𝑠 ‘𝑊)𝑋) ∈ ((LSpan‘𝑊)‘(𝐹 ∖ {𝑋}))))
154	153	ralbidv 3177	. . . . . 6 ⊢ (𝑥 = 𝑋 → (∀𝑘 ∈ ((Base‘(Scalar‘𝑊)) ∖ {(0_g‘(Scalar‘𝑊))}) ¬ (𝑘( ·_𝑠 ‘𝑊)𝑥) ∈ ((LSpan‘𝑊)‘((𝐹 ∪ {𝑋}) ∖ {𝑥})) ↔ ∀𝑘 ∈ ((Base‘(Scalar‘𝑊)) ∖ {(0_g‘(Scalar‘𝑊))}) ¬ (𝑘( ·_𝑠 ‘𝑊)𝑋) ∈ ((LSpan‘𝑊)‘(𝐹 ∖ {𝑋}))))
155	154	ralsng 4674	. . . . 5 ⊢ (𝑋 ∈ ((Base‘𝑊) ∖ ((LSpan‘𝑊)‘𝐹)) → (∀𝑥 ∈ {𝑋}∀𝑘 ∈ ((Base‘(Scalar‘𝑊)) ∖ {(0_g‘(Scalar‘𝑊))}) ¬ (𝑘( ·_𝑠 ‘𝑊)𝑥) ∈ ((LSpan‘𝑊)‘((𝐹 ∪ {𝑋}) ∖ {𝑥})) ↔ ∀𝑘 ∈ ((Base‘(Scalar‘𝑊)) ∖ {(0_g‘(Scalar‘𝑊))}) ¬ (𝑘( ·_𝑠 ‘𝑊)𝑋) ∈ ((LSpan‘𝑊)‘(𝐹 ∖ {𝑋}))))
156	155	3ad2ant3 1135	. . . 4 ⊢ ((𝑊 ∈ LVec ∧ 𝐹 ∈ (LIndS‘𝑊) ∧ 𝑋 ∈ ((Base‘𝑊) ∖ ((LSpan‘𝑊)‘𝐹))) → (∀𝑥 ∈ {𝑋}∀𝑘 ∈ ((Base‘(Scalar‘𝑊)) ∖ {(0_g‘(Scalar‘𝑊))}) ¬ (𝑘( ·_𝑠 ‘𝑊)𝑥) ∈ ((LSpan‘𝑊)‘((𝐹 ∪ {𝑋}) ∖ {𝑥})) ↔ ∀𝑘 ∈ ((Base‘(Scalar‘𝑊)) ∖ {(0_g‘(Scalar‘𝑊))}) ¬ (𝑘( ·_𝑠 ‘𝑊)𝑋) ∈ ((LSpan‘𝑊)‘(𝐹 ∖ {𝑋}))))
157	145, 156	mpbird 257	. . 3 ⊢ ((𝑊 ∈ LVec ∧ 𝐹 ∈ (LIndS‘𝑊) ∧ 𝑋 ∈ ((Base‘𝑊) ∖ ((LSpan‘𝑊)‘𝐹))) → ∀𝑥 ∈ {𝑋}∀𝑘 ∈ ((Base‘(Scalar‘𝑊)) ∖ {(0_g‘(Scalar‘𝑊))}) ¬ (𝑘( ·_𝑠 ‘𝑊)𝑥) ∈ ((LSpan‘𝑊)‘((𝐹 ∪ {𝑋}) ∖ {𝑥})))
158		ralunb 4196	. . 3 ⊢ (∀𝑥 ∈ (𝐹 ∪ {𝑋})∀𝑘 ∈ ((Base‘(Scalar‘𝑊)) ∖ {(0_g‘(Scalar‘𝑊))}) ¬ (𝑘( ·_𝑠 ‘𝑊)𝑥) ∈ ((LSpan‘𝑊)‘((𝐹 ∪ {𝑋}) ∖ {𝑥})) ↔ (∀𝑥 ∈ 𝐹 ∀𝑘 ∈ ((Base‘(Scalar‘𝑊)) ∖ {(0_g‘(Scalar‘𝑊))}) ¬ (𝑘( ·_𝑠 ‘𝑊)𝑥) ∈ ((LSpan‘𝑊)‘((𝐹 ∪ {𝑋}) ∖ {𝑥})) ∧ ∀𝑥 ∈ {𝑋}∀𝑘 ∈ ((Base‘(Scalar‘𝑊)) ∖ {(0_g‘(Scalar‘𝑊))}) ¬ (𝑘( ·_𝑠 ‘𝑊)𝑥) ∈ ((LSpan‘𝑊)‘((𝐹 ∪ {𝑋}) ∖ {𝑥}))))
159	113, 157, 158	sylanbrc 583	. 2 ⊢ ((𝑊 ∈ LVec ∧ 𝐹 ∈ (LIndS‘𝑊) ∧ 𝑋 ∈ ((Base‘𝑊) ∖ ((LSpan‘𝑊)‘𝐹))) → ∀𝑥 ∈ (𝐹 ∪ {𝑋})∀𝑘 ∈ ((Base‘(Scalar‘𝑊)) ∖ {(0_g‘(Scalar‘𝑊))}) ¬ (𝑘( ·_𝑠 ‘𝑊)𝑥) ∈ ((LSpan‘𝑊)‘((𝐹 ∪ {𝑋}) ∖ {𝑥})))
160	1, 75, 31, 21, 25, 24	islinds2 21834	. . 3 ⊢ (𝑊 ∈ LVec → ((𝐹 ∪ {𝑋}) ∈ (LIndS‘𝑊) ↔ ((𝐹 ∪ {𝑋}) ⊆ (Base‘𝑊) ∧ ∀𝑥 ∈ (𝐹 ∪ {𝑋})∀𝑘 ∈ ((Base‘(Scalar‘𝑊)) ∖ {(0_g‘(Scalar‘𝑊))}) ¬ (𝑘( ·_𝑠 ‘𝑊)𝑥) ∈ ((LSpan‘𝑊)‘((𝐹 ∪ {𝑋}) ∖ {𝑥})))))
161	160	3ad2ant1 1133	. 2 ⊢ ((𝑊 ∈ LVec ∧ 𝐹 ∈ (LIndS‘𝑊) ∧ 𝑋 ∈ ((Base‘𝑊) ∖ ((LSpan‘𝑊)‘𝐹))) → ((𝐹 ∪ {𝑋}) ∈ (LIndS‘𝑊) ↔ ((𝐹 ∪ {𝑋}) ⊆ (Base‘𝑊) ∧ ∀𝑥 ∈ (𝐹 ∪ {𝑋})∀𝑘 ∈ ((Base‘(Scalar‘𝑊)) ∖ {(0_g‘(Scalar‘𝑊))}) ¬ (𝑘( ·_𝑠 ‘𝑊)𝑥) ∈ ((LSpan‘𝑊)‘((𝐹 ∪ {𝑋}) ∖ {𝑥})))))
162	8, 159, 161	mpbir2and 713	1 ⊢ ((𝑊 ∈ LVec ∧ 𝐹 ∈ (LIndS‘𝑊) ∧ 𝑋 ∈ ((Base‘𝑊) ∖ ((LSpan‘𝑊)‘𝐹))) → (𝐹 ∪ {𝑋}) ∈ (LIndS‘𝑊))

Colors of variables: wff setvar class

Syntax hints: ¬ wn 3 → wi 4 ↔ wb 206 ∧ wa 395 ∧ w3a 1086 = wceq 1539 ∈ wcel 2107 ≠ wne 2939 ∀wral 3060 ∖ cdif 3947 ∪ cun 3948 ∩ cin 3949 ⊆ wss 3950 ∅c0 4332 {csn 4625 ‘cfv 6560 (class class class)co 7432 Basecbs 17248 Scalarcsca 17301 ·_𝑠 cvsca 17302 0_gc0g 17485 Ringcrg 20231 NzRingcnzr 20513 LModclmod 20859 LSubSpclss 20930 LSpanclspn 20970 LVecclvec 21102 LIndSclinds 21826

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1794 ax-4 1808 ax-5 1909 ax-6 1966 ax-7 2006 ax-8 2109 ax-9 2117 ax-10 2140 ax-11 2156 ax-12 2176 ax-ext 2707 ax-rep 5278 ax-sep 5295 ax-nul 5305 ax-pow 5364 ax-pr 5431 ax-un 7756 ax-cnex 11212 ax-resscn 11213 ax-1cn 11214 ax-icn 11215 ax-addcl 11216 ax-addrcl 11217 ax-mulcl 11218 ax-mulrcl 11219 ax-mulcom 11220 ax-addass 11221 ax-mulass 11222 ax-distr 11223 ax-i2m1 11224 ax-1ne0 11225 ax-1rid 11226 ax-rnegex 11227 ax-rrecex 11228 ax-cnre 11229 ax-pre-lttri 11230 ax-pre-lttrn 11231 ax-pre-ltadd 11232 ax-pre-mulgt0 11233

This theorem depends on definitions: df-bi 207 df-an 396 df-or 848 df-3or 1087 df-3an 1088 df-tru 1542 df-fal 1552 df-ex 1779 df-nf 1783 df-sb 2064 df-mo 2539 df-eu 2568 df-clab 2714 df-cleq 2728 df-clel 2815 df-nfc 2891 df-ne 2940 df-nel 3046 df-ral 3061 df-rex 3070 df-rmo 3379 df-reu 3380 df-rab 3436 df-v 3481 df-sbc 3788 df-csb 3899 df-dif 3953 df-un 3955 df-in 3957 df-ss 3967 df-pss 3970 df-nul 4333 df-if 4525 df-pw 4601 df-sn 4626 df-pr 4628 df-op 4632 df-uni 4907 df-int 4946 df-iun 4992 df-br 5143 df-opab 5205 df-mpt 5225 df-tr 5259 df-id 5577 df-eprel 5583 df-po 5591 df-so 5592 df-fr 5636 df-we 5638 df-xp 5690 df-rel 5691 df-cnv 5692 df-co 5693 df-dm 5694 df-rn 5695 df-res 5696 df-ima 5697 df-pred 6320 df-ord 6386 df-on 6387 df-lim 6388 df-suc 6389 df-iota 6513 df-fun 6562 df-fn 6563 df-f 6564 df-f1 6565 df-fo 6566 df-f1o 6567 df-fv 6568 df-riota 7389 df-ov 7435 df-oprab 7436 df-mpo 7437 df-om 7889 df-1st 8015 df-2nd 8016 df-tpos 8252 df-frecs 8307 df-wrecs 8338 df-recs 8412 df-rdg 8451 df-er 8746 df-en 8987 df-dom 8988 df-sdom 8989 df-pnf 11298 df-mnf 11299 df-xr 11300 df-ltxr 11301 df-le 11302 df-sub 11495 df-neg 11496 df-nn 12268 df-2 12330 df-3 12331 df-sets 17202 df-slot 17220 df-ndx 17232 df-base 17249 df-ress 17276 df-plusg 17311 df-mulr 17312 df-0g 17487 df-mgm 18654 df-sgrp 18733 df-mnd 18749 df-grp 18955 df-minusg 18956 df-sbg 18957 df-cmn 19801 df-abl 19802 df-mgp 20139 df-rng 20151 df-ur 20180 df-ring 20233 df-oppr 20335 df-dvdsr 20358 df-unit 20359 df-invr 20389 df-nzr 20514 df-drng 20732 df-lmod 20861 df-lss 20931 df-lsp 20971 df-lvec 21103 df-lindf 21827 df-linds 21828

This theorem is referenced by: (None)

W3C validator