Theorem baerlem3lem2 38840

Description: Lemma for baerlem3 38843. (Contributed by NM, 9-Apr-2015.)

Hypotheses

Ref	Expression
baerlem3.v	⊢ 𝑉 = (Base‘𝑊)
baerlem3.m	⊢ − = (-g‘𝑊)
baerlem3.o	⊢ 0 = (0g‘𝑊)
baerlem3.s	⊢ ⊕ = (LSSum‘𝑊)
baerlem3.n	⊢ 𝑁 = (LSpan‘𝑊)
baerlem3.w	⊢ (𝜑 → 𝑊 ∈ LVec)
baerlem3.x	⊢ (𝜑 → 𝑋 ∈ 𝑉)
baerlem3.c	⊢ (𝜑 → ¬ 𝑋 ∈ (𝑁‘{𝑌, 𝑍}))
baerlem3.d	⊢ (𝜑 → (𝑁‘{𝑌}) ≠ (𝑁‘{𝑍}))
baerlem3.y	⊢ (𝜑 → 𝑌 ∈ (𝑉 ∖ { 0 }))
baerlem3.z	⊢ (𝜑 → 𝑍 ∈ (𝑉 ∖ { 0 }))
baerlem3.p	⊢ + = (+g‘𝑊)
baerlem3.t	⊢ · = ( ·𝑠 ‘𝑊)
baerlem3.r	⊢ 𝑅 = (Scalar‘𝑊)
baerlem3.b	⊢ 𝐵 = (Base‘𝑅)
baerlem3.a	⊢ ⨣ = (+g‘𝑅)
baerlem3.l	⊢ 𝐿 = (-g‘𝑅)
baerlem3.q	⊢ 𝑄 = (0g‘𝑅)
baerlem3.i	⊢ 𝐼 = (invg‘𝑅)

Assertion

Ref	Expression
baerlem3lem2	⊢ (𝜑 → (𝑁‘{(𝑌 − 𝑍)}) = (((𝑁‘{𝑌}) ⊕ (𝑁‘{𝑍})) ∩ ((𝑁‘{(𝑋 − 𝑌)}) ⊕ (𝑁‘{(𝑋 − 𝑍)}))))

Proof of Theorem baerlem3lem2

Dummy variables 𝑎 𝑏 𝑑 𝑒 𝑗 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		baerlem3.w	. . . . 5 ⊢ (𝜑 → 𝑊 ∈ LVec)
2		lveclmod 19872	. . . . 5 ⊢ (𝑊 ∈ LVec → 𝑊 ∈ LMod)
3	1, 2	syl 17	. . . 4 ⊢ (𝜑 → 𝑊 ∈ LMod)
4		baerlem3.y	. . . . 5 ⊢ (𝜑 → 𝑌 ∈ (𝑉 ∖ { 0 }))
5	4	eldifad 3948	. . . 4 ⊢ (𝜑 → 𝑌 ∈ 𝑉)
6		baerlem3.z	. . . . 5 ⊢ (𝜑 → 𝑍 ∈ (𝑉 ∖ { 0 }))
7	6	eldifad 3948	. . . 4 ⊢ (𝜑 → 𝑍 ∈ 𝑉)
8		baerlem3.v	. . . . 5 ⊢ 𝑉 = (Base‘𝑊)
9		baerlem3.m	. . . . 5 ⊢ − = (-g‘𝑊)
10		baerlem3.s	. . . . 5 ⊢ ⊕ = (LSSum‘𝑊)
11		baerlem3.n	. . . . 5 ⊢ 𝑁 = (LSpan‘𝑊)
12	8, 9, 10, 11	lspsntrim 19864	. . . 4 ⊢ ((𝑊 ∈ LMod ∧ 𝑌 ∈ 𝑉 ∧ 𝑍 ∈ 𝑉) → (𝑁‘{(𝑌 − 𝑍)}) ⊆ ((𝑁‘{𝑌}) ⊕ (𝑁‘{𝑍})))
13	3, 5, 7, 12	syl3anc 1367	. . 3 ⊢ (𝜑 → (𝑁‘{(𝑌 − 𝑍)}) ⊆ ((𝑁‘{𝑌}) ⊕ (𝑁‘{𝑍})))
14	8, 9, 11, 3, 5, 7	lspsnsub 19773	. . . . 5 ⊢ (𝜑 → (𝑁‘{(𝑌 − 𝑍)}) = (𝑁‘{(𝑍 − 𝑌)}))
15		lmodabl 19675	. . . . . . . . 9 ⊢ (𝑊 ∈ LMod → 𝑊 ∈ Abel)
16	3, 15	syl 17	. . . . . . . 8 ⊢ (𝜑 → 𝑊 ∈ Abel)
17		baerlem3.x	. . . . . . . 8 ⊢ (𝜑 → 𝑋 ∈ 𝑉)
18	8, 9, 16, 17, 5, 7	ablnnncan1 18938	. . . . . . 7 ⊢ (𝜑 → ((𝑋 − 𝑌) − (𝑋 − 𝑍)) = (𝑍 − 𝑌))
19	18	sneqd 4573	. . . . . 6 ⊢ (𝜑 → {((𝑋 − 𝑌) − (𝑋 − 𝑍))} = {(𝑍 − 𝑌)})
20	19	fveq2d 6669	. . . . 5 ⊢ (𝜑 → (𝑁‘{((𝑋 − 𝑌) − (𝑋 − 𝑍))}) = (𝑁‘{(𝑍 − 𝑌)}))
21	14, 20	eqtr4d 2859	. . . 4 ⊢ (𝜑 → (𝑁‘{(𝑌 − 𝑍)}) = (𝑁‘{((𝑋 − 𝑌) − (𝑋 − 𝑍))}))
22	8, 9	lmodvsubcl 19673	. . . . . 6 ⊢ ((𝑊 ∈ LMod ∧ 𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑉) → (𝑋 − 𝑌) ∈ 𝑉)
23	3, 17, 5, 22	syl3anc 1367	. . . . 5 ⊢ (𝜑 → (𝑋 − 𝑌) ∈ 𝑉)
24	8, 9	lmodvsubcl 19673	. . . . . 6 ⊢ ((𝑊 ∈ LMod ∧ 𝑋 ∈ 𝑉 ∧ 𝑍 ∈ 𝑉) → (𝑋 − 𝑍) ∈ 𝑉)
25	3, 17, 7, 24	syl3anc 1367	. . . . 5 ⊢ (𝜑 → (𝑋 − 𝑍) ∈ 𝑉)
26	8, 9, 10, 11	lspsntrim 19864	. . . . 5 ⊢ ((𝑊 ∈ LMod ∧ (𝑋 − 𝑌) ∈ 𝑉 ∧ (𝑋 − 𝑍) ∈ 𝑉) → (𝑁‘{((𝑋 − 𝑌) − (𝑋 − 𝑍))}) ⊆ ((𝑁‘{(𝑋 − 𝑌)}) ⊕ (𝑁‘{(𝑋 − 𝑍)})))
27	3, 23, 25, 26	syl3anc 1367	. . . 4 ⊢ (𝜑 → (𝑁‘{((𝑋 − 𝑌) − (𝑋 − 𝑍))}) ⊆ ((𝑁‘{(𝑋 − 𝑌)}) ⊕ (𝑁‘{(𝑋 − 𝑍)})))
28	21, 27	eqsstrd 4005	. . 3 ⊢ (𝜑 → (𝑁‘{(𝑌 − 𝑍)}) ⊆ ((𝑁‘{(𝑋 − 𝑌)}) ⊕ (𝑁‘{(𝑋 − 𝑍)})))
29	13, 28	ssind 4209	. 2 ⊢ (𝜑 → (𝑁‘{(𝑌 − 𝑍)}) ⊆ (((𝑁‘{𝑌}) ⊕ (𝑁‘{𝑍})) ∩ ((𝑁‘{(𝑋 − 𝑌)}) ⊕ (𝑁‘{(𝑋 − 𝑍)}))))
30		elin 4169	. . . . 5 ⊢ (𝑗 ∈ (((𝑁‘{𝑌}) ⊕ (𝑁‘{𝑍})) ∩ ((𝑁‘{(𝑋 − 𝑌)}) ⊕ (𝑁‘{(𝑋 − 𝑍)}))) ↔ (𝑗 ∈ ((𝑁‘{𝑌}) ⊕ (𝑁‘{𝑍})) ∧ 𝑗 ∈ ((𝑁‘{(𝑋 − 𝑌)}) ⊕ (𝑁‘{(𝑋 − 𝑍)}))))
31		baerlem3.p	. . . . . . 7 ⊢ + = (+g‘𝑊)
32		baerlem3.r	. . . . . . 7 ⊢ 𝑅 = (Scalar‘𝑊)
33		baerlem3.b	. . . . . . 7 ⊢ 𝐵 = (Base‘𝑅)
34		baerlem3.t	. . . . . . 7 ⊢ · = ( ·𝑠 ‘𝑊)
35	8, 31, 32, 33, 34, 10, 11, 3, 5, 7	lsmspsn 19850	. . . . . 6 ⊢ (𝜑 → (𝑗 ∈ ((𝑁‘{𝑌}) ⊕ (𝑁‘{𝑍})) ↔ ∃𝑎 ∈ 𝐵 ∃𝑏 ∈ 𝐵 𝑗 = ((𝑎 · 𝑌) + (𝑏 · 𝑍))))
36	8, 31, 32, 33, 34, 10, 11, 3, 23, 25	lsmspsn 19850	. . . . . 6 ⊢ (𝜑 → (𝑗 ∈ ((𝑁‘{(𝑋 − 𝑌)}) ⊕ (𝑁‘{(𝑋 − 𝑍)})) ↔ ∃𝑑 ∈ 𝐵 ∃𝑒 ∈ 𝐵 𝑗 = ((𝑑 · (𝑋 − 𝑌)) + (𝑒 · (𝑋 − 𝑍)))))
37	35, 36	anbi12d 632	. . . . 5 ⊢ (𝜑 → ((𝑗 ∈ ((𝑁‘{𝑌}) ⊕ (𝑁‘{𝑍})) ∧ 𝑗 ∈ ((𝑁‘{(𝑋 − 𝑌)}) ⊕ (𝑁‘{(𝑋 − 𝑍)}))) ↔ (∃𝑎 ∈ 𝐵 ∃𝑏 ∈ 𝐵 𝑗 = ((𝑎 · 𝑌) + (𝑏 · 𝑍)) ∧ ∃𝑑 ∈ 𝐵 ∃𝑒 ∈ 𝐵 𝑗 = ((𝑑 · (𝑋 − 𝑌)) + (𝑒 · (𝑋 − 𝑍))))))
38	30, 37	syl5bb 285	. . . 4 ⊢ (𝜑 → (𝑗 ∈ (((𝑁‘{𝑌}) ⊕ (𝑁‘{𝑍})) ∩ ((𝑁‘{(𝑋 − 𝑌)}) ⊕ (𝑁‘{(𝑋 − 𝑍)}))) ↔ (∃𝑎 ∈ 𝐵 ∃𝑏 ∈ 𝐵 𝑗 = ((𝑎 · 𝑌) + (𝑏 · 𝑍)) ∧ ∃𝑑 ∈ 𝐵 ∃𝑒 ∈ 𝐵 𝑗 = ((𝑑 · (𝑋 − 𝑌)) + (𝑒 · (𝑋 − 𝑍))))))
39		baerlem3.o	. . . . . . . . . . 11 ⊢ 0 = (0g‘𝑊)
40		simp11 1199	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ (𝑎 ∈ 𝐵 ∧ 𝑏 ∈ 𝐵) ∧ 𝑗 = ((𝑎 · 𝑌) + (𝑏 · 𝑍))) ∧ (𝑑 ∈ 𝐵 ∧ 𝑒 ∈ 𝐵) ∧ 𝑗 = ((𝑑 · (𝑋 − 𝑌)) + (𝑒 · (𝑋 − 𝑍)))) → 𝜑)
41	40, 1	syl 17	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ (𝑎 ∈ 𝐵 ∧ 𝑏 ∈ 𝐵) ∧ 𝑗 = ((𝑎 · 𝑌) + (𝑏 · 𝑍))) ∧ (𝑑 ∈ 𝐵 ∧ 𝑒 ∈ 𝐵) ∧ 𝑗 = ((𝑑 · (𝑋 − 𝑌)) + (𝑒 · (𝑋 − 𝑍)))) → 𝑊 ∈ LVec)
42	40, 17	syl 17	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ (𝑎 ∈ 𝐵 ∧ 𝑏 ∈ 𝐵) ∧ 𝑗 = ((𝑎 · 𝑌) + (𝑏 · 𝑍))) ∧ (𝑑 ∈ 𝐵 ∧ 𝑒 ∈ 𝐵) ∧ 𝑗 = ((𝑑 · (𝑋 − 𝑌)) + (𝑒 · (𝑋 − 𝑍)))) → 𝑋 ∈ 𝑉)
43		baerlem3.c	. . . . . . . . . . . 12 ⊢ (𝜑 → ¬ 𝑋 ∈ (𝑁‘{𝑌, 𝑍}))
44	40, 43	syl 17	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ (𝑎 ∈ 𝐵 ∧ 𝑏 ∈ 𝐵) ∧ 𝑗 = ((𝑎 · 𝑌) + (𝑏 · 𝑍))) ∧ (𝑑 ∈ 𝐵 ∧ 𝑒 ∈ 𝐵) ∧ 𝑗 = ((𝑑 · (𝑋 − 𝑌)) + (𝑒 · (𝑋 − 𝑍)))) → ¬ 𝑋 ∈ (𝑁‘{𝑌, 𝑍}))
45		baerlem3.d	. . . . . . . . . . . 12 ⊢ (𝜑 → (𝑁‘{𝑌}) ≠ (𝑁‘{𝑍}))
46	40, 45	syl 17	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ (𝑎 ∈ 𝐵 ∧ 𝑏 ∈ 𝐵) ∧ 𝑗 = ((𝑎 · 𝑌) + (𝑏 · 𝑍))) ∧ (𝑑 ∈ 𝐵 ∧ 𝑒 ∈ 𝐵) ∧ 𝑗 = ((𝑑 · (𝑋 − 𝑌)) + (𝑒 · (𝑋 − 𝑍)))) → (𝑁‘{𝑌}) ≠ (𝑁‘{𝑍}))
47	40, 4	syl 17	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ (𝑎 ∈ 𝐵 ∧ 𝑏 ∈ 𝐵) ∧ 𝑗 = ((𝑎 · 𝑌) + (𝑏 · 𝑍))) ∧ (𝑑 ∈ 𝐵 ∧ 𝑒 ∈ 𝐵) ∧ 𝑗 = ((𝑑 · (𝑋 − 𝑌)) + (𝑒 · (𝑋 − 𝑍)))) → 𝑌 ∈ (𝑉 ∖ { 0 }))
48	40, 6	syl 17	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ (𝑎 ∈ 𝐵 ∧ 𝑏 ∈ 𝐵) ∧ 𝑗 = ((𝑎 · 𝑌) + (𝑏 · 𝑍))) ∧ (𝑑 ∈ 𝐵 ∧ 𝑒 ∈ 𝐵) ∧ 𝑗 = ((𝑑 · (𝑋 − 𝑌)) + (𝑒 · (𝑋 − 𝑍)))) → 𝑍 ∈ (𝑉 ∖ { 0 }))
49		baerlem3.a	. . . . . . . . . . 11 ⊢ ⨣ = (+g‘𝑅)
50		baerlem3.l	. . . . . . . . . . 11 ⊢ 𝐿 = (-g‘𝑅)
51		baerlem3.q	. . . . . . . . . . 11 ⊢ 𝑄 = (0g‘𝑅)
52		baerlem3.i	. . . . . . . . . . 11 ⊢ 𝐼 = (invg‘𝑅)
53		simp12l 1282	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ (𝑎 ∈ 𝐵 ∧ 𝑏 ∈ 𝐵) ∧ 𝑗 = ((𝑎 · 𝑌) + (𝑏 · 𝑍))) ∧ (𝑑 ∈ 𝐵 ∧ 𝑒 ∈ 𝐵) ∧ 𝑗 = ((𝑑 · (𝑋 − 𝑌)) + (𝑒 · (𝑋 − 𝑍)))) → 𝑎 ∈ 𝐵)
54		simp12r 1283	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ (𝑎 ∈ 𝐵 ∧ 𝑏 ∈ 𝐵) ∧ 𝑗 = ((𝑎 · 𝑌) + (𝑏 · 𝑍))) ∧ (𝑑 ∈ 𝐵 ∧ 𝑒 ∈ 𝐵) ∧ 𝑗 = ((𝑑 · (𝑋 − 𝑌)) + (𝑒 · (𝑋 − 𝑍)))) → 𝑏 ∈ 𝐵)
55		simp2l 1195	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ (𝑎 ∈ 𝐵 ∧ 𝑏 ∈ 𝐵) ∧ 𝑗 = ((𝑎 · 𝑌) + (𝑏 · 𝑍))) ∧ (𝑑 ∈ 𝐵 ∧ 𝑒 ∈ 𝐵) ∧ 𝑗 = ((𝑑 · (𝑋 − 𝑌)) + (𝑒 · (𝑋 − 𝑍)))) → 𝑑 ∈ 𝐵)
56		simp2r 1196	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ (𝑎 ∈ 𝐵 ∧ 𝑏 ∈ 𝐵) ∧ 𝑗 = ((𝑎 · 𝑌) + (𝑏 · 𝑍))) ∧ (𝑑 ∈ 𝐵 ∧ 𝑒 ∈ 𝐵) ∧ 𝑗 = ((𝑑 · (𝑋 − 𝑌)) + (𝑒 · (𝑋 − 𝑍)))) → 𝑒 ∈ 𝐵)
57		simp13 1201	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ (𝑎 ∈ 𝐵 ∧ 𝑏 ∈ 𝐵) ∧ 𝑗 = ((𝑎 · 𝑌) + (𝑏 · 𝑍))) ∧ (𝑑 ∈ 𝐵 ∧ 𝑒 ∈ 𝐵) ∧ 𝑗 = ((𝑑 · (𝑋 − 𝑌)) + (𝑒 · (𝑋 − 𝑍)))) → 𝑗 = ((𝑎 · 𝑌) + (𝑏 · 𝑍)))
58		simp3 1134	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ (𝑎 ∈ 𝐵 ∧ 𝑏 ∈ 𝐵) ∧ 𝑗 = ((𝑎 · 𝑌) + (𝑏 · 𝑍))) ∧ (𝑑 ∈ 𝐵 ∧ 𝑒 ∈ 𝐵) ∧ 𝑗 = ((𝑑 · (𝑋 − 𝑌)) + (𝑒 · (𝑋 − 𝑍)))) → 𝑗 = ((𝑑 · (𝑋 − 𝑌)) + (𝑒 · (𝑋 − 𝑍))))
59	8, 9, 39, 10, 11, 41, 42, 44, 46, 47, 48, 31, 34, 32, 33, 49, 50, 51, 52, 53, 54, 55, 56, 57, 58	baerlem3lem1 38837	. . . . . . . . . 10 ⊢ (((𝜑 ∧ (𝑎 ∈ 𝐵 ∧ 𝑏 ∈ 𝐵) ∧ 𝑗 = ((𝑎 · 𝑌) + (𝑏 · 𝑍))) ∧ (𝑑 ∈ 𝐵 ∧ 𝑒 ∈ 𝐵) ∧ 𝑗 = ((𝑑 · (𝑋 − 𝑌)) + (𝑒 · (𝑋 − 𝑍)))) → 𝑗 = (𝑎 · (𝑌 − 𝑍)))
60	40, 3	syl 17	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ (𝑎 ∈ 𝐵 ∧ 𝑏 ∈ 𝐵) ∧ 𝑗 = ((𝑎 · 𝑌) + (𝑏 · 𝑍))) ∧ (𝑑 ∈ 𝐵 ∧ 𝑒 ∈ 𝐵) ∧ 𝑗 = ((𝑑 · (𝑋 − 𝑌)) + (𝑒 · (𝑋 − 𝑍)))) → 𝑊 ∈ LMod)
61	8, 9	lmodvsubcl 19673	. . . . . . . . . . . . 13 ⊢ ((𝑊 ∈ LMod ∧ 𝑌 ∈ 𝑉 ∧ 𝑍 ∈ 𝑉) → (𝑌 − 𝑍) ∈ 𝑉)
62	3, 5, 7, 61	syl3anc 1367	. . . . . . . . . . . 12 ⊢ (𝜑 → (𝑌 − 𝑍) ∈ 𝑉)
63	40, 62	syl 17	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ (𝑎 ∈ 𝐵 ∧ 𝑏 ∈ 𝐵) ∧ 𝑗 = ((𝑎 · 𝑌) + (𝑏 · 𝑍))) ∧ (𝑑 ∈ 𝐵 ∧ 𝑒 ∈ 𝐵) ∧ 𝑗 = ((𝑑 · (𝑋 − 𝑌)) + (𝑒 · (𝑋 − 𝑍)))) → (𝑌 − 𝑍) ∈ 𝑉)
64	8, 34, 32, 33, 11, 60, 53, 63	lspsneli 19767	. . . . . . . . . 10 ⊢ (((𝜑 ∧ (𝑎 ∈ 𝐵 ∧ 𝑏 ∈ 𝐵) ∧ 𝑗 = ((𝑎 · 𝑌) + (𝑏 · 𝑍))) ∧ (𝑑 ∈ 𝐵 ∧ 𝑒 ∈ 𝐵) ∧ 𝑗 = ((𝑑 · (𝑋 − 𝑌)) + (𝑒 · (𝑋 − 𝑍)))) → (𝑎 · (𝑌 − 𝑍)) ∈ (𝑁‘{(𝑌 − 𝑍)}))
65	59, 64	eqeltrd 2913	. . . . . . . . 9 ⊢ (((𝜑 ∧ (𝑎 ∈ 𝐵 ∧ 𝑏 ∈ 𝐵) ∧ 𝑗 = ((𝑎 · 𝑌) + (𝑏 · 𝑍))) ∧ (𝑑 ∈ 𝐵 ∧ 𝑒 ∈ 𝐵) ∧ 𝑗 = ((𝑑 · (𝑋 − 𝑌)) + (𝑒 · (𝑋 − 𝑍)))) → 𝑗 ∈ (𝑁‘{(𝑌 − 𝑍)}))
66	65	3exp 1115	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑎 ∈ 𝐵 ∧ 𝑏 ∈ 𝐵) ∧ 𝑗 = ((𝑎 · 𝑌) + (𝑏 · 𝑍))) → ((𝑑 ∈ 𝐵 ∧ 𝑒 ∈ 𝐵) → (𝑗 = ((𝑑 · (𝑋 − 𝑌)) + (𝑒 · (𝑋 − 𝑍))) → 𝑗 ∈ (𝑁‘{(𝑌 − 𝑍)}))))
67	66	rexlimdvv 3293	. . . . . . 7 ⊢ ((𝜑 ∧ (𝑎 ∈ 𝐵 ∧ 𝑏 ∈ 𝐵) ∧ 𝑗 = ((𝑎 · 𝑌) + (𝑏 · 𝑍))) → (∃𝑑 ∈ 𝐵 ∃𝑒 ∈ 𝐵 𝑗 = ((𝑑 · (𝑋 − 𝑌)) + (𝑒 · (𝑋 − 𝑍))) → 𝑗 ∈ (𝑁‘{(𝑌 − 𝑍)})))
68	67	3exp 1115	. . . . . 6 ⊢ (𝜑 → ((𝑎 ∈ 𝐵 ∧ 𝑏 ∈ 𝐵) → (𝑗 = ((𝑎 · 𝑌) + (𝑏 · 𝑍)) → (∃𝑑 ∈ 𝐵 ∃𝑒 ∈ 𝐵 𝑗 = ((𝑑 · (𝑋 − 𝑌)) + (𝑒 · (𝑋 − 𝑍))) → 𝑗 ∈ (𝑁‘{(𝑌 − 𝑍)})))))
69	68	rexlimdvv 3293	. . . . 5 ⊢ (𝜑 → (∃𝑎 ∈ 𝐵 ∃𝑏 ∈ 𝐵 𝑗 = ((𝑎 · 𝑌) + (𝑏 · 𝑍)) → (∃𝑑 ∈ 𝐵 ∃𝑒 ∈ 𝐵 𝑗 = ((𝑑 · (𝑋 − 𝑌)) + (𝑒 · (𝑋 − 𝑍))) → 𝑗 ∈ (𝑁‘{(𝑌 − 𝑍)}))))
70	69	impd 413	. . . 4 ⊢ (𝜑 → ((∃𝑎 ∈ 𝐵 ∃𝑏 ∈ 𝐵 𝑗 = ((𝑎 · 𝑌) + (𝑏 · 𝑍)) ∧ ∃𝑑 ∈ 𝐵 ∃𝑒 ∈ 𝐵 𝑗 = ((𝑑 · (𝑋 − 𝑌)) + (𝑒 · (𝑋 − 𝑍)))) → 𝑗 ∈ (𝑁‘{(𝑌 − 𝑍)})))
71	38, 70	sylbid 242	. . 3 ⊢ (𝜑 → (𝑗 ∈ (((𝑁‘{𝑌}) ⊕ (𝑁‘{𝑍})) ∩ ((𝑁‘{(𝑋 − 𝑌)}) ⊕ (𝑁‘{(𝑋 − 𝑍)}))) → 𝑗 ∈ (𝑁‘{(𝑌 − 𝑍)})))
72	71	ssrdv 3973	. 2 ⊢ (𝜑 → (((𝑁‘{𝑌}) ⊕ (𝑁‘{𝑍})) ∩ ((𝑁‘{(𝑋 − 𝑌)}) ⊕ (𝑁‘{(𝑋 − 𝑍)}))) ⊆ (𝑁‘{(𝑌 − 𝑍)}))
73	29, 72	eqssd 3984	1 ⊢ (𝜑 → (𝑁‘{(𝑌 − 𝑍)}) = (((𝑁‘{𝑌}) ⊕ (𝑁‘{𝑍})) ∩ ((𝑁‘{(𝑋 − 𝑌)}) ⊕ (𝑁‘{(𝑋 − 𝑍)}))))

Syntax hints:  ¬ wn 3   → wi 4   ∧ wa 398   ∧ w3a 1083   = wceq 1533   ∈ wcel 2110   ≠ wne 3016  ∃wrex 3139   ∖ cdif 3933   ∩ cin 3935   ⊆ wss 3936  {csn 4561  {cpr 4563  ‘cfv 6350  (class class class)co 7150  Basecbs 16477  +_gcplusg 16559  Scalarcsca 16562   ·_𝑠 cvsca 16563  0_gc0g 16707  inv_gcminusg 18098  -_gcsg 18099  LSSumclsm 18753  Abelcabl 18901  LModclmod 19628  LSpanclspn 19737  LVecclvec 19868

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1792  ax-4 1806  ax-5 1907  ax-6 1966  ax-7 2011  ax-8 2112  ax-9 2120  ax-10 2141  ax-11 2156  ax-12 2172  ax-ext 2793  ax-rep 5183  ax-sep 5196  ax-nul 5203  ax-pow 5259  ax-pr 5322  ax-un 7455  ax-cnex 10587  ax-resscn 10588  ax-1cn 10589  ax-icn 10590  ax-addcl 10591  ax-addrcl 10592  ax-mulcl 10593  ax-mulrcl 10594  ax-mulcom 10595  ax-addass 10596  ax-mulass 10597  ax-distr 10598  ax-i2m1 10599  ax-1ne0 10600  ax-1rid 10601  ax-rnegex 10602  ax-rrecex 10603  ax-cnre 10604  ax-pre-lttri 10605  ax-pre-lttrn 10606  ax-pre-ltadd 10607  ax-pre-mulgt0 10608

This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-3or 1084  df-3an 1085  df-tru 1536  df-ex 1777  df-nf 1781  df-sb 2066  df-mo 2618  df-eu 2650  df-clab 2800  df-cleq 2814  df-clel 2893  df-nfc 2963  df-ne 3017  df-nel 3124  df-ral 3143  df-rex 3144  df-reu 3145  df-rmo 3146  df-rab 3147  df-v 3497  df-sbc 3773  df-csb 3884  df-dif 3939  df-un 3941  df-in 3943  df-ss 3952  df-pss 3954  df-nul 4292  df-if 4468  df-pw 4541  df-sn 4562  df-pr 4564  df-tp 4566  df-op 4568  df-uni 4833  df-int 4870  df-iun 4914  df-br 5060  df-opab 5122  df-mpt 5140  df-tr 5166  df-id 5455  df-eprel 5460  df-po 5469  df-so 5470  df-fr 5509  df-we 5511  df-xp 5556  df-rel 5557  df-cnv 5558  df-co 5559  df-dm 5560  df-rn 5561  df-res 5562  df-ima 5563  df-pred 6143  df-ord 6189  df-on 6190  df-lim 6191  df-suc 6192  df-iota 6309  df-fun 6352  df-fn 6353  df-f 6354  df-f1 6355  df-fo 6356  df-f1o 6357  df-fv 6358  df-riota 7108  df-ov 7153  df-oprab 7154  df-mpo 7155  df-om 7575  df-1st 7683  df-2nd 7684  df-tpos 7886  df-wrecs 7941  df-recs 8002  df-rdg 8040  df-er 8283  df-en 8504  df-dom 8505  df-sdom 8506  df-pnf 10671  df-mnf 10672  df-xr 10673  df-ltxr 10674  df-le 10675  df-sub 10866  df-neg 10867  df-nn 11633  df-2 11694  df-3 11695  df-ndx 16480  df-slot 16481  df-base 16483  df-sets 16484  df-ress 16485  df-plusg 16572  df-mulr 16573  df-0g 16709  df-mgm 17846  df-sgrp 17895  df-mnd 17906  df-submnd 17951  df-grp 18100  df-minusg 18101  df-sbg 18102  df-subg 18270  df-cntz 18441  df-lsm 18755  df-cmn 18902  df-abl 18903  df-mgp 19234  df-ur 19246  df-ring 19293  df-oppr 19367  df-dvdsr 19385  df-unit 19386  df-invr 19416  df-drng 19498  df-lmod 19630  df-lss 19698  df-lsp 19738  df-lvec 19869

This theorem is referenced by:  baerlem3  38843