Theorem baerlem3lem2

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

	Ref	Expression
Hypotheses	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	baerlem3lem2	⊢ ( 𝜑 → ( 𝑁 ‘ { ( 𝑌 − 𝑍 ) } ) = ( ( ( 𝑁 ‘ { 𝑌 } ) ⊕ ( 𝑁 ‘ { 𝑍 } ) ) ∩ ( ( 𝑁 ‘ { ( 𝑋 − 𝑌 ) } ) ⊕ ( 𝑁 ‘ { ( 𝑋 − 𝑍 ) } ) ) ) )

Proof

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