Metamath Proof Explorer


Theorem lcfrlem23

Description: Lemma for lcfr . TODO: this proof was built from other proof pieces that may change N{ X , Y } into subspace sum and back unnecessarily, or similar things. (Contributed by NM, 1-Mar-2015)

Ref Expression
Hypotheses lcfrlem17.h 𝐻 = ( LHyp ‘ 𝐾 )
lcfrlem17.o = ( ( ocH ‘ 𝐾 ) ‘ 𝑊 )
lcfrlem17.u 𝑈 = ( ( DVecH ‘ 𝐾 ) ‘ 𝑊 )
lcfrlem17.v 𝑉 = ( Base ‘ 𝑈 )
lcfrlem17.p + = ( +g𝑈 )
lcfrlem17.z 0 = ( 0g𝑈 )
lcfrlem17.n 𝑁 = ( LSpan ‘ 𝑈 )
lcfrlem17.a 𝐴 = ( LSAtoms ‘ 𝑈 )
lcfrlem17.k ( 𝜑 → ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) )
lcfrlem17.x ( 𝜑𝑋 ∈ ( 𝑉 ∖ { 0 } ) )
lcfrlem17.y ( 𝜑𝑌 ∈ ( 𝑉 ∖ { 0 } ) )
lcfrlem17.ne ( 𝜑 → ( 𝑁 ‘ { 𝑋 } ) ≠ ( 𝑁 ‘ { 𝑌 } ) )
lcfrlem22.b 𝐵 = ( ( 𝑁 ‘ { 𝑋 , 𝑌 } ) ∩ ( ‘ { ( 𝑋 + 𝑌 ) } ) )
lcfrlem23.s = ( LSSum ‘ 𝑈 )
Assertion lcfrlem23 ( 𝜑 → ( ( ‘ { 𝑋 , 𝑌 } ) 𝐵 ) = ( ‘ { ( 𝑋 + 𝑌 ) } ) )

Proof

Step Hyp Ref Expression
1 lcfrlem17.h 𝐻 = ( LHyp ‘ 𝐾 )
2 lcfrlem17.o = ( ( ocH ‘ 𝐾 ) ‘ 𝑊 )
3 lcfrlem17.u 𝑈 = ( ( DVecH ‘ 𝐾 ) ‘ 𝑊 )
4 lcfrlem17.v 𝑉 = ( Base ‘ 𝑈 )
5 lcfrlem17.p + = ( +g𝑈 )
6 lcfrlem17.z 0 = ( 0g𝑈 )
7 lcfrlem17.n 𝑁 = ( LSpan ‘ 𝑈 )
8 lcfrlem17.a 𝐴 = ( LSAtoms ‘ 𝑈 )
9 lcfrlem17.k ( 𝜑 → ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) )
10 lcfrlem17.x ( 𝜑𝑋 ∈ ( 𝑉 ∖ { 0 } ) )
11 lcfrlem17.y ( 𝜑𝑌 ∈ ( 𝑉 ∖ { 0 } ) )
12 lcfrlem17.ne ( 𝜑 → ( 𝑁 ‘ { 𝑋 } ) ≠ ( 𝑁 ‘ { 𝑌 } ) )
13 lcfrlem22.b 𝐵 = ( ( 𝑁 ‘ { 𝑋 , 𝑌 } ) ∩ ( ‘ { ( 𝑋 + 𝑌 ) } ) )
14 lcfrlem23.s = ( LSSum ‘ 𝑈 )
15 13 fveq2i ( 𝐵 ) = ( ‘ ( ( 𝑁 ‘ { 𝑋 , 𝑌 } ) ∩ ( ‘ { ( 𝑋 + 𝑌 ) } ) ) )
16 eqid ( ( DIsoH ‘ 𝐾 ) ‘ 𝑊 ) = ( ( DIsoH ‘ 𝐾 ) ‘ 𝑊 )
17 eqid ( ( joinH ‘ 𝐾 ) ‘ 𝑊 ) = ( ( joinH ‘ 𝐾 ) ‘ 𝑊 )
18 10 eldifad ( 𝜑𝑋𝑉 )
19 11 eldifad ( 𝜑𝑌𝑉 )
20 1 3 4 7 16 9 18 19 dihprrn ( 𝜑 → ( 𝑁 ‘ { 𝑋 , 𝑌 } ) ∈ ran ( ( DIsoH ‘ 𝐾 ) ‘ 𝑊 ) )
21 1 3 9 dvhlmod ( 𝜑𝑈 ∈ LMod )
22 4 5 lmodvacl ( ( 𝑈 ∈ LMod ∧ 𝑋𝑉𝑌𝑉 ) → ( 𝑋 + 𝑌 ) ∈ 𝑉 )
23 21 18 19 22 syl3anc ( 𝜑 → ( 𝑋 + 𝑌 ) ∈ 𝑉 )
24 23 snssd ( 𝜑 → { ( 𝑋 + 𝑌 ) } ⊆ 𝑉 )
25 1 16 3 4 2 dochcl ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ { ( 𝑋 + 𝑌 ) } ⊆ 𝑉 ) → ( ‘ { ( 𝑋 + 𝑌 ) } ) ∈ ran ( ( DIsoH ‘ 𝐾 ) ‘ 𝑊 ) )
26 9 24 25 syl2anc ( 𝜑 → ( ‘ { ( 𝑋 + 𝑌 ) } ) ∈ ran ( ( DIsoH ‘ 𝐾 ) ‘ 𝑊 ) )
27 1 16 3 4 2 17 9 20 26 dochdmm1 ( 𝜑 → ( ‘ ( ( 𝑁 ‘ { 𝑋 , 𝑌 } ) ∩ ( ‘ { ( 𝑋 + 𝑌 ) } ) ) ) = ( ( ‘ ( 𝑁 ‘ { 𝑋 , 𝑌 } ) ) ( ( joinH ‘ 𝐾 ) ‘ 𝑊 ) ( ‘ ( ‘ { ( 𝑋 + 𝑌 ) } ) ) ) )
28 1 3 2 4 7 9 23 dochocsn ( 𝜑 → ( ‘ ( ‘ { ( 𝑋 + 𝑌 ) } ) ) = ( 𝑁 ‘ { ( 𝑋 + 𝑌 ) } ) )
29 28 oveq2d ( 𝜑 → ( ( ‘ ( 𝑁 ‘ { 𝑋 , 𝑌 } ) ) ( ( joinH ‘ 𝐾 ) ‘ 𝑊 ) ( ‘ ( ‘ { ( 𝑋 + 𝑌 ) } ) ) ) = ( ( ‘ ( 𝑁 ‘ { 𝑋 , 𝑌 } ) ) ( ( joinH ‘ 𝐾 ) ‘ 𝑊 ) ( 𝑁 ‘ { ( 𝑋 + 𝑌 ) } ) ) )
30 prssi ( ( 𝑋𝑉𝑌𝑉 ) → { 𝑋 , 𝑌 } ⊆ 𝑉 )
31 18 19 30 syl2anc ( 𝜑 → { 𝑋 , 𝑌 } ⊆ 𝑉 )
32 4 7 lspssv ( ( 𝑈 ∈ LMod ∧ { 𝑋 , 𝑌 } ⊆ 𝑉 ) → ( 𝑁 ‘ { 𝑋 , 𝑌 } ) ⊆ 𝑉 )
33 21 31 32 syl2anc ( 𝜑 → ( 𝑁 ‘ { 𝑋 , 𝑌 } ) ⊆ 𝑉 )
34 1 16 3 4 2 dochcl ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( 𝑁 ‘ { 𝑋 , 𝑌 } ) ⊆ 𝑉 ) → ( ‘ ( 𝑁 ‘ { 𝑋 , 𝑌 } ) ) ∈ ran ( ( DIsoH ‘ 𝐾 ) ‘ 𝑊 ) )
35 9 33 34 syl2anc ( 𝜑 → ( ‘ ( 𝑁 ‘ { 𝑋 , 𝑌 } ) ) ∈ ran ( ( DIsoH ‘ 𝐾 ) ‘ 𝑊 ) )
36 1 3 4 14 7 16 17 9 35 23 dihjat1 ( 𝜑 → ( ( ‘ ( 𝑁 ‘ { 𝑋 , 𝑌 } ) ) ( ( joinH ‘ 𝐾 ) ‘ 𝑊 ) ( 𝑁 ‘ { ( 𝑋 + 𝑌 ) } ) ) = ( ( ‘ ( 𝑁 ‘ { 𝑋 , 𝑌 } ) ) ( 𝑁 ‘ { ( 𝑋 + 𝑌 ) } ) ) )
37 27 29 36 3eqtrd ( 𝜑 → ( ‘ ( ( 𝑁 ‘ { 𝑋 , 𝑌 } ) ∩ ( ‘ { ( 𝑋 + 𝑌 ) } ) ) ) = ( ( ‘ ( 𝑁 ‘ { 𝑋 , 𝑌 } ) ) ( 𝑁 ‘ { ( 𝑋 + 𝑌 ) } ) ) )
38 15 37 syl5eq ( 𝜑 → ( 𝐵 ) = ( ( ‘ ( 𝑁 ‘ { 𝑋 , 𝑌 } ) ) ( 𝑁 ‘ { ( 𝑋 + 𝑌 ) } ) ) )
39 38 ineq2d ( 𝜑 → ( ( ( 𝑁 ‘ { 𝑋 } ) ( 𝑁 ‘ { 𝑌 } ) ) ∩ ( 𝐵 ) ) = ( ( ( 𝑁 ‘ { 𝑋 } ) ( 𝑁 ‘ { 𝑌 } ) ) ∩ ( ( ‘ ( 𝑁 ‘ { 𝑋 , 𝑌 } ) ) ( 𝑁 ‘ { ( 𝑋 + 𝑌 ) } ) ) ) )
40 eqid ( LSubSp ‘ 𝑈 ) = ( LSubSp ‘ 𝑈 )
41 40 lsssssubg ( 𝑈 ∈ LMod → ( LSubSp ‘ 𝑈 ) ⊆ ( SubGrp ‘ 𝑈 ) )
42 21 41 syl ( 𝜑 → ( LSubSp ‘ 𝑈 ) ⊆ ( SubGrp ‘ 𝑈 ) )
43 4 40 7 lspsncl ( ( 𝑈 ∈ LMod ∧ 𝑋𝑉 ) → ( 𝑁 ‘ { 𝑋 } ) ∈ ( LSubSp ‘ 𝑈 ) )
44 21 18 43 syl2anc ( 𝜑 → ( 𝑁 ‘ { 𝑋 } ) ∈ ( LSubSp ‘ 𝑈 ) )
45 4 40 7 lspsncl ( ( 𝑈 ∈ LMod ∧ 𝑌𝑉 ) → ( 𝑁 ‘ { 𝑌 } ) ∈ ( LSubSp ‘ 𝑈 ) )
46 21 19 45 syl2anc ( 𝜑 → ( 𝑁 ‘ { 𝑌 } ) ∈ ( LSubSp ‘ 𝑈 ) )
47 40 14 lsmcl ( ( 𝑈 ∈ LMod ∧ ( 𝑁 ‘ { 𝑋 } ) ∈ ( LSubSp ‘ 𝑈 ) ∧ ( 𝑁 ‘ { 𝑌 } ) ∈ ( LSubSp ‘ 𝑈 ) ) → ( ( 𝑁 ‘ { 𝑋 } ) ( 𝑁 ‘ { 𝑌 } ) ) ∈ ( LSubSp ‘ 𝑈 ) )
48 21 44 46 47 syl3anc ( 𝜑 → ( ( 𝑁 ‘ { 𝑋 } ) ( 𝑁 ‘ { 𝑌 } ) ) ∈ ( LSubSp ‘ 𝑈 ) )
49 42 48 sseldd ( 𝜑 → ( ( 𝑁 ‘ { 𝑋 } ) ( 𝑁 ‘ { 𝑌 } ) ) ∈ ( SubGrp ‘ 𝑈 ) )
50 1 3 4 40 2 dochlss ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( 𝑁 ‘ { 𝑋 , 𝑌 } ) ⊆ 𝑉 ) → ( ‘ ( 𝑁 ‘ { 𝑋 , 𝑌 } ) ) ∈ ( LSubSp ‘ 𝑈 ) )
51 9 33 50 syl2anc ( 𝜑 → ( ‘ ( 𝑁 ‘ { 𝑋 , 𝑌 } ) ) ∈ ( LSubSp ‘ 𝑈 ) )
52 42 51 sseldd ( 𝜑 → ( ‘ ( 𝑁 ‘ { 𝑋 , 𝑌 } ) ) ∈ ( SubGrp ‘ 𝑈 ) )
53 4 40 7 lspsncl ( ( 𝑈 ∈ LMod ∧ ( 𝑋 + 𝑌 ) ∈ 𝑉 ) → ( 𝑁 ‘ { ( 𝑋 + 𝑌 ) } ) ∈ ( LSubSp ‘ 𝑈 ) )
54 21 23 53 syl2anc ( 𝜑 → ( 𝑁 ‘ { ( 𝑋 + 𝑌 ) } ) ∈ ( LSubSp ‘ 𝑈 ) )
55 42 54 sseldd ( 𝜑 → ( 𝑁 ‘ { ( 𝑋 + 𝑌 ) } ) ∈ ( SubGrp ‘ 𝑈 ) )
56 4 5 7 14 lspsntri ( ( 𝑈 ∈ LMod ∧ 𝑋𝑉𝑌𝑉 ) → ( 𝑁 ‘ { ( 𝑋 + 𝑌 ) } ) ⊆ ( ( 𝑁 ‘ { 𝑋 } ) ( 𝑁 ‘ { 𝑌 } ) ) )
57 21 18 19 56 syl3anc ( 𝜑 → ( 𝑁 ‘ { ( 𝑋 + 𝑌 ) } ) ⊆ ( ( 𝑁 ‘ { 𝑋 } ) ( 𝑁 ‘ { 𝑌 } ) ) )
58 14 lsmmod2 ( ( ( ( ( 𝑁 ‘ { 𝑋 } ) ( 𝑁 ‘ { 𝑌 } ) ) ∈ ( SubGrp ‘ 𝑈 ) ∧ ( ‘ ( 𝑁 ‘ { 𝑋 , 𝑌 } ) ) ∈ ( SubGrp ‘ 𝑈 ) ∧ ( 𝑁 ‘ { ( 𝑋 + 𝑌 ) } ) ∈ ( SubGrp ‘ 𝑈 ) ) ∧ ( 𝑁 ‘ { ( 𝑋 + 𝑌 ) } ) ⊆ ( ( 𝑁 ‘ { 𝑋 } ) ( 𝑁 ‘ { 𝑌 } ) ) ) → ( ( ( 𝑁 ‘ { 𝑋 } ) ( 𝑁 ‘ { 𝑌 } ) ) ∩ ( ( ‘ ( 𝑁 ‘ { 𝑋 , 𝑌 } ) ) ( 𝑁 ‘ { ( 𝑋 + 𝑌 ) } ) ) ) = ( ( ( ( 𝑁 ‘ { 𝑋 } ) ( 𝑁 ‘ { 𝑌 } ) ) ∩ ( ‘ ( 𝑁 ‘ { 𝑋 , 𝑌 } ) ) ) ( 𝑁 ‘ { ( 𝑋 + 𝑌 ) } ) ) )
59 49 52 55 57 58 syl31anc ( 𝜑 → ( ( ( 𝑁 ‘ { 𝑋 } ) ( 𝑁 ‘ { 𝑌 } ) ) ∩ ( ( ‘ ( 𝑁 ‘ { 𝑋 , 𝑌 } ) ) ( 𝑁 ‘ { ( 𝑋 + 𝑌 ) } ) ) ) = ( ( ( ( 𝑁 ‘ { 𝑋 } ) ( 𝑁 ‘ { 𝑌 } ) ) ∩ ( ‘ ( 𝑁 ‘ { 𝑋 , 𝑌 } ) ) ) ( 𝑁 ‘ { ( 𝑋 + 𝑌 ) } ) ) )
60 4 7 14 21 18 19 lsmpr ( 𝜑 → ( 𝑁 ‘ { 𝑋 , 𝑌 } ) = ( ( 𝑁 ‘ { 𝑋 } ) ( 𝑁 ‘ { 𝑌 } ) ) )
61 60 ineq1d ( 𝜑 → ( ( 𝑁 ‘ { 𝑋 , 𝑌 } ) ∩ ( ‘ ( 𝑁 ‘ { 𝑋 , 𝑌 } ) ) ) = ( ( ( 𝑁 ‘ { 𝑋 } ) ( 𝑁 ‘ { 𝑌 } ) ) ∩ ( ‘ ( 𝑁 ‘ { 𝑋 , 𝑌 } ) ) ) )
62 4 40 7 21 18 19 lspprcl ( 𝜑 → ( 𝑁 ‘ { 𝑋 , 𝑌 } ) ∈ ( LSubSp ‘ 𝑈 ) )
63 1 3 40 6 2 dochnoncon ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( 𝑁 ‘ { 𝑋 , 𝑌 } ) ∈ ( LSubSp ‘ 𝑈 ) ) → ( ( 𝑁 ‘ { 𝑋 , 𝑌 } ) ∩ ( ‘ ( 𝑁 ‘ { 𝑋 , 𝑌 } ) ) ) = { 0 } )
64 9 62 63 syl2anc ( 𝜑 → ( ( 𝑁 ‘ { 𝑋 , 𝑌 } ) ∩ ( ‘ ( 𝑁 ‘ { 𝑋 , 𝑌 } ) ) ) = { 0 } )
65 61 64 eqtr3d ( 𝜑 → ( ( ( 𝑁 ‘ { 𝑋 } ) ( 𝑁 ‘ { 𝑌 } ) ) ∩ ( ‘ ( 𝑁 ‘ { 𝑋 , 𝑌 } ) ) ) = { 0 } )
66 65 oveq1d ( 𝜑 → ( ( ( ( 𝑁 ‘ { 𝑋 } ) ( 𝑁 ‘ { 𝑌 } ) ) ∩ ( ‘ ( 𝑁 ‘ { 𝑋 , 𝑌 } ) ) ) ( 𝑁 ‘ { ( 𝑋 + 𝑌 ) } ) ) = ( { 0 } ( 𝑁 ‘ { ( 𝑋 + 𝑌 ) } ) ) )
67 6 14 lsm02 ( ( 𝑁 ‘ { ( 𝑋 + 𝑌 ) } ) ∈ ( SubGrp ‘ 𝑈 ) → ( { 0 } ( 𝑁 ‘ { ( 𝑋 + 𝑌 ) } ) ) = ( 𝑁 ‘ { ( 𝑋 + 𝑌 ) } ) )
68 55 67 syl ( 𝜑 → ( { 0 } ( 𝑁 ‘ { ( 𝑋 + 𝑌 ) } ) ) = ( 𝑁 ‘ { ( 𝑋 + 𝑌 ) } ) )
69 66 68 eqtrd ( 𝜑 → ( ( ( ( 𝑁 ‘ { 𝑋 } ) ( 𝑁 ‘ { 𝑌 } ) ) ∩ ( ‘ ( 𝑁 ‘ { 𝑋 , 𝑌 } ) ) ) ( 𝑁 ‘ { ( 𝑋 + 𝑌 ) } ) ) = ( 𝑁 ‘ { ( 𝑋 + 𝑌 ) } ) )
70 39 59 69 3eqtrd ( 𝜑 → ( ( ( 𝑁 ‘ { 𝑋 } ) ( 𝑁 ‘ { 𝑌 } ) ) ∩ ( 𝐵 ) ) = ( 𝑁 ‘ { ( 𝑋 + 𝑌 ) } ) )
71 70 fveq2d ( 𝜑 → ( ‘ ( ( ( 𝑁 ‘ { 𝑋 } ) ( 𝑁 ‘ { 𝑌 } ) ) ∩ ( 𝐵 ) ) ) = ( ‘ ( 𝑁 ‘ { ( 𝑋 + 𝑌 ) } ) ) )
72 1 3 4 14 7 16 9 18 19 dihsmsnrn ( 𝜑 → ( ( 𝑁 ‘ { 𝑋 } ) ( 𝑁 ‘ { 𝑌 } ) ) ∈ ran ( ( DIsoH ‘ 𝐾 ) ‘ 𝑊 ) )
73 1 2 3 4 5 6 7 8 9 10 11 12 13 lcfrlem22 ( 𝜑𝐵𝐴 )
74 4 8 21 73 lsatssv ( 𝜑𝐵𝑉 )
75 1 16 3 4 2 dochcl ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ 𝐵𝑉 ) → ( 𝐵 ) ∈ ran ( ( DIsoH ‘ 𝐾 ) ‘ 𝑊 ) )
76 9 74 75 syl2anc ( 𝜑 → ( 𝐵 ) ∈ ran ( ( DIsoH ‘ 𝐾 ) ‘ 𝑊 ) )
77 1 16 3 4 2 17 9 72 76 dochdmm1 ( 𝜑 → ( ‘ ( ( ( 𝑁 ‘ { 𝑋 } ) ( 𝑁 ‘ { 𝑌 } ) ) ∩ ( 𝐵 ) ) ) = ( ( ‘ ( ( 𝑁 ‘ { 𝑋 } ) ( 𝑁 ‘ { 𝑌 } ) ) ) ( ( joinH ‘ 𝐾 ) ‘ 𝑊 ) ( ‘ ( 𝐵 ) ) ) )
78 60 fveq2d ( 𝜑 → ( ‘ ( 𝑁 ‘ { 𝑋 , 𝑌 } ) ) = ( ‘ ( ( 𝑁 ‘ { 𝑋 } ) ( 𝑁 ‘ { 𝑌 } ) ) ) )
79 1 3 2 4 7 9 31 dochocsp ( 𝜑 → ( ‘ ( 𝑁 ‘ { 𝑋 , 𝑌 } ) ) = ( ‘ { 𝑋 , 𝑌 } ) )
80 78 79 eqtr3d ( 𝜑 → ( ‘ ( ( 𝑁 ‘ { 𝑋 } ) ( 𝑁 ‘ { 𝑌 } ) ) ) = ( ‘ { 𝑋 , 𝑌 } ) )
81 1 3 16 8 dih1dimat ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ 𝐵𝐴 ) → 𝐵 ∈ ran ( ( DIsoH ‘ 𝐾 ) ‘ 𝑊 ) )
82 9 73 81 syl2anc ( 𝜑𝐵 ∈ ran ( ( DIsoH ‘ 𝐾 ) ‘ 𝑊 ) )
83 1 16 2 dochoc ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ 𝐵 ∈ ran ( ( DIsoH ‘ 𝐾 ) ‘ 𝑊 ) ) → ( ‘ ( 𝐵 ) ) = 𝐵 )
84 9 82 83 syl2anc ( 𝜑 → ( ‘ ( 𝐵 ) ) = 𝐵 )
85 80 84 oveq12d ( 𝜑 → ( ( ‘ ( ( 𝑁 ‘ { 𝑋 } ) ( 𝑁 ‘ { 𝑌 } ) ) ) ( ( joinH ‘ 𝐾 ) ‘ 𝑊 ) ( ‘ ( 𝐵 ) ) ) = ( ( ‘ { 𝑋 , 𝑌 } ) ( ( joinH ‘ 𝐾 ) ‘ 𝑊 ) 𝐵 ) )
86 1 16 3 4 2 dochcl ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ { 𝑋 , 𝑌 } ⊆ 𝑉 ) → ( ‘ { 𝑋 , 𝑌 } ) ∈ ran ( ( DIsoH ‘ 𝐾 ) ‘ 𝑊 ) )
87 9 31 86 syl2anc ( 𝜑 → ( ‘ { 𝑋 , 𝑌 } ) ∈ ran ( ( DIsoH ‘ 𝐾 ) ‘ 𝑊 ) )
88 1 16 17 3 14 8 9 87 73 dihjat2 ( 𝜑 → ( ( ‘ { 𝑋 , 𝑌 } ) ( ( joinH ‘ 𝐾 ) ‘ 𝑊 ) 𝐵 ) = ( ( ‘ { 𝑋 , 𝑌 } ) 𝐵 ) )
89 77 85 88 3eqtrd ( 𝜑 → ( ‘ ( ( ( 𝑁 ‘ { 𝑋 } ) ( 𝑁 ‘ { 𝑌 } ) ) ∩ ( 𝐵 ) ) ) = ( ( ‘ { 𝑋 , 𝑌 } ) 𝐵 ) )
90 1 3 2 4 7 9 24 dochocsp ( 𝜑 → ( ‘ ( 𝑁 ‘ { ( 𝑋 + 𝑌 ) } ) ) = ( ‘ { ( 𝑋 + 𝑌 ) } ) )
91 71 89 90 3eqtr3d ( 𝜑 → ( ( ‘ { 𝑋 , 𝑌 } ) 𝐵 ) = ( ‘ { ( 𝑋 + 𝑌 ) } ) )