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 37934

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 21790	. . . 4 ⊢ (𝐹 ∈ (LIndS‘𝑊) → 𝐹 ⊆ (Base‘𝑊))
3		eldifi 4071	. . . . 5 ⊢ (𝑋 ∈ ((Base‘𝑊) ∖ ((LSpan‘𝑊)‘𝐹)) → 𝑋 ∈ (Base‘𝑊))
4	3	snssd 4730	. . . 4 ⊢ (𝑋 ∈ ((Base‘𝑊) ∖ ((LSpan‘𝑊)‘𝐹)) → {𝑋} ⊆ (Base‘𝑊))
5		unss 4130	. . . . 5 ⊢ ((𝐹 ⊆ (Base‘𝑊) ∧ {𝑋} ⊆ (Base‘𝑊)) ↔ (𝐹 ∪ {𝑋}) ⊆ (Base‘𝑊))
6	5	biimpi 216	. . . 4 ⊢ ((𝐹 ⊆ (Base‘𝑊) ∧ {𝑋} ⊆ (Base‘𝑊)) → (𝐹 ∪ {𝑋}) ⊆ (Base‘𝑊))
7	2, 4, 6	syl2an 597	. . 3 ⊢ ((𝐹 ∈ (LIndS‘𝑊) ∧ 𝑋 ∈ ((Base‘𝑊) ∖ ((LSpan‘𝑊)‘𝐹))) → (𝐹 ∪ {𝑋}) ⊆ (Base‘𝑊))
8	7	3adant1 1131	. 2 ⊢ ((𝑊 ∈ LVec ∧ 𝐹 ∈ (LIndS‘𝑊) ∧ 𝑋 ∈ ((Base‘𝑊) ∖ ((LSpan‘𝑊)‘𝐹))) → (𝐹 ∪ {𝑋}) ⊆ (Base‘𝑊))
9		eldifn 4072	. . . . . . 7 ⊢ (𝑋 ∈ ((Base‘𝑊) ∖ ((LSpan‘𝑊)‘𝐹)) → ¬ 𝑋 ∈ ((LSpan‘𝑊)‘𝐹))
10	9	3ad2ant3 1136	. . . . . 6 ⊢ ((𝑊 ∈ LVec ∧ 𝐹 ∈ (LIndS‘𝑊) ∧ 𝑋 ∈ ((Base‘𝑊) ∖ ((LSpan‘𝑊)‘𝐹))) → ¬ 𝑋 ∈ ((LSpan‘𝑊)‘𝐹))
11	10	adantr 480	. . . . 5 ⊢ (((𝑊 ∈ LVec ∧ 𝐹 ∈ (LIndS‘𝑊) ∧ 𝑋 ∈ ((Base‘𝑊) ∖ ((LSpan‘𝑊)‘𝐹))) ∧ (𝑥 ∈ 𝐹 ∧ 𝑘 ∈ ((Base‘(Scalar‘𝑊)) ∖ {(0_g‘(Scalar‘𝑊))}))) → ¬ 𝑋 ∈ ((LSpan‘𝑊)‘𝐹))
12		simpll1 1214	. . . . . . . 8 ⊢ ((((𝑊 ∈ LVec ∧ 𝐹 ∈ (LIndS‘𝑊) ∧ 𝑋 ∈ ((Base‘𝑊) ∖ ((LSpan‘𝑊)‘𝐹))) ∧ (𝑥 ∈ 𝐹 ∧ 𝑘 ∈ ((Base‘(Scalar‘𝑊)) ∖ {(0_g‘(Scalar‘𝑊))}))) ∧ 𝑥 ∈ ((LSpan‘𝑊)‘((𝐹 ∖ {𝑥}) ∪ {𝑋}))) → 𝑊 ∈ LVec)
13	2	ssdifssd 4087	. . . . . . . . . 10 ⊢ (𝐹 ∈ (LIndS‘𝑊) → (𝐹 ∖ {𝑥}) ⊆ (Base‘𝑊))
14	13	3ad2ant2 1135	. . . . . . . . 9 ⊢ ((𝑊 ∈ LVec ∧ 𝐹 ∈ (LIndS‘𝑊) ∧ 𝑋 ∈ ((Base‘𝑊) ∖ ((LSpan‘𝑊)‘𝐹))) → (𝐹 ∖ {𝑥}) ⊆ (Base‘𝑊))
15	14	ad2antrr 727	. . . . . . . 8 ⊢ ((((𝑊 ∈ LVec ∧ 𝐹 ∈ (LIndS‘𝑊) ∧ 𝑋 ∈ ((Base‘𝑊) ∖ ((LSpan‘𝑊)‘𝐹))) ∧ (𝑥 ∈ 𝐹 ∧ 𝑘 ∈ ((Base‘(Scalar‘𝑊)) ∖ {(0_g‘(Scalar‘𝑊))}))) ∧ 𝑥 ∈ ((LSpan‘𝑊)‘((𝐹 ∖ {𝑥}) ∪ {𝑋}))) → (𝐹 ∖ {𝑥}) ⊆ (Base‘𝑊))
16	3	3ad2ant3 1136	. . . . . . . . 9 ⊢ ((𝑊 ∈ LVec ∧ 𝐹 ∈ (LIndS‘𝑊) ∧ 𝑋 ∈ ((Base‘𝑊) ∖ ((LSpan‘𝑊)‘𝐹))) → 𝑋 ∈ (Base‘𝑊))
17	16	ad2antrr 727	. . . . . . . 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 21101	. . . . . . . . . . . . 13 ⊢ (𝑊 ∈ LVec → 𝑊 ∈ LMod)
20	19	ad2antrr 727	. . . . . . . . . . . 12 ⊢ (((𝑊 ∈ LVec ∧ 𝐹 ∈ (LIndS‘𝑊)) ∧ (𝑥 ∈ 𝐹 ∧ 𝑘 ∈ ((Base‘(Scalar‘𝑊)) ∖ {(0_g‘(Scalar‘𝑊))}))) → 𝑊 ∈ LMod)
21		eqid 2736	. . . . . . . . . . . . . . . 16 ⊢ (Scalar‘𝑊) = (Scalar‘𝑊)
22	21	lmodring 20863	. . . . . . . . . . . . . . 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 20500	. . . . . . . . . . . . . 14 ⊢ (((Scalar‘𝑊) ∈ Ring ∧ 𝑘 ∈ ((Base‘(Scalar‘𝑊)) ∖ {(0_g‘(Scalar‘𝑊))})) → (Scalar‘𝑊) ∈ NzRing)
27	23, 26	sylan 581	. . . . . . . . . . . . 13 ⊢ ((𝑊 ∈ LVec ∧ 𝑘 ∈ ((Base‘(Scalar‘𝑊)) ∖ {(0_g‘(Scalar‘𝑊))})) → (Scalar‘𝑊) ∈ NzRing)
28	27	ad2ant2rl 750	. . . . . . . . . . . 12 ⊢ (((𝑊 ∈ LVec ∧ 𝐹 ∈ (LIndS‘𝑊)) ∧ (𝑥 ∈ 𝐹 ∧ 𝑘 ∈ ((Base‘(Scalar‘𝑊)) ∖ {(0_g‘(Scalar‘𝑊))}))) → (Scalar‘𝑊) ∈ NzRing)
29		simplr 769	. . . . . . . . . . . 12 ⊢ (((𝑊 ∈ LVec ∧ 𝐹 ∈ (LIndS‘𝑊)) ∧ (𝑥 ∈ 𝐹 ∧ 𝑘 ∈ ((Base‘(Scalar‘𝑊)) ∖ {(0_g‘(Scalar‘𝑊))}))) → 𝐹 ∈ (LIndS‘𝑊))
30		simprl 771	. . . . . . . . . . . 12 ⊢ (((𝑊 ∈ LVec ∧ 𝐹 ∈ (LIndS‘𝑊)) ∧ (𝑥 ∈ 𝐹 ∧ 𝑘 ∈ ((Base‘(Scalar‘𝑊)) ∖ {(0_g‘(Scalar‘𝑊))}))) → 𝑥 ∈ 𝐹)
31		eqid 2736	. . . . . . . . . . . . 13 ⊢ (LSpan‘𝑊) = (LSpan‘𝑊)
32	31, 21	lindsind2 21799	. . . . . . . . . . . 12 ⊢ (((𝑊 ∈ LMod ∧ (Scalar‘𝑊) ∈ NzRing) ∧ 𝐹 ∈ (LIndS‘𝑊) ∧ 𝑥 ∈ 𝐹) → ¬ 𝑥 ∈ ((LSpan‘𝑊)‘(𝐹 ∖ {𝑥})))
33	20, 28, 29, 30, 32	syl211anc 1379	. . . . . . . . . . 11 ⊢ (((𝑊 ∈ LVec ∧ 𝐹 ∈ (LIndS‘𝑊)) ∧ (𝑥 ∈ 𝐹 ∧ 𝑘 ∈ ((Base‘(Scalar‘𝑊)) ∖ {(0_g‘(Scalar‘𝑊))}))) → ¬ 𝑥 ∈ ((LSpan‘𝑊)‘(𝐹 ∖ {𝑥})))
34	33	3adantl3 1170	. . . . . . . . . 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 3900	. . . . . . . 8 ⊢ ((((𝑊 ∈ LVec ∧ 𝐹 ∈ (LIndS‘𝑊) ∧ 𝑋 ∈ ((Base‘𝑊) ∖ ((LSpan‘𝑊)‘𝐹))) ∧ (𝑥 ∈ 𝐹 ∧ 𝑘 ∈ ((Base‘(Scalar‘𝑊)) ∖ {(0_g‘(Scalar‘𝑊))}))) ∧ 𝑥 ∈ ((LSpan‘𝑊)‘((𝐹 ∖ {𝑥}) ∪ {𝑋}))) → 𝑥 ∈ (((LSpan‘𝑊)‘((𝐹 ∖ {𝑥}) ∪ {𝑋})) ∖ ((LSpan‘𝑊)‘(𝐹 ∖ {𝑥}))))
37		eqid 2736	. . . . . . . . 9 ⊢ (LSubSp‘𝑊) = (LSubSp‘𝑊)
38	1, 37, 31	lspsolv 21141	. . . . . . . 8 ⊢ ((𝑊 ∈ LVec ∧ ((𝐹 ∖ {𝑥}) ⊆ (Base‘𝑊) ∧ 𝑋 ∈ (Base‘𝑊) ∧ 𝑥 ∈ (((LSpan‘𝑊)‘((𝐹 ∖ {𝑥}) ∪ {𝑋})) ∖ ((LSpan‘𝑊)‘(𝐹 ∖ {𝑥}))))) → 𝑋 ∈ ((LSpan‘𝑊)‘((𝐹 ∖ {𝑥}) ∪ {𝑥})))
39	12, 15, 17, 36, 38	syl13anc 1375	. . . . . . 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 3899	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑋 ∈ ((Base‘𝑊) ∖ ((LSpan‘𝑊)‘𝐹)) ↔ (𝑋 ∈ (Base‘𝑊) ∧ ¬ 𝑋 ∈ ((LSpan‘𝑊)‘𝐹)))
42		snssi 4729	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝑋 ∈ 𝐹 → {𝑋} ⊆ 𝐹)
43	1, 31	lspss 20979	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((𝑊 ∈ LMod ∧ 𝐹 ⊆ (Base‘𝑊) ∧ {𝑋} ⊆ 𝐹) → ((LSpan‘𝑊)‘{𝑋}) ⊆ ((LSpan‘𝑊)‘𝐹))
44	19, 2, 42, 43	syl3an 1161	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝑊 ∈ LVec ∧ 𝐹 ∈ (LIndS‘𝑊) ∧ 𝑋 ∈ 𝐹) → ((LSpan‘𝑊)‘{𝑋}) ⊆ ((LSpan‘𝑊)‘𝐹))
45	44	ad4ant124 1175	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((((𝑊 ∈ LVec ∧ 𝐹 ∈ (LIndS‘𝑊)) ∧ 𝑋 ∈ (Base‘𝑊)) ∧ 𝑋 ∈ 𝐹) → ((LSpan‘𝑊)‘{𝑋}) ⊆ ((LSpan‘𝑊)‘𝐹))
46	1, 31	lspsnid 20988	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((𝑊 ∈ LMod ∧ 𝑋 ∈ (Base‘𝑊)) → 𝑋 ∈ ((LSpan‘𝑊)‘{𝑋}))
47	19, 46	sylan 581	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝑊 ∈ LVec ∧ 𝑋 ∈ (Base‘𝑊)) → 𝑋 ∈ ((LSpan‘𝑊)‘{𝑋}))
48	47	ad4ant13 752	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((((𝑊 ∈ LVec ∧ 𝐹 ∈ (LIndS‘𝑊)) ∧ 𝑋 ∈ (Base‘𝑊)) ∧ 𝑋 ∈ 𝐹) → 𝑋 ∈ ((LSpan‘𝑊)‘{𝑋}))
49	45, 48	sseldd 3922	. . . . . . . . . . . . . . . . . . . . . 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 1118	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑊 ∈ LVec ∧ 𝐹 ∈ (LIndS‘𝑊) ∧ (𝑋 ∈ (Base‘𝑊) ∧ ¬ 𝑋 ∈ ((LSpan‘𝑊)‘𝐹))) → ¬ 𝑋 ∈ 𝐹)
54	41, 53	syl3an3b 1408	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑊 ∈ LVec ∧ 𝐹 ∈ (LIndS‘𝑊) ∧ 𝑋 ∈ ((Base‘𝑊) ∖ ((LSpan‘𝑊)‘𝐹))) → ¬ 𝑋 ∈ 𝐹)
55		eleq1 2824	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑋 = 𝑥 → (𝑋 ∈ 𝐹 ↔ 𝑥 ∈ 𝐹))
56	55	notbid 318	. . . . . . . . . . . . . . . . 17 ⊢ (𝑋 = 𝑥 → (¬ 𝑋 ∈ 𝐹 ↔ ¬ 𝑥 ∈ 𝐹))
57	54, 56	syl5ibcom 245	. . . . . . . . . . . . . . . 16 ⊢ ((𝑊 ∈ LVec ∧ 𝐹 ∈ (LIndS‘𝑊) ∧ 𝑋 ∈ ((Base‘𝑊) ∖ ((LSpan‘𝑊)‘𝐹))) → (𝑋 = 𝑥 → ¬ 𝑥 ∈ 𝐹))
58	57	necon2ad 2947	. . . . . . . . . . . . . . 15 ⊢ ((𝑊 ∈ LVec ∧ 𝐹 ∈ (LIndS‘𝑊) ∧ 𝑋 ∈ ((Base‘𝑊) ∖ ((LSpan‘𝑊)‘𝐹))) → (𝑥 ∈ 𝐹 → 𝑋 ≠ 𝑥))
59	58	imp 406	. . . . . . . . . . . . . 14 ⊢ (((𝑊 ∈ LVec ∧ 𝐹 ∈ (LIndS‘𝑊) ∧ 𝑋 ∈ ((Base‘𝑊) ∖ ((LSpan‘𝑊)‘𝐹))) ∧ 𝑥 ∈ 𝐹) → 𝑋 ≠ 𝑥)
60		disjsn2 4656	. . . . . . . . . . . . . 14 ⊢ (𝑋 ≠ 𝑥 → ({𝑋} ∩ {𝑥}) = ∅)
61	59, 60	syl 17	. . . . . . . . . . . . 13 ⊢ (((𝑊 ∈ LVec ∧ 𝐹 ∈ (LIndS‘𝑊) ∧ 𝑋 ∈ ((Base‘𝑊) ∖ ((LSpan‘𝑊)‘𝐹))) ∧ 𝑥 ∈ 𝐹) → ({𝑋} ∩ {𝑥}) = ∅)
62		disj3 4394	. . . . . . . . . . . . 13 ⊢ (({𝑋} ∩ {𝑥}) = ∅ ↔ {𝑋} = ({𝑋} ∖ {𝑥}))
63	61, 62	sylib 218	. . . . . . . . . . . 12 ⊢ (((𝑊 ∈ LVec ∧ 𝐹 ∈ (LIndS‘𝑊) ∧ 𝑋 ∈ ((Base‘𝑊) ∖ ((LSpan‘𝑊)‘𝐹))) ∧ 𝑥 ∈ 𝐹) → {𝑋} = ({𝑋} ∖ {𝑥}))
64	63	uneq2d 4108	. . . . . . . . . . 11 ⊢ (((𝑊 ∈ LVec ∧ 𝐹 ∈ (LIndS‘𝑊) ∧ 𝑋 ∈ ((Base‘𝑊) ∖ ((LSpan‘𝑊)‘𝐹))) ∧ 𝑥 ∈ 𝐹) → ((𝐹 ∖ {𝑥}) ∪ {𝑋}) = ((𝐹 ∖ {𝑥}) ∪ ({𝑋} ∖ {𝑥})))
65		difundir 4231	. . . . . . . . . . 11 ⊢ ((𝐹 ∪ {𝑋}) ∖ {𝑥}) = ((𝐹 ∖ {𝑥}) ∪ ({𝑋} ∖ {𝑥}))
66	64, 65	eqtr4di 2789	. . . . . . . . . 10 ⊢ (((𝑊 ∈ LVec ∧ 𝐹 ∈ (LIndS‘𝑊) ∧ 𝑋 ∈ ((Base‘𝑊) ∖ ((LSpan‘𝑊)‘𝐹))) ∧ 𝑥 ∈ 𝐹) → ((𝐹 ∖ {𝑥}) ∪ {𝑋}) = ((𝐹 ∪ {𝑋}) ∖ {𝑥}))
67	66	fveq2d 6844	. . . . . . . . 9 ⊢ (((𝑊 ∈ LVec ∧ 𝐹 ∈ (LIndS‘𝑊) ∧ 𝑋 ∈ ((Base‘𝑊) ∖ ((LSpan‘𝑊)‘𝐹))) ∧ 𝑥 ∈ 𝐹) → ((LSpan‘𝑊)‘((𝐹 ∖ {𝑥}) ∪ {𝑋})) = ((LSpan‘𝑊)‘((𝐹 ∪ {𝑋}) ∖ {𝑥})))
68	67	eleq2d 2822	. . . . . . . 8 ⊢ (((𝑊 ∈ LVec ∧ 𝐹 ∈ (LIndS‘𝑊) ∧ 𝑋 ∈ ((Base‘𝑊) ∖ ((LSpan‘𝑊)‘𝐹))) ∧ 𝑥 ∈ 𝐹) → (𝑥 ∈ ((LSpan‘𝑊)‘((𝐹 ∖ {𝑥}) ∪ {𝑋})) ↔ 𝑥 ∈ ((LSpan‘𝑊)‘((𝐹 ∪ {𝑋}) ∖ {𝑥}))))
69	68	adantrr 718	. . . . . . 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 4731	. . . . . . . . . . . . . . 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 3921	. . . . . . . . . . . . 13 ⊢ ((𝐹 ∈ (LIndS‘𝑊) ∧ 𝑥 ∈ 𝐹) → 𝑥 ∈ (Base‘𝑊))
75		eqid 2736	. . . . . . . . . . . . . 14 ⊢ ( ·_𝑠 ‘𝑊) = ( ·_𝑠 ‘𝑊)
76	1, 21, 75, 25, 24, 31	lspsnvs 21112	. . . . . . . . . . . . 13 ⊢ ((𝑊 ∈ LVec ∧ (𝑘 ∈ (Base‘(Scalar‘𝑊)) ∧ 𝑘 ≠ (0_g‘(Scalar‘𝑊))) ∧ 𝑥 ∈ (Base‘𝑊)) → ((LSpan‘𝑊)‘{(𝑘( ·_𝑠 ‘𝑊)𝑥)}) = ((LSpan‘𝑊)‘{𝑥}))
77	70, 73, 74, 76	syl2an3an 1425	. . . . . . . . . . . 12 ⊢ (((𝑊 ∈ LVec ∧ 𝑘 ∈ ((Base‘(Scalar‘𝑊)) ∖ {(0_g‘(Scalar‘𝑊))})) ∧ (𝐹 ∈ (LIndS‘𝑊) ∧ 𝑥 ∈ 𝐹)) → ((LSpan‘𝑊)‘{(𝑘( ·_𝑠 ‘𝑊)𝑥)}) = ((LSpan‘𝑊)‘{𝑥}))
78	77	an42s 662	. . . . . . . . . . 11 ⊢ (((𝑊 ∈ LVec ∧ 𝐹 ∈ (LIndS‘𝑊)) ∧ (𝑥 ∈ 𝐹 ∧ 𝑘 ∈ ((Base‘(Scalar‘𝑊)) ∖ {(0_g‘(Scalar‘𝑊))}))) → ((LSpan‘𝑊)‘{(𝑘( ·_𝑠 ‘𝑊)𝑥)}) = ((LSpan‘𝑊)‘{𝑥}))
79	78	sseq1d 3953	. . . . . . . . . 10 ⊢ (((𝑊 ∈ LVec ∧ 𝐹 ∈ (LIndS‘𝑊)) ∧ (𝑥 ∈ 𝐹 ∧ 𝑘 ∈ ((Base‘(Scalar‘𝑊)) ∖ {(0_g‘(Scalar‘𝑊))}))) → (((LSpan‘𝑊)‘{(𝑘( ·_𝑠 ‘𝑊)𝑥)}) ⊆ ((LSpan‘𝑊)‘((𝐹 ∪ {𝑋}) ∖ {𝑥})) ↔ ((LSpan‘𝑊)‘{𝑥}) ⊆ ((LSpan‘𝑊)‘((𝐹 ∪ {𝑋}) ∖ {𝑥}))))
80	79	3adantl3 1170	. . . . . . . . 9 ⊢ (((𝑊 ∈ LVec ∧ 𝐹 ∈ (LIndS‘𝑊) ∧ 𝑋 ∈ (Base‘𝑊)) ∧ (𝑥 ∈ 𝐹 ∧ 𝑘 ∈ ((Base‘(Scalar‘𝑊)) ∖ {(0_g‘(Scalar‘𝑊))}))) → (((LSpan‘𝑊)‘{(𝑘( ·_𝑠 ‘𝑊)𝑥)}) ⊆ ((LSpan‘𝑊)‘((𝐹 ∪ {𝑋}) ∖ {𝑥})) ↔ ((LSpan‘𝑊)‘{𝑥}) ⊆ ((LSpan‘𝑊)‘((𝐹 ∪ {𝑋}) ∖ {𝑥}))))
81		eldifi 4071	. . . . . . . . . 10 ⊢ (𝑘 ∈ ((Base‘(Scalar‘𝑊)) ∖ {(0_g‘(Scalar‘𝑊))}) → 𝑘 ∈ (Base‘(Scalar‘𝑊)))
82	19	3ad2ant1 1134	. . . . . . . . . . . 12 ⊢ ((𝑊 ∈ LVec ∧ 𝐹 ∈ (LIndS‘𝑊) ∧ 𝑋 ∈ (Base‘𝑊)) → 𝑊 ∈ LMod)
83	82	adantr 480	. . . . . . . . . . 11 ⊢ (((𝑊 ∈ LVec ∧ 𝐹 ∈ (LIndS‘𝑊) ∧ 𝑋 ∈ (Base‘𝑊)) ∧ (𝑥 ∈ 𝐹 ∧ 𝑘 ∈ (Base‘(Scalar‘𝑊)))) → 𝑊 ∈ LMod)
84		snssi 4729	. . . . . . . . . . . . . . . 16 ⊢ (𝑋 ∈ (Base‘𝑊) → {𝑋} ⊆ (Base‘𝑊))
85	2, 84, 6	syl2an 597	. . . . . . . . . . . . . . 15 ⊢ ((𝐹 ∈ (LIndS‘𝑊) ∧ 𝑋 ∈ (Base‘𝑊)) → (𝐹 ∪ {𝑋}) ⊆ (Base‘𝑊))
86	85	ssdifssd 4087	. . . . . . . . . . . . . 14 ⊢ ((𝐹 ∈ (LIndS‘𝑊) ∧ 𝑋 ∈ (Base‘𝑊)) → ((𝐹 ∪ {𝑋}) ∖ {𝑥}) ⊆ (Base‘𝑊))
87	1, 37, 31	lspcl 20971	. . . . . . . . . . . . . 14 ⊢ ((𝑊 ∈ LMod ∧ ((𝐹 ∪ {𝑋}) ∖ {𝑥}) ⊆ (Base‘𝑊)) → ((LSpan‘𝑊)‘((𝐹 ∪ {𝑋}) ∖ {𝑥})) ∈ (LSubSp‘𝑊))
88	19, 86, 87	syl2an 597	. . . . . . . . . . . . 13 ⊢ ((𝑊 ∈ LVec ∧ (𝐹 ∈ (LIndS‘𝑊) ∧ 𝑋 ∈ (Base‘𝑊))) → ((LSpan‘𝑊)‘((𝐹 ∪ {𝑋}) ∖ {𝑥})) ∈ (LSubSp‘𝑊))
89	88	3impb 1115	. . . . . . . . . . . 12 ⊢ ((𝑊 ∈ LVec ∧ 𝐹 ∈ (LIndS‘𝑊) ∧ 𝑋 ∈ (Base‘𝑊)) → ((LSpan‘𝑊)‘((𝐹 ∪ {𝑋}) ∖ {𝑥})) ∈ (LSubSp‘𝑊))
90	89	adantr 480	. . . . . . . . . . 11 ⊢ (((𝑊 ∈ LVec ∧ 𝐹 ∈ (LIndS‘𝑊) ∧ 𝑋 ∈ (Base‘𝑊)) ∧ (𝑥 ∈ 𝐹 ∧ 𝑘 ∈ (Base‘(Scalar‘𝑊)))) → ((LSpan‘𝑊)‘((𝐹 ∪ {𝑋}) ∖ {𝑥})) ∈ (LSubSp‘𝑊))
91	19	anim1i 616	. . . . . . . . . . . . . 14 ⊢ ((𝑊 ∈ LVec ∧ 𝑘 ∈ (Base‘(Scalar‘𝑊))) → (𝑊 ∈ LMod ∧ 𝑘 ∈ (Base‘(Scalar‘𝑊))))
92	1, 21, 75, 25	lmodvscl 20873	. . . . . . . . . . . . . . 15 ⊢ ((𝑊 ∈ LMod ∧ 𝑘 ∈ (Base‘(Scalar‘𝑊)) ∧ 𝑥 ∈ (Base‘𝑊)) → (𝑘( ·_𝑠 ‘𝑊)𝑥) ∈ (Base‘𝑊))
93	92	3expa 1119	. . . . . . . . . . . . . 14 ⊢ (((𝑊 ∈ LMod ∧ 𝑘 ∈ (Base‘(Scalar‘𝑊))) ∧ 𝑥 ∈ (Base‘𝑊)) → (𝑘( ·_𝑠 ‘𝑊)𝑥) ∈ (Base‘𝑊))
94	91, 74, 93	syl2an 597	. . . . . . . . . . . . 13 ⊢ (((𝑊 ∈ LVec ∧ 𝑘 ∈ (Base‘(Scalar‘𝑊))) ∧ (𝐹 ∈ (LIndS‘𝑊) ∧ 𝑥 ∈ 𝐹)) → (𝑘( ·_𝑠 ‘𝑊)𝑥) ∈ (Base‘𝑊))
95	94	an42s 662	. . . . . . . . . . . 12 ⊢ (((𝑊 ∈ LVec ∧ 𝐹 ∈ (LIndS‘𝑊)) ∧ (𝑥 ∈ 𝐹 ∧ 𝑘 ∈ (Base‘(Scalar‘𝑊)))) → (𝑘( ·_𝑠 ‘𝑊)𝑥) ∈ (Base‘𝑊))
96	95	3adantl3 1170	. . . . . . . . . . 11 ⊢ (((𝑊 ∈ LVec ∧ 𝐹 ∈ (LIndS‘𝑊) ∧ 𝑋 ∈ (Base‘𝑊)) ∧ (𝑥 ∈ 𝐹 ∧ 𝑘 ∈ (Base‘(Scalar‘𝑊)))) → (𝑘( ·_𝑠 ‘𝑊)𝑥) ∈ (Base‘𝑊))
97	1, 37, 31, 83, 90, 96	ellspsn5b 20990	. . . . . . . . . 10 ⊢ (((𝑊 ∈ LVec ∧ 𝐹 ∈ (LIndS‘𝑊) ∧ 𝑋 ∈ (Base‘𝑊)) ∧ (𝑥 ∈ 𝐹 ∧ 𝑘 ∈ (Base‘(Scalar‘𝑊)))) → ((𝑘( ·_𝑠 ‘𝑊)𝑥) ∈ ((LSpan‘𝑊)‘((𝐹 ∪ {𝑋}) ∖ {𝑥})) ↔ ((LSpan‘𝑊)‘{(𝑘( ·_𝑠 ‘𝑊)𝑥)}) ⊆ ((LSpan‘𝑊)‘((𝐹 ∪ {𝑋}) ∖ {𝑥}))))
98	81, 97	sylanr2 684	. . . . . . . . 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 1188	. . . . . . . . . . 11 ⊢ (((𝑊 ∈ LVec ∧ 𝐹 ∈ (LIndS‘𝑊) ∧ 𝑋 ∈ (Base‘𝑊)) ∧ 𝑥 ∈ 𝐹) → 𝑥 ∈ (Base‘𝑊))
102	1, 37, 31, 99, 100, 101	ellspsn5b 20990	. . . . . . . . . 10 ⊢ (((𝑊 ∈ LVec ∧ 𝐹 ∈ (LIndS‘𝑊) ∧ 𝑋 ∈ (Base‘𝑊)) ∧ 𝑥 ∈ 𝐹) → (𝑥 ∈ ((LSpan‘𝑊)‘((𝐹 ∪ {𝑋}) ∖ {𝑥})) ↔ ((LSpan‘𝑊)‘{𝑥}) ⊆ ((LSpan‘𝑊)‘((𝐹 ∪ {𝑋}) ∖ {𝑥}))))
103	102	adantrr 718	. . . . . . . . 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 1417	. . . . . . 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 4753	. . . . . . . . 9 ⊢ (𝑥 ∈ 𝐹 → ((𝐹 ∖ {𝑥}) ∪ {𝑥}) = 𝐹)
108	107	fveq2d 6844	. . . . . . . 8 ⊢ (𝑥 ∈ 𝐹 → ((LSpan‘𝑊)‘((𝐹 ∖ {𝑥}) ∪ {𝑥})) = ((LSpan‘𝑊)‘𝐹))
109	108	eleq2d 2822	. . . . . . 7 ⊢ (𝑥 ∈ 𝐹 → (𝑋 ∈ ((LSpan‘𝑊)‘((𝐹 ∖ {𝑥}) ∪ {𝑥})) ↔ 𝑋 ∈ ((LSpan‘𝑊)‘𝐹)))
110	109	ad2antrl 729	. . . . . 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 3180	. . 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 4743	. . . . . . . . . . 11 ⊢ (¬ 𝑋 ∈ 𝐹 → (𝐹 ∖ {𝑋}) = 𝐹)
116	54, 115	syl 17	. . . . . . . . . 10 ⊢ ((𝑊 ∈ LVec ∧ 𝐹 ∈ (LIndS‘𝑊) ∧ 𝑋 ∈ ((Base‘𝑊) ∖ ((LSpan‘𝑊)‘𝐹))) → (𝐹 ∖ {𝑋}) = 𝐹)
117	116	fveq2d 6844	. . . . . . . . 9 ⊢ ((𝑊 ∈ LVec ∧ 𝐹 ∈ (LIndS‘𝑊) ∧ 𝑋 ∈ ((Base‘𝑊) ∖ ((LSpan‘𝑊)‘𝐹))) → ((LSpan‘𝑊)‘(𝐹 ∖ {𝑋})) = ((LSpan‘𝑊)‘𝐹))
118	117	eleq2d 2822	. . . . . . . 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 21112	. . . . . . . . . . . . . 14 ⊢ ((𝑊 ∈ LVec ∧ (𝑘 ∈ (Base‘(Scalar‘𝑊)) ∧ 𝑘 ≠ (0_g‘(Scalar‘𝑊))) ∧ 𝑋 ∈ (Base‘𝑊)) → ((LSpan‘𝑊)‘{(𝑘( ·_𝑠 ‘𝑊)𝑋)}) = ((LSpan‘𝑊)‘{𝑋}))
121	120	3expa 1119	. . . . . . . . . . . . 13 ⊢ (((𝑊 ∈ LVec ∧ (𝑘 ∈ (Base‘(Scalar‘𝑊)) ∧ 𝑘 ≠ (0_g‘(Scalar‘𝑊)))) ∧ 𝑋 ∈ (Base‘𝑊)) → ((LSpan‘𝑊)‘{(𝑘( ·_𝑠 ‘𝑊)𝑋)}) = ((LSpan‘𝑊)‘{𝑋}))
122	121	an32s 653	. . . . . . . . . . . 12 ⊢ (((𝑊 ∈ LVec ∧ 𝑋 ∈ (Base‘𝑊)) ∧ (𝑘 ∈ (Base‘(Scalar‘𝑊)) ∧ 𝑘 ≠ (0_g‘(Scalar‘𝑊)))) → ((LSpan‘𝑊)‘{(𝑘( ·_𝑠 ‘𝑊)𝑋)}) = ((LSpan‘𝑊)‘{𝑋}))
123	71, 122	sylan2b 595	. . . . . . . . . . 11 ⊢ (((𝑊 ∈ LVec ∧ 𝑋 ∈ (Base‘𝑊)) ∧ 𝑘 ∈ ((Base‘(Scalar‘𝑊)) ∖ {(0_g‘(Scalar‘𝑊))})) → ((LSpan‘𝑊)‘{(𝑘( ·_𝑠 ‘𝑊)𝑋)}) = ((LSpan‘𝑊)‘{𝑋}))
124	123	sseq1d 3953	. . . . . . . . . 10 ⊢ (((𝑊 ∈ LVec ∧ 𝑋 ∈ (Base‘𝑊)) ∧ 𝑘 ∈ ((Base‘(Scalar‘𝑊)) ∖ {(0_g‘(Scalar‘𝑊))})) → (((LSpan‘𝑊)‘{(𝑘( ·_𝑠 ‘𝑊)𝑋)}) ⊆ ((LSpan‘𝑊)‘𝐹) ↔ ((LSpan‘𝑊)‘{𝑋}) ⊆ ((LSpan‘𝑊)‘𝐹)))
125	124	3adantl2 1169	. . . . . . . . 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 20971	. . . . . . . . . . . . . 14 ⊢ ((𝑊 ∈ LMod ∧ 𝐹 ⊆ (Base‘𝑊)) → ((LSpan‘𝑊)‘𝐹) ∈ (LSubSp‘𝑊))
128	19, 2, 127	syl2an 597	. . . . . . . . . . . . 13 ⊢ ((𝑊 ∈ LVec ∧ 𝐹 ∈ (LIndS‘𝑊)) → ((LSpan‘𝑊)‘𝐹) ∈ (LSubSp‘𝑊))
129	128	3adant3 1133	. . . . . . . . . . . 12 ⊢ ((𝑊 ∈ LVec ∧ 𝐹 ∈ (LIndS‘𝑊) ∧ 𝑋 ∈ (Base‘𝑊)) → ((LSpan‘𝑊)‘𝐹) ∈ (LSubSp‘𝑊))
130	129	adantr 480	. . . . . . . . . . 11 ⊢ (((𝑊 ∈ LVec ∧ 𝐹 ∈ (LIndS‘𝑊) ∧ 𝑋 ∈ (Base‘𝑊)) ∧ 𝑘 ∈ (Base‘(Scalar‘𝑊))) → ((LSpan‘𝑊)‘𝐹) ∈ (LSubSp‘𝑊))
131	1, 21, 75, 25	lmodvscl 20873	. . . . . . . . . . . . . . 15 ⊢ ((𝑊 ∈ LMod ∧ 𝑘 ∈ (Base‘(Scalar‘𝑊)) ∧ 𝑋 ∈ (Base‘𝑊)) → (𝑘( ·_𝑠 ‘𝑊)𝑋) ∈ (Base‘𝑊))
132	131	3expa 1119	. . . . . . . . . . . . . 14 ⊢ (((𝑊 ∈ LMod ∧ 𝑘 ∈ (Base‘(Scalar‘𝑊))) ∧ 𝑋 ∈ (Base‘𝑊)) → (𝑘( ·_𝑠 ‘𝑊)𝑋) ∈ (Base‘𝑊))
133	132	an32s 653	. . . . . . . . . . . . 13 ⊢ (((𝑊 ∈ LMod ∧ 𝑋 ∈ (Base‘𝑊)) ∧ 𝑘 ∈ (Base‘(Scalar‘𝑊))) → (𝑘( ·_𝑠 ‘𝑊)𝑋) ∈ (Base‘𝑊))
134	19, 133	sylanl1 681	. . . . . . . . . . . 12 ⊢ (((𝑊 ∈ LVec ∧ 𝑋 ∈ (Base‘𝑊)) ∧ 𝑘 ∈ (Base‘(Scalar‘𝑊))) → (𝑘( ·_𝑠 ‘𝑊)𝑋) ∈ (Base‘𝑊))
135	134	3adantl2 1169	. . . . . . . . . . 11 ⊢ (((𝑊 ∈ LVec ∧ 𝐹 ∈ (LIndS‘𝑊) ∧ 𝑋 ∈ (Base‘𝑊)) ∧ 𝑘 ∈ (Base‘(Scalar‘𝑊))) → (𝑘( ·_𝑠 ‘𝑊)𝑋) ∈ (Base‘𝑊))
136	1, 37, 31, 126, 130, 135	ellspsn5b 20990	. . . . . . . . . 10 ⊢ (((𝑊 ∈ LVec ∧ 𝐹 ∈ (LIndS‘𝑊) ∧ 𝑋 ∈ (Base‘𝑊)) ∧ 𝑘 ∈ (Base‘(Scalar‘𝑊))) → ((𝑘( ·_𝑠 ‘𝑊)𝑋) ∈ ((LSpan‘𝑊)‘𝐹) ↔ ((LSpan‘𝑊)‘{(𝑘( ·_𝑠 ‘𝑊)𝑋)}) ⊆ ((LSpan‘𝑊)‘𝐹)))
137	81, 136	sylan2 594	. . . . . . . . 9 ⊢ (((𝑊 ∈ LVec ∧ 𝐹 ∈ (LIndS‘𝑊) ∧ 𝑋 ∈ (Base‘𝑊)) ∧ 𝑘 ∈ ((Base‘(Scalar‘𝑊)) ∖ {(0_g‘(Scalar‘𝑊))})) → ((𝑘( ·_𝑠 ‘𝑊)𝑋) ∈ ((LSpan‘𝑊)‘𝐹) ↔ ((LSpan‘𝑊)‘{(𝑘( ·_𝑠 ‘𝑊)𝑋)}) ⊆ ((LSpan‘𝑊)‘𝐹)))
138		simp3 1139	. . . . . . . . . . 11 ⊢ ((𝑊 ∈ LVec ∧ 𝐹 ∈ (LIndS‘𝑊) ∧ 𝑋 ∈ (Base‘𝑊)) → 𝑋 ∈ (Base‘𝑊))
139	1, 37, 31, 82, 129, 138	ellspsn5b 20990	. . . . . . . . . 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 1417	. . . . . . 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 3129	. . . 4 ⊢ ((𝑊 ∈ LVec ∧ 𝐹 ∈ (LIndS‘𝑊) ∧ 𝑋 ∈ ((Base‘𝑊) ∖ ((LSpan‘𝑊)‘𝐹))) → ∀𝑘 ∈ ((Base‘(Scalar‘𝑊)) ∖ {(0_g‘(Scalar‘𝑊))}) ¬ (𝑘( ·_𝑠 ‘𝑊)𝑋) ∈ ((LSpan‘𝑊)‘(𝐹 ∖ {𝑋})))
146		oveq2 7375	. . . . . . . . 9 ⊢ (𝑥 = 𝑋 → (𝑘( ·_𝑠 ‘𝑊)𝑥) = (𝑘( ·_𝑠 ‘𝑊)𝑋))
147		sneq 4577	. . . . . . . . . . . 12 ⊢ (𝑥 = 𝑋 → {𝑥} = {𝑋})
148	147	difeq2d 4066	. . . . . . . . . . 11 ⊢ (𝑥 = 𝑋 → ((𝐹 ∪ {𝑋}) ∖ {𝑥}) = ((𝐹 ∪ {𝑋}) ∖ {𝑋}))
149		difun2 4421	. . . . . . . . . . 11 ⊢ ((𝐹 ∪ {𝑋}) ∖ {𝑋}) = (𝐹 ∖ {𝑋})
150	148, 149	eqtrdi 2787	. . . . . . . . . 10 ⊢ (𝑥 = 𝑋 → ((𝐹 ∪ {𝑋}) ∖ {𝑥}) = (𝐹 ∖ {𝑋}))
151	150	fveq2d 6844	. . . . . . . . 9 ⊢ (𝑥 = 𝑋 → ((LSpan‘𝑊)‘((𝐹 ∪ {𝑋}) ∖ {𝑥})) = ((LSpan‘𝑊)‘(𝐹 ∖ {𝑋})))
152	146, 151	eleq12d 2830	. . . . . . . 8 ⊢ (𝑥 = 𝑋 → ((𝑘( ·_𝑠 ‘𝑊)𝑥) ∈ ((LSpan‘𝑊)‘((𝐹 ∪ {𝑋}) ∖ {𝑥})) ↔ (𝑘( ·_𝑠 ‘𝑊)𝑋) ∈ ((LSpan‘𝑊)‘(𝐹 ∖ {𝑋}))))
153	152	notbid 318	. . . . . . 7 ⊢ (𝑥 = 𝑋 → (¬ (𝑘( ·_𝑠 ‘𝑊)𝑥) ∈ ((LSpan‘𝑊)‘((𝐹 ∪ {𝑋}) ∖ {𝑥})) ↔ ¬ (𝑘( ·_𝑠 ‘𝑊)𝑋) ∈ ((LSpan‘𝑊)‘(𝐹 ∖ {𝑋}))))
154	153	ralbidv 3160	. . . . . 6 ⊢ (𝑥 = 𝑋 → (∀𝑘 ∈ ((Base‘(Scalar‘𝑊)) ∖ {(0_g‘(Scalar‘𝑊))}) ¬ (𝑘( ·_𝑠 ‘𝑊)𝑥) ∈ ((LSpan‘𝑊)‘((𝐹 ∪ {𝑋}) ∖ {𝑥})) ↔ ∀𝑘 ∈ ((Base‘(Scalar‘𝑊)) ∖ {(0_g‘(Scalar‘𝑊))}) ¬ (𝑘( ·_𝑠 ‘𝑊)𝑋) ∈ ((LSpan‘𝑊)‘(𝐹 ∖ {𝑋}))))
155	154	ralsng 4619	. . . . 5 ⊢ (𝑋 ∈ ((Base‘𝑊) ∖ ((LSpan‘𝑊)‘𝐹)) → (∀𝑥 ∈ {𝑋}∀𝑘 ∈ ((Base‘(Scalar‘𝑊)) ∖ {(0_g‘(Scalar‘𝑊))}) ¬ (𝑘( ·_𝑠 ‘𝑊)𝑥) ∈ ((LSpan‘𝑊)‘((𝐹 ∪ {𝑋}) ∖ {𝑥})) ↔ ∀𝑘 ∈ ((Base‘(Scalar‘𝑊)) ∖ {(0_g‘(Scalar‘𝑊))}) ¬ (𝑘( ·_𝑠 ‘𝑊)𝑋) ∈ ((LSpan‘𝑊)‘(𝐹 ∖ {𝑋}))))
156	155	3ad2ant3 1136	. . . 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 4137	. . 3 ⊢ (∀𝑥 ∈ (𝐹 ∪ {𝑋})∀𝑘 ∈ ((Base‘(Scalar‘𝑊)) ∖ {(0_g‘(Scalar‘𝑊))}) ¬ (𝑘( ·_𝑠 ‘𝑊)𝑥) ∈ ((LSpan‘𝑊)‘((𝐹 ∪ {𝑋}) ∖ {𝑥})) ↔ (∀𝑥 ∈ 𝐹 ∀𝑘 ∈ ((Base‘(Scalar‘𝑊)) ∖ {(0_g‘(Scalar‘𝑊))}) ¬ (𝑘( ·_𝑠 ‘𝑊)𝑥) ∈ ((LSpan‘𝑊)‘((𝐹 ∪ {𝑋}) ∖ {𝑥})) ∧ ∀𝑥 ∈ {𝑋}∀𝑘 ∈ ((Base‘(Scalar‘𝑊)) ∖ {(0_g‘(Scalar‘𝑊))}) ¬ (𝑘( ·_𝑠 ‘𝑊)𝑥) ∈ ((LSpan‘𝑊)‘((𝐹 ∪ {𝑋}) ∖ {𝑥}))))
159	113, 157, 158	sylanbrc 584	. 2 ⊢ ((𝑊 ∈ LVec ∧ 𝐹 ∈ (LIndS‘𝑊) ∧ 𝑋 ∈ ((Base‘𝑊) ∖ ((LSpan‘𝑊)‘𝐹))) → ∀𝑥 ∈ (𝐹 ∪ {𝑋})∀𝑘 ∈ ((Base‘(Scalar‘𝑊)) ∖ {(0_g‘(Scalar‘𝑊))}) ¬ (𝑘( ·_𝑠 ‘𝑊)𝑥) ∈ ((LSpan‘𝑊)‘((𝐹 ∪ {𝑋}) ∖ {𝑥})))
160	1, 75, 31, 21, 25, 24	islinds2 21793	. . 3 ⊢ (𝑊 ∈ LVec → ((𝐹 ∪ {𝑋}) ∈ (LIndS‘𝑊) ↔ ((𝐹 ∪ {𝑋}) ⊆ (Base‘𝑊) ∧ ∀𝑥 ∈ (𝐹 ∪ {𝑋})∀𝑘 ∈ ((Base‘(Scalar‘𝑊)) ∖ {(0_g‘(Scalar‘𝑊))}) ¬ (𝑘( ·_𝑠 ‘𝑊)𝑥) ∈ ((LSpan‘𝑊)‘((𝐹 ∪ {𝑋}) ∖ {𝑥})))))
161	160	3ad2ant1 1134	. 2 ⊢ ((𝑊 ∈ LVec ∧ 𝐹 ∈ (LIndS‘𝑊) ∧ 𝑋 ∈ ((Base‘𝑊) ∖ ((LSpan‘𝑊)‘𝐹))) → ((𝐹 ∪ {𝑋}) ∈ (LIndS‘𝑊) ↔ ((𝐹 ∪ {𝑋}) ⊆ (Base‘𝑊) ∧ ∀𝑥 ∈ (𝐹 ∪ {𝑋})∀𝑘 ∈ ((Base‘(Scalar‘𝑊)) ∖ {(0_g‘(Scalar‘𝑊))}) ¬ (𝑘( ·_𝑠 ‘𝑊)𝑥) ∈ ((LSpan‘𝑊)‘((𝐹 ∪ {𝑋}) ∖ {𝑥})))))
162	8, 159, 161	mpbir2and 714	1 ⊢ ((𝑊 ∈ LVec ∧ 𝐹 ∈ (LIndS‘𝑊) ∧ 𝑋 ∈ ((Base‘𝑊) ∖ ((LSpan‘𝑊)‘𝐹))) → (𝐹 ∪ {𝑋}) ∈ (LIndS‘𝑊))

Colors of variables: wff setvar class

Syntax hints: ¬ wn 3 → wi 4 ↔ wb 206 ∧ wa 395 ∧ w3a 1087 = wceq 1542 ∈ wcel 2114 ≠ wne 2932 ∀wral 3051 ∖ cdif 3886 ∪ cun 3887 ∩ cin 3888 ⊆ wss 3889 ∅c0 4273 {csn 4567 ‘cfv 6498 (class class class)co 7367 Basecbs 17179 Scalarcsca 17223 ·_𝑠 cvsca 17224 0_gc0g 17402 Ringcrg 20214 NzRingcnzr 20489 LModclmod 20855 LSubSpclss 20926 LSpanclspn 20966 LVecclvec 21097 LIndSclinds 21785

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1797 ax-4 1811 ax-5 1912 ax-6 1969 ax-7 2010 ax-8 2116 ax-9 2124 ax-10 2147 ax-11 2163 ax-12 2185 ax-ext 2708 ax-rep 5212 ax-sep 5231 ax-nul 5241 ax-pow 5307 ax-pr 5375 ax-un 7689 ax-cnex 11094 ax-resscn 11095 ax-1cn 11096 ax-icn 11097 ax-addcl 11098 ax-addrcl 11099 ax-mulcl 11100 ax-mulrcl 11101 ax-mulcom 11102 ax-addass 11103 ax-mulass 11104 ax-distr 11105 ax-i2m1 11106 ax-1ne0 11107 ax-1rid 11108 ax-rnegex 11109 ax-rrecex 11110 ax-cnre 11111 ax-pre-lttri 11112 ax-pre-lttrn 11113 ax-pre-ltadd 11114 ax-pre-mulgt0 11115

This theorem depends on definitions: df-bi 207 df-an 396 df-or 849 df-3or 1088 df-3an 1089 df-tru 1545 df-fal 1555 df-ex 1782 df-nf 1786 df-sb 2069 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 3062 df-rmo 3342 df-reu 3343 df-rab 3390 df-v 3431 df-sbc 3729 df-csb 3838 df-dif 3892 df-un 3894 df-in 3896 df-ss 3906 df-pss 3909 df-nul 4274 df-if 4467 df-pw 4543 df-sn 4568 df-pr 4570 df-op 4574 df-uni 4851 df-int 4890 df-iun 4935 df-br 5086 df-opab 5148 df-mpt 5167 df-tr 5193 df-id 5526 df-eprel 5531 df-po 5539 df-so 5540 df-fr 5584 df-we 5586 df-xp 5637 df-rel 5638 df-cnv 5639 df-co 5640 df-dm 5641 df-rn 5642 df-res 5643 df-ima 5644 df-pred 6265 df-ord 6326 df-on 6327 df-lim 6328 df-suc 6329 df-iota 6454 df-fun 6500 df-fn 6501 df-f 6502 df-f1 6503 df-fo 6504 df-f1o 6505 df-fv 6506 df-riota 7324 df-ov 7370 df-oprab 7371 df-mpo 7372 df-om 7818 df-1st 7942 df-2nd 7943 df-tpos 8176 df-frecs 8231 df-wrecs 8262 df-recs 8311 df-rdg 8349 df-er 8643 df-en 8894 df-dom 8895 df-sdom 8896 df-pnf 11181 df-mnf 11182 df-xr 11183 df-ltxr 11184 df-le 11185 df-sub 11379 df-neg 11380 df-nn 12175 df-2 12244 df-3 12245 df-sets 17134 df-slot 17152 df-ndx 17164 df-base 17180 df-ress 17201 df-plusg 17233 df-mulr 17234 df-0g 17404 df-mgm 18608 df-sgrp 18687 df-mnd 18703 df-grp 18912 df-minusg 18913 df-sbg 18914 df-cmn 19757 df-abl 19758 df-mgp 20122 df-rng 20134 df-ur 20163 df-ring 20216 df-oppr 20317 df-dvdsr 20337 df-unit 20338 df-invr 20368 df-nzr 20490 df-drng 20708 df-lmod 20857 df-lss 20927 df-lsp 20967 df-lvec 21098 df-lindf 21786 df-linds 21787

This theorem is referenced by: (None)

W3C validator