Metamath Proof Explorer

Theorem baerlem5blem2

Description: Lemma for baerlem5b . (Contributed by NM, 13-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 baerlem5blem2 ( 𝜑 → ( 𝑁 ‘ { ( 𝑌 + 𝑍 ) } ) = ( ( ( 𝑁 ‘ { 𝑌 } ) ⊕ ( 𝑁 ‘ { 𝑍 } ) ) ∩ ( ( 𝑁 ‘ { ( 𝑋 − ( 𝑌 + 𝑍 ) ) } ) ⊕ ( 𝑁 ‘ { 𝑋 } ) ) ) )

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 12 5 4 lspsntri ⊢ ( ( 𝑊 ∈ LMod ∧ 𝑌 ∈ 𝑉 ∧ 𝑍 ∈ 𝑉 ) → ( 𝑁 ‘ { ( 𝑌 + 𝑍 ) } ) ⊆ ( ( 𝑁 ‘ { 𝑌 } ) ⊕ ( 𝑁 ‘ { 𝑍 } ) ) )
25 21 22 23 24 syl3anc ⊢ ( 𝜑 → ( 𝑁 ‘ { ( 𝑌 + 𝑍 ) } ) ⊆ ( ( 𝑁 ‘ { 𝑌 } ) ⊕ ( 𝑁 ‘ { 𝑍 } ) ) )
26 1 12 lmodvacl ⊢ ( ( 𝑊 ∈ LMod ∧ 𝑌 ∈ 𝑉 ∧ 𝑍 ∈ 𝑉 ) → ( 𝑌 + 𝑍 ) ∈ 𝑉 )
27 21 22 23 26 syl3anc ⊢ ( 𝜑 → ( 𝑌 + 𝑍 ) ∈ 𝑉 )
28 1 2 lmodvsubcl ⊢ ( ( 𝑊 ∈ LMod ∧ 𝑋 ∈ 𝑉 ∧ ( 𝑌 + 𝑍 ) ∈ 𝑉 ) → ( 𝑋 − ( 𝑌 + 𝑍 ) ) ∈ 𝑉 )
29 21 7 27 28 syl3anc ⊢ ( 𝜑 → ( 𝑋 − ( 𝑌 + 𝑍 ) ) ∈ 𝑉 )
30 1 2 5 21 29 7 lspsnsub ⊢ ( 𝜑 → ( 𝑁 ‘ { ( ( 𝑋 − ( 𝑌 + 𝑍 ) ) − 𝑋 ) } ) = ( 𝑁 ‘ { ( 𝑋 − ( 𝑋 − ( 𝑌 + 𝑍 ) ) ) } ) )
31 lmodabl ⊢ ( 𝑊 ∈ LMod → 𝑊 ∈ Abel )
32 21 31 syl ⊢ ( 𝜑 → 𝑊 ∈ Abel )
33 1 2 32 7 27 ablnncan ⊢ ( 𝜑 → ( 𝑋 − ( 𝑋 − ( 𝑌 + 𝑍 ) ) ) = ( 𝑌 + 𝑍 ) )
34 33 sneqd ⊢ ( 𝜑 → { ( 𝑋 − ( 𝑋 − ( 𝑌 + 𝑍 ) ) ) } = { ( 𝑌 + 𝑍 ) } )
35 34 fveq2d ⊢ ( 𝜑 → ( 𝑁 ‘ { ( 𝑋 − ( 𝑋 − ( 𝑌 + 𝑍 ) ) ) } ) = ( 𝑁 ‘ { ( 𝑌 + 𝑍 ) } ) )
36 30 35 eqtrd ⊢ ( 𝜑 → ( 𝑁 ‘ { ( ( 𝑋 − ( 𝑌 + 𝑍 ) ) − 𝑋 ) } ) = ( 𝑁 ‘ { ( 𝑌 + 𝑍 ) } ) )
37 1 2 4 5 lspsntrim ⊢ ( ( 𝑊 ∈ LMod ∧ ( 𝑋 − ( 𝑌 + 𝑍 ) ) ∈ 𝑉 ∧ 𝑋 ∈ 𝑉 ) → ( 𝑁 ‘ { ( ( 𝑋 − ( 𝑌 + 𝑍 ) ) − 𝑋 ) } ) ⊆ ( ( 𝑁 ‘ { ( 𝑋 − ( 𝑌 + 𝑍 ) ) } ) ⊕ ( 𝑁 ‘ { 𝑋 } ) ) )
38 21 29 7 37 syl3anc ⊢ ( 𝜑 → ( 𝑁 ‘ { ( ( 𝑋 − ( 𝑌 + 𝑍 ) ) − 𝑋 ) } ) ⊆ ( ( 𝑁 ‘ { ( 𝑋 − ( 𝑌 + 𝑍 ) ) } ) ⊕ ( 𝑁 ‘ { 𝑋 } ) ) )
39 36 38 eqsstrrd ⊢ ( 𝜑 → ( 𝑁 ‘ { ( 𝑌 + 𝑍 ) } ) ⊆ ( ( 𝑁 ‘ { ( 𝑋 − ( 𝑌 + 𝑍 ) ) } ) ⊕ ( 𝑁 ‘ { 𝑋 } ) ) )
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 29 7 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 baerlem5blem1 ⊢ ( ( ( 𝜑 ∧ ( 𝑎 ∈ 𝐵 ∧ 𝑏 ∈ 𝐵 ) ∧ 𝑗 = ( ( 𝑎 · 𝑌 ) + ( 𝑏 · 𝑍 ) ) ) ∧ ( 𝑑 ∈ 𝐵 ∧ 𝑒 ∈ 𝐵 ) ∧ 𝑗 = ( ( 𝑑 · ( 𝑋 − ( 𝑌 + 𝑍 ) ) ) + ( 𝑒 · 𝑋 ) ) ) → 𝑗 = ( ( 𝐼 ‘ 𝑑 ) · ( 𝑌 + 𝑍 ) ) )
60 46 21 syl ⊢ ( ( ( 𝜑 ∧ ( 𝑎 ∈ 𝐵 ∧ 𝑏 ∈ 𝐵 ) ∧ 𝑗 = ( ( 𝑎 · 𝑌 ) + ( 𝑏 · 𝑍 ) ) ) ∧ ( 𝑑 ∈ 𝐵 ∧ 𝑒 ∈ 𝐵 ) ∧ 𝑗 = ( ( 𝑑 · ( 𝑋 − ( 𝑌 + 𝑍 ) ) ) + ( 𝑒 · 𝑋 ) ) ) → 𝑊 ∈ LMod )
61 14 lmodring ⊢ ( 𝑊 ∈ LMod → 𝑅 ∈ Ring )
62 ringgrp ⊢ ( 𝑅 ∈ Ring → 𝑅 ∈ Grp )
63 46 21 61 62 4syl ⊢ ( ( ( 𝜑 ∧ ( 𝑎 ∈ 𝐵 ∧ 𝑏 ∈ 𝐵 ) ∧ 𝑗 = ( ( 𝑎 · 𝑌 ) + ( 𝑏 · 𝑍 ) ) ) ∧ ( 𝑑 ∈ 𝐵 ∧ 𝑒 ∈ 𝐵 ) ∧ 𝑗 = ( ( 𝑑 · ( 𝑋 − ( 𝑌 + 𝑍 ) ) ) + ( 𝑒 · 𝑋 ) ) ) → 𝑅 ∈ Grp )
64 15 19 grpinvcl ⊢ ( ( 𝑅 ∈ Grp ∧ 𝑑 ∈ 𝐵 ) → ( 𝐼 ‘ 𝑑 ) ∈ 𝐵 )
65 63 55 64 syl2anc ⊢ ( ( ( 𝜑 ∧ ( 𝑎 ∈ 𝐵 ∧ 𝑏 ∈ 𝐵 ) ∧ 𝑗 = ( ( 𝑎 · 𝑌 ) + ( 𝑏 · 𝑍 ) ) ) ∧ ( 𝑑 ∈ 𝐵 ∧ 𝑒 ∈ 𝐵 ) ∧ 𝑗 = ( ( 𝑑 · ( 𝑋 − ( 𝑌 + 𝑍 ) ) ) + ( 𝑒 · 𝑋 ) ) ) → ( 𝐼 ‘ 𝑑 ) ∈ 𝐵 )
66 46 27 syl ⊢ ( ( ( 𝜑 ∧ ( 𝑎 ∈ 𝐵 ∧ 𝑏 ∈ 𝐵 ) ∧ 𝑗 = ( ( 𝑎 · 𝑌 ) + ( 𝑏 · 𝑍 ) ) ) ∧ ( 𝑑 ∈ 𝐵 ∧ 𝑒 ∈ 𝐵 ) ∧ 𝑗 = ( ( 𝑑 · ( 𝑋 − ( 𝑌 + 𝑍 ) ) ) + ( 𝑒 · 𝑋 ) ) ) → ( 𝑌 + 𝑍 ) ∈ 𝑉 )
67 1 13 14 15 5 60 65 66 ellspsni ⊢ ( ( ( 𝜑 ∧ ( 𝑎 ∈ 𝐵 ∧ 𝑏 ∈ 𝐵 ) ∧ 𝑗 = ( ( 𝑎 · 𝑌 ) + ( 𝑏 · 𝑍 ) ) ) ∧ ( 𝑑 ∈ 𝐵 ∧ 𝑒 ∈ 𝐵 ) ∧ 𝑗 = ( ( 𝑑 · ( 𝑋 − ( 𝑌 + 𝑍 ) ) ) + ( 𝑒 · 𝑋 ) ) ) → ( ( 𝐼 ‘ 𝑑 ) · ( 𝑌 + 𝑍 ) ) ∈ ( 𝑁 ‘ { ( 𝑌 + 𝑍 ) } ) )
68 59 67 eqeltrd ⊢ ( ( ( 𝜑 ∧ ( 𝑎 ∈ 𝐵 ∧ 𝑏 ∈ 𝐵 ) ∧ 𝑗 = ( ( 𝑎 · 𝑌 ) + ( 𝑏 · 𝑍 ) ) ) ∧ ( 𝑑 ∈ 𝐵 ∧ 𝑒 ∈ 𝐵 ) ∧ 𝑗 = ( ( 𝑑 · ( 𝑋 − ( 𝑌 + 𝑍 ) ) ) + ( 𝑒 · 𝑋 ) ) ) → 𝑗 ∈ ( 𝑁 ‘ { ( 𝑌 + 𝑍 ) } ) )
69 68 3exp ⊢ ( ( 𝜑 ∧ ( 𝑎 ∈ 𝐵 ∧ 𝑏 ∈ 𝐵 ) ∧ 𝑗 = ( ( 𝑎 · 𝑌 ) + ( 𝑏 · 𝑍 ) ) ) → ( ( 𝑑 ∈ 𝐵 ∧ 𝑒 ∈ 𝐵 ) → ( 𝑗 = ( ( 𝑑 · ( 𝑋 − ( 𝑌 + 𝑍 ) ) ) + ( 𝑒 · 𝑋 ) ) → 𝑗 ∈ ( 𝑁 ‘ { ( 𝑌 + 𝑍 ) } ) ) ) )
70 69 rexlimdvv ⊢ ( ( 𝜑 ∧ ( 𝑎 ∈ 𝐵 ∧ 𝑏 ∈ 𝐵 ) ∧ 𝑗 = ( ( 𝑎 · 𝑌 ) + ( 𝑏 · 𝑍 ) ) ) → ( ∃ 𝑑 ∈ 𝐵 ∃ 𝑒 ∈ 𝐵 𝑗 = ( ( 𝑑 · ( 𝑋 − ( 𝑌 + 𝑍 ) ) ) + ( 𝑒 · 𝑋 ) ) → 𝑗 ∈ ( 𝑁 ‘ { ( 𝑌 + 𝑍 ) } ) ) )
71 70 3exp ⊢ ( 𝜑 → ( ( 𝑎 ∈ 𝐵 ∧ 𝑏 ∈ 𝐵 ) → ( 𝑗 = ( ( 𝑎 · 𝑌 ) + ( 𝑏 · 𝑍 ) ) → ( ∃ 𝑑 ∈ 𝐵 ∃ 𝑒 ∈ 𝐵 𝑗 = ( ( 𝑑 · ( 𝑋 − ( 𝑌 + 𝑍 ) ) ) + ( 𝑒 · 𝑋 ) ) → 𝑗 ∈ ( 𝑁 ‘ { ( 𝑌 + 𝑍 ) } ) ) ) ) )
72 71 rexlimdvv ⊢ ( 𝜑 → ( ∃ 𝑎 ∈ 𝐵 ∃ 𝑏 ∈ 𝐵 𝑗 = ( ( 𝑎 · 𝑌 ) + ( 𝑏 · 𝑍 ) ) → ( ∃ 𝑑 ∈ 𝐵 ∃ 𝑒 ∈ 𝐵 𝑗 = ( ( 𝑑 · ( 𝑋 − ( 𝑌 + 𝑍 ) ) ) + ( 𝑒 · 𝑋 ) ) → 𝑗 ∈ ( 𝑁 ‘ { ( 𝑌 + 𝑍 ) } ) ) ) )
73 72 impd ⊢ ( 𝜑 → ( ( ∃ 𝑎 ∈ 𝐵 ∃ 𝑏 ∈ 𝐵 𝑗 = ( ( 𝑎 · 𝑌 ) + ( 𝑏 · 𝑍 ) ) ∧ ∃ 𝑑 ∈ 𝐵 ∃ 𝑒 ∈ 𝐵 𝑗 = ( ( 𝑑 · ( 𝑋 − ( 𝑌 + 𝑍 ) ) ) + ( 𝑒 · 𝑋 ) ) ) → 𝑗 ∈ ( 𝑁 ‘ { ( 𝑌 + 𝑍 ) } ) ) )
74 45 73 sylbid ⊢ ( 𝜑 → ( 𝑗 ∈ ( ( ( 𝑁 ‘ { 𝑌 } ) ⊕ ( 𝑁 ‘ { 𝑍 } ) ) ∩ ( ( 𝑁 ‘ { ( 𝑋 − ( 𝑌 + 𝑍 ) ) } ) ⊕ ( 𝑁 ‘ { 𝑋 } ) ) ) → 𝑗 ∈ ( 𝑁 ‘ { ( 𝑌 + 𝑍 ) } ) ) )
75 74 ssrdv ⊢ ( 𝜑 → ( ( ( 𝑁 ‘ { 𝑌 } ) ⊕ ( 𝑁 ‘ { 𝑍 } ) ) ∩ ( ( 𝑁 ‘ { ( 𝑋 − ( 𝑌 + 𝑍 ) ) } ) ⊕ ( 𝑁 ‘ { 𝑋 } ) ) ) ⊆ ( 𝑁 ‘ { ( 𝑌 + 𝑍 ) } ) )
76 40 75 eqssd ⊢ ( 𝜑 → ( 𝑁 ‘ { ( 𝑌 + 𝑍 ) } ) = ( ( ( 𝑁 ‘ { 𝑌 } ) ⊕ ( 𝑁 ‘ { 𝑍 } ) ) ∩ ( ( 𝑁 ‘ { ( 𝑋 − ( 𝑌 + 𝑍 ) ) } ) ⊕ ( 𝑁 ‘ { 𝑋 } ) ) ) )