Metamath Proof Explorer


Theorem baerlem5alem2

Description: Lemma for baerlem5a . (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 baerlem5alem2 ( 𝜑 → ( 𝑁 ‘ { ( 𝑋 ( 𝑌 + 𝑍 ) ) } ) = ( ( ( 𝑁 ‘ { ( 𝑋 𝑌 ) } ) ( 𝑁 ‘ { 𝑍 } ) ) ∩ ( ( 𝑁 ‘ { ( 𝑋 𝑍 ) } ) ( 𝑁 ‘ { 𝑌 } ) ) ) )

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 lmodabl ( 𝑊 ∈ LMod → 𝑊 ∈ Abel )
23 21 22 syl ( 𝜑𝑊 ∈ Abel )
24 10 eldifad ( 𝜑𝑌𝑉 )
25 11 eldifad ( 𝜑𝑍𝑉 )
26 1 12 2 23 7 24 25 ablsubsub4 ( 𝜑 → ( ( 𝑋 𝑌 ) 𝑍 ) = ( 𝑋 ( 𝑌 + 𝑍 ) ) )
27 26 sneqd ( 𝜑 → { ( ( 𝑋 𝑌 ) 𝑍 ) } = { ( 𝑋 ( 𝑌 + 𝑍 ) ) } )
28 27 fveq2d ( 𝜑 → ( 𝑁 ‘ { ( ( 𝑋 𝑌 ) 𝑍 ) } ) = ( 𝑁 ‘ { ( 𝑋 ( 𝑌 + 𝑍 ) ) } ) )
29 1 2 lmodvsubcl ( ( 𝑊 ∈ LMod ∧ 𝑋𝑉𝑌𝑉 ) → ( 𝑋 𝑌 ) ∈ 𝑉 )
30 21 7 24 29 syl3anc ( 𝜑 → ( 𝑋 𝑌 ) ∈ 𝑉 )
31 1 2 4 5 lspsntrim ( ( 𝑊 ∈ LMod ∧ ( 𝑋 𝑌 ) ∈ 𝑉𝑍𝑉 ) → ( 𝑁 ‘ { ( ( 𝑋 𝑌 ) 𝑍 ) } ) ⊆ ( ( 𝑁 ‘ { ( 𝑋 𝑌 ) } ) ( 𝑁 ‘ { 𝑍 } ) ) )
32 21 30 25 31 syl3anc ( 𝜑 → ( 𝑁 ‘ { ( ( 𝑋 𝑌 ) 𝑍 ) } ) ⊆ ( ( 𝑁 ‘ { ( 𝑋 𝑌 ) } ) ( 𝑁 ‘ { 𝑍 } ) ) )
33 28 32 eqsstrrd ( 𝜑 → ( 𝑁 ‘ { ( 𝑋 ( 𝑌 + 𝑍 ) ) } ) ⊆ ( ( 𝑁 ‘ { ( 𝑋 𝑌 ) } ) ( 𝑁 ‘ { 𝑍 } ) ) )
34 1 2 23 7 25 24 ablsub32 ( 𝜑 → ( ( 𝑋 𝑍 ) 𝑌 ) = ( ( 𝑋 𝑌 ) 𝑍 ) )
35 34 26 eqtrd ( 𝜑 → ( ( 𝑋 𝑍 ) 𝑌 ) = ( 𝑋 ( 𝑌 + 𝑍 ) ) )
36 35 sneqd ( 𝜑 → { ( ( 𝑋 𝑍 ) 𝑌 ) } = { ( 𝑋 ( 𝑌 + 𝑍 ) ) } )
37 36 fveq2d ( 𝜑 → ( 𝑁 ‘ { ( ( 𝑋 𝑍 ) 𝑌 ) } ) = ( 𝑁 ‘ { ( 𝑋 ( 𝑌 + 𝑍 ) ) } ) )
38 1 2 lmodvsubcl ( ( 𝑊 ∈ LMod ∧ 𝑋𝑉𝑍𝑉 ) → ( 𝑋 𝑍 ) ∈ 𝑉 )
39 21 7 25 38 syl3anc ( 𝜑 → ( 𝑋 𝑍 ) ∈ 𝑉 )
40 1 2 4 5 lspsntrim ( ( 𝑊 ∈ LMod ∧ ( 𝑋 𝑍 ) ∈ 𝑉𝑌𝑉 ) → ( 𝑁 ‘ { ( ( 𝑋 𝑍 ) 𝑌 ) } ) ⊆ ( ( 𝑁 ‘ { ( 𝑋 𝑍 ) } ) ( 𝑁 ‘ { 𝑌 } ) ) )
41 21 39 24 40 syl3anc ( 𝜑 → ( 𝑁 ‘ { ( ( 𝑋 𝑍 ) 𝑌 ) } ) ⊆ ( ( 𝑁 ‘ { ( 𝑋 𝑍 ) } ) ( 𝑁 ‘ { 𝑌 } ) ) )
42 37 41 eqsstrrd ( 𝜑 → ( 𝑁 ‘ { ( 𝑋 ( 𝑌 + 𝑍 ) ) } ) ⊆ ( ( 𝑁 ‘ { ( 𝑋 𝑍 ) } ) ( 𝑁 ‘ { 𝑌 } ) ) )
43 33 42 ssind ( 𝜑 → ( 𝑁 ‘ { ( 𝑋 ( 𝑌 + 𝑍 ) ) } ) ⊆ ( ( ( 𝑁 ‘ { ( 𝑋 𝑌 ) } ) ( 𝑁 ‘ { 𝑍 } ) ) ∩ ( ( 𝑁 ‘ { ( 𝑋 𝑍 ) } ) ( 𝑁 ‘ { 𝑌 } ) ) ) )
44 elin ( 𝑗 ∈ ( ( ( 𝑁 ‘ { ( 𝑋 𝑌 ) } ) ( 𝑁 ‘ { 𝑍 } ) ) ∩ ( ( 𝑁 ‘ { ( 𝑋 𝑍 ) } ) ( 𝑁 ‘ { 𝑌 } ) ) ) ↔ ( 𝑗 ∈ ( ( 𝑁 ‘ { ( 𝑋 𝑌 ) } ) ( 𝑁 ‘ { 𝑍 } ) ) ∧ 𝑗 ∈ ( ( 𝑁 ‘ { ( 𝑋 𝑍 ) } ) ( 𝑁 ‘ { 𝑌 } ) ) ) )
45 1 12 14 15 13 4 5 21 30 25 lsmspsn ( 𝜑 → ( 𝑗 ∈ ( ( 𝑁 ‘ { ( 𝑋 𝑌 ) } ) ( 𝑁 ‘ { 𝑍 } ) ) ↔ ∃ 𝑎𝐵𝑏𝐵 𝑗 = ( ( 𝑎 · ( 𝑋 𝑌 ) ) + ( 𝑏 · 𝑍 ) ) ) )
46 1 12 14 15 13 4 5 21 39 24 lsmspsn ( 𝜑 → ( 𝑗 ∈ ( ( 𝑁 ‘ { ( 𝑋 𝑍 ) } ) ( 𝑁 ‘ { 𝑌 } ) ) ↔ ∃ 𝑑𝐵𝑒𝐵 𝑗 = ( ( 𝑑 · ( 𝑋 𝑍 ) ) + ( 𝑒 · 𝑌 ) ) ) )
47 45 46 anbi12d ( 𝜑 → ( ( 𝑗 ∈ ( ( 𝑁 ‘ { ( 𝑋 𝑌 ) } ) ( 𝑁 ‘ { 𝑍 } ) ) ∧ 𝑗 ∈ ( ( 𝑁 ‘ { ( 𝑋 𝑍 ) } ) ( 𝑁 ‘ { 𝑌 } ) ) ) ↔ ( ∃ 𝑎𝐵𝑏𝐵 𝑗 = ( ( 𝑎 · ( 𝑋 𝑌 ) ) + ( 𝑏 · 𝑍 ) ) ∧ ∃ 𝑑𝐵𝑒𝐵 𝑗 = ( ( 𝑑 · ( 𝑋 𝑍 ) ) + ( 𝑒 · 𝑌 ) ) ) ) )
48 44 47 syl5bb ( 𝜑 → ( 𝑗 ∈ ( ( ( 𝑁 ‘ { ( 𝑋 𝑌 ) } ) ( 𝑁 ‘ { 𝑍 } ) ) ∩ ( ( 𝑁 ‘ { ( 𝑋 𝑍 ) } ) ( 𝑁 ‘ { 𝑌 } ) ) ) ↔ ( ∃ 𝑎𝐵𝑏𝐵 𝑗 = ( ( 𝑎 · ( 𝑋 𝑌 ) ) + ( 𝑏 · 𝑍 ) ) ∧ ∃ 𝑑𝐵𝑒𝐵 𝑗 = ( ( 𝑑 · ( 𝑋 𝑍 ) ) + ( 𝑒 · 𝑌 ) ) ) ) )
49 simp11 ( ( ( 𝜑 ∧ ( 𝑎𝐵𝑏𝐵 ) ∧ 𝑗 = ( ( 𝑎 · ( 𝑋 𝑌 ) ) + ( 𝑏 · 𝑍 ) ) ) ∧ ( 𝑑𝐵𝑒𝐵 ) ∧ 𝑗 = ( ( 𝑑 · ( 𝑋 𝑍 ) ) + ( 𝑒 · 𝑌 ) ) ) → 𝜑 )
50 49 6 syl ( ( ( 𝜑 ∧ ( 𝑎𝐵𝑏𝐵 ) ∧ 𝑗 = ( ( 𝑎 · ( 𝑋 𝑌 ) ) + ( 𝑏 · 𝑍 ) ) ) ∧ ( 𝑑𝐵𝑒𝐵 ) ∧ 𝑗 = ( ( 𝑑 · ( 𝑋 𝑍 ) ) + ( 𝑒 · 𝑌 ) ) ) → 𝑊 ∈ LVec )
51 49 7 syl ( ( ( 𝜑 ∧ ( 𝑎𝐵𝑏𝐵 ) ∧ 𝑗 = ( ( 𝑎 · ( 𝑋 𝑌 ) ) + ( 𝑏 · 𝑍 ) ) ) ∧ ( 𝑑𝐵𝑒𝐵 ) ∧ 𝑗 = ( ( 𝑑 · ( 𝑋 𝑍 ) ) + ( 𝑒 · 𝑌 ) ) ) → 𝑋𝑉 )
52 49 8 syl ( ( ( 𝜑 ∧ ( 𝑎𝐵𝑏𝐵 ) ∧ 𝑗 = ( ( 𝑎 · ( 𝑋 𝑌 ) ) + ( 𝑏 · 𝑍 ) ) ) ∧ ( 𝑑𝐵𝑒𝐵 ) ∧ 𝑗 = ( ( 𝑑 · ( 𝑋 𝑍 ) ) + ( 𝑒 · 𝑌 ) ) ) → ¬ 𝑋 ∈ ( 𝑁 ‘ { 𝑌 , 𝑍 } ) )
53 49 9 syl ( ( ( 𝜑 ∧ ( 𝑎𝐵𝑏𝐵 ) ∧ 𝑗 = ( ( 𝑎 · ( 𝑋 𝑌 ) ) + ( 𝑏 · 𝑍 ) ) ) ∧ ( 𝑑𝐵𝑒𝐵 ) ∧ 𝑗 = ( ( 𝑑 · ( 𝑋 𝑍 ) ) + ( 𝑒 · 𝑌 ) ) ) → ( 𝑁 ‘ { 𝑌 } ) ≠ ( 𝑁 ‘ { 𝑍 } ) )
54 49 10 syl ( ( ( 𝜑 ∧ ( 𝑎𝐵𝑏𝐵 ) ∧ 𝑗 = ( ( 𝑎 · ( 𝑋 𝑌 ) ) + ( 𝑏 · 𝑍 ) ) ) ∧ ( 𝑑𝐵𝑒𝐵 ) ∧ 𝑗 = ( ( 𝑑 · ( 𝑋 𝑍 ) ) + ( 𝑒 · 𝑌 ) ) ) → 𝑌 ∈ ( 𝑉 ∖ { 0 } ) )
55 49 11 syl ( ( ( 𝜑 ∧ ( 𝑎𝐵𝑏𝐵 ) ∧ 𝑗 = ( ( 𝑎 · ( 𝑋 𝑌 ) ) + ( 𝑏 · 𝑍 ) ) ) ∧ ( 𝑑𝐵𝑒𝐵 ) ∧ 𝑗 = ( ( 𝑑 · ( 𝑋 𝑍 ) ) + ( 𝑒 · 𝑌 ) ) ) → 𝑍 ∈ ( 𝑉 ∖ { 0 } ) )
56 simp12l ( ( ( 𝜑 ∧ ( 𝑎𝐵𝑏𝐵 ) ∧ 𝑗 = ( ( 𝑎 · ( 𝑋 𝑌 ) ) + ( 𝑏 · 𝑍 ) ) ) ∧ ( 𝑑𝐵𝑒𝐵 ) ∧ 𝑗 = ( ( 𝑑 · ( 𝑋 𝑍 ) ) + ( 𝑒 · 𝑌 ) ) ) → 𝑎𝐵 )
57 simp12r ( ( ( 𝜑 ∧ ( 𝑎𝐵𝑏𝐵 ) ∧ 𝑗 = ( ( 𝑎 · ( 𝑋 𝑌 ) ) + ( 𝑏 · 𝑍 ) ) ) ∧ ( 𝑑𝐵𝑒𝐵 ) ∧ 𝑗 = ( ( 𝑑 · ( 𝑋 𝑍 ) ) + ( 𝑒 · 𝑌 ) ) ) → 𝑏𝐵 )
58 simp2l ( ( ( 𝜑 ∧ ( 𝑎𝐵𝑏𝐵 ) ∧ 𝑗 = ( ( 𝑎 · ( 𝑋 𝑌 ) ) + ( 𝑏 · 𝑍 ) ) ) ∧ ( 𝑑𝐵𝑒𝐵 ) ∧ 𝑗 = ( ( 𝑑 · ( 𝑋 𝑍 ) ) + ( 𝑒 · 𝑌 ) ) ) → 𝑑𝐵 )
59 simp2r ( ( ( 𝜑 ∧ ( 𝑎𝐵𝑏𝐵 ) ∧ 𝑗 = ( ( 𝑎 · ( 𝑋 𝑌 ) ) + ( 𝑏 · 𝑍 ) ) ) ∧ ( 𝑑𝐵𝑒𝐵 ) ∧ 𝑗 = ( ( 𝑑 · ( 𝑋 𝑍 ) ) + ( 𝑒 · 𝑌 ) ) ) → 𝑒𝐵 )
60 simp13 ( ( ( 𝜑 ∧ ( 𝑎𝐵𝑏𝐵 ) ∧ 𝑗 = ( ( 𝑎 · ( 𝑋 𝑌 ) ) + ( 𝑏 · 𝑍 ) ) ) ∧ ( 𝑑𝐵𝑒𝐵 ) ∧ 𝑗 = ( ( 𝑑 · ( 𝑋 𝑍 ) ) + ( 𝑒 · 𝑌 ) ) ) → 𝑗 = ( ( 𝑎 · ( 𝑋 𝑌 ) ) + ( 𝑏 · 𝑍 ) ) )
61 simp3 ( ( ( 𝜑 ∧ ( 𝑎𝐵𝑏𝐵 ) ∧ 𝑗 = ( ( 𝑎 · ( 𝑋 𝑌 ) ) + ( 𝑏 · 𝑍 ) ) ) ∧ ( 𝑑𝐵𝑒𝐵 ) ∧ 𝑗 = ( ( 𝑑 · ( 𝑋 𝑍 ) ) + ( 𝑒 · 𝑌 ) ) ) → 𝑗 = ( ( 𝑑 · ( 𝑋 𝑍 ) ) + ( 𝑒 · 𝑌 ) ) )
62 1 2 3 4 5 50 51 52 53 54 55 12 13 14 15 16 17 18 19 56 57 58 59 60 61 baerlem5alem1 ( ( ( 𝜑 ∧ ( 𝑎𝐵𝑏𝐵 ) ∧ 𝑗 = ( ( 𝑎 · ( 𝑋 𝑌 ) ) + ( 𝑏 · 𝑍 ) ) ) ∧ ( 𝑑𝐵𝑒𝐵 ) ∧ 𝑗 = ( ( 𝑑 · ( 𝑋 𝑍 ) ) + ( 𝑒 · 𝑌 ) ) ) → 𝑗 = ( 𝑎 · ( 𝑋 ( 𝑌 + 𝑍 ) ) ) )
63 49 21 syl ( ( ( 𝜑 ∧ ( 𝑎𝐵𝑏𝐵 ) ∧ 𝑗 = ( ( 𝑎 · ( 𝑋 𝑌 ) ) + ( 𝑏 · 𝑍 ) ) ) ∧ ( 𝑑𝐵𝑒𝐵 ) ∧ 𝑗 = ( ( 𝑑 · ( 𝑋 𝑍 ) ) + ( 𝑒 · 𝑌 ) ) ) → 𝑊 ∈ LMod )
64 1 12 lmodvacl ( ( 𝑊 ∈ LMod ∧ 𝑌𝑉𝑍𝑉 ) → ( 𝑌 + 𝑍 ) ∈ 𝑉 )
65 21 24 25 64 syl3anc ( 𝜑 → ( 𝑌 + 𝑍 ) ∈ 𝑉 )
66 1 2 lmodvsubcl ( ( 𝑊 ∈ LMod ∧ 𝑋𝑉 ∧ ( 𝑌 + 𝑍 ) ∈ 𝑉 ) → ( 𝑋 ( 𝑌 + 𝑍 ) ) ∈ 𝑉 )
67 21 7 65 66 syl3anc ( 𝜑 → ( 𝑋 ( 𝑌 + 𝑍 ) ) ∈ 𝑉 )
68 49 67 syl ( ( ( 𝜑 ∧ ( 𝑎𝐵𝑏𝐵 ) ∧ 𝑗 = ( ( 𝑎 · ( 𝑋 𝑌 ) ) + ( 𝑏 · 𝑍 ) ) ) ∧ ( 𝑑𝐵𝑒𝐵 ) ∧ 𝑗 = ( ( 𝑑 · ( 𝑋 𝑍 ) ) + ( 𝑒 · 𝑌 ) ) ) → ( 𝑋 ( 𝑌 + 𝑍 ) ) ∈ 𝑉 )
69 1 13 14 15 5 63 56 68 lspsneli ( ( ( 𝜑 ∧ ( 𝑎𝐵𝑏𝐵 ) ∧ 𝑗 = ( ( 𝑎 · ( 𝑋 𝑌 ) ) + ( 𝑏 · 𝑍 ) ) ) ∧ ( 𝑑𝐵𝑒𝐵 ) ∧ 𝑗 = ( ( 𝑑 · ( 𝑋 𝑍 ) ) + ( 𝑒 · 𝑌 ) ) ) → ( 𝑎 · ( 𝑋 ( 𝑌 + 𝑍 ) ) ) ∈ ( 𝑁 ‘ { ( 𝑋 ( 𝑌 + 𝑍 ) ) } ) )
70 62 69 eqeltrd ( ( ( 𝜑 ∧ ( 𝑎𝐵𝑏𝐵 ) ∧ 𝑗 = ( ( 𝑎 · ( 𝑋 𝑌 ) ) + ( 𝑏 · 𝑍 ) ) ) ∧ ( 𝑑𝐵𝑒𝐵 ) ∧ 𝑗 = ( ( 𝑑 · ( 𝑋 𝑍 ) ) + ( 𝑒 · 𝑌 ) ) ) → 𝑗 ∈ ( 𝑁 ‘ { ( 𝑋 ( 𝑌 + 𝑍 ) ) } ) )
71 70 3exp ( ( 𝜑 ∧ ( 𝑎𝐵𝑏𝐵 ) ∧ 𝑗 = ( ( 𝑎 · ( 𝑋 𝑌 ) ) + ( 𝑏 · 𝑍 ) ) ) → ( ( 𝑑𝐵𝑒𝐵 ) → ( 𝑗 = ( ( 𝑑 · ( 𝑋 𝑍 ) ) + ( 𝑒 · 𝑌 ) ) → 𝑗 ∈ ( 𝑁 ‘ { ( 𝑋 ( 𝑌 + 𝑍 ) ) } ) ) ) )
72 71 rexlimdvv ( ( 𝜑 ∧ ( 𝑎𝐵𝑏𝐵 ) ∧ 𝑗 = ( ( 𝑎 · ( 𝑋 𝑌 ) ) + ( 𝑏 · 𝑍 ) ) ) → ( ∃ 𝑑𝐵𝑒𝐵 𝑗 = ( ( 𝑑 · ( 𝑋 𝑍 ) ) + ( 𝑒 · 𝑌 ) ) → 𝑗 ∈ ( 𝑁 ‘ { ( 𝑋 ( 𝑌 + 𝑍 ) ) } ) ) )
73 72 3exp ( 𝜑 → ( ( 𝑎𝐵𝑏𝐵 ) → ( 𝑗 = ( ( 𝑎 · ( 𝑋 𝑌 ) ) + ( 𝑏 · 𝑍 ) ) → ( ∃ 𝑑𝐵𝑒𝐵 𝑗 = ( ( 𝑑 · ( 𝑋 𝑍 ) ) + ( 𝑒 · 𝑌 ) ) → 𝑗 ∈ ( 𝑁 ‘ { ( 𝑋 ( 𝑌 + 𝑍 ) ) } ) ) ) ) )
74 73 rexlimdvv ( 𝜑 → ( ∃ 𝑎𝐵𝑏𝐵 𝑗 = ( ( 𝑎 · ( 𝑋 𝑌 ) ) + ( 𝑏 · 𝑍 ) ) → ( ∃ 𝑑𝐵𝑒𝐵 𝑗 = ( ( 𝑑 · ( 𝑋 𝑍 ) ) + ( 𝑒 · 𝑌 ) ) → 𝑗 ∈ ( 𝑁 ‘ { ( 𝑋 ( 𝑌 + 𝑍 ) ) } ) ) ) )
75 74 impd ( 𝜑 → ( ( ∃ 𝑎𝐵𝑏𝐵 𝑗 = ( ( 𝑎 · ( 𝑋 𝑌 ) ) + ( 𝑏 · 𝑍 ) ) ∧ ∃ 𝑑𝐵𝑒𝐵 𝑗 = ( ( 𝑑 · ( 𝑋 𝑍 ) ) + ( 𝑒 · 𝑌 ) ) ) → 𝑗 ∈ ( 𝑁 ‘ { ( 𝑋 ( 𝑌 + 𝑍 ) ) } ) ) )
76 48 75 sylbid ( 𝜑 → ( 𝑗 ∈ ( ( ( 𝑁 ‘ { ( 𝑋 𝑌 ) } ) ( 𝑁 ‘ { 𝑍 } ) ) ∩ ( ( 𝑁 ‘ { ( 𝑋 𝑍 ) } ) ( 𝑁 ‘ { 𝑌 } ) ) ) → 𝑗 ∈ ( 𝑁 ‘ { ( 𝑋 ( 𝑌 + 𝑍 ) ) } ) ) )
77 76 ssrdv ( 𝜑 → ( ( ( 𝑁 ‘ { ( 𝑋 𝑌 ) } ) ( 𝑁 ‘ { 𝑍 } ) ) ∩ ( ( 𝑁 ‘ { ( 𝑋 𝑍 ) } ) ( 𝑁 ‘ { 𝑌 } ) ) ) ⊆ ( 𝑁 ‘ { ( 𝑋 ( 𝑌 + 𝑍 ) ) } ) )
78 43 77 eqssd ( 𝜑 → ( 𝑁 ‘ { ( 𝑋 ( 𝑌 + 𝑍 ) ) } ) = ( ( ( 𝑁 ‘ { ( 𝑋 𝑌 ) } ) ( 𝑁 ‘ { 𝑍 } ) ) ∩ ( ( 𝑁 ‘ { ( 𝑋 𝑍 ) } ) ( 𝑁 ‘ { 𝑌 } ) ) ) )