Metamath Proof Explorer

Theorem fprodcom2

Description: Interchange order of multiplication. Note that B ( j ) and D ( k ) are not necessarily constant expressions. (Contributed by Scott Fenton, 1-Feb-2018) (Proof shortened by JJ, 2-Aug-2021)

Ref Expression
Hypotheses fprodcom2.1 
|- ( ph -> A e. Fin )
fprodcom2.2 
|- ( ph -> C e. Fin )
fprodcom2.3 
|- ( ( ph /\ j e. A ) -> B e. Fin )
fprodcom2.4 
|- ( ph -> ( ( j e. A /\ k e. B ) <-> ( k e. C /\ j e. D ) ) )
fprodcom2.5 
|- ( ( ph /\ ( j e. A /\ k e. B ) ) -> E e. CC )
Assertion fprodcom2 
|- ( ph -> prod_ j e. A prod_ k e. B E = prod_ k e. C prod_ j e. D E )

Proof

Step Hyp Ref Expression
1 fprodcom2.1 
 |-  ( ph -> A e. Fin )
2 fprodcom2.2 
 |-  ( ph -> C e. Fin )
3 fprodcom2.3 
 |-  ( ( ph /\ j e. A ) -> B e. Fin )
4 fprodcom2.4 
 |-  ( ph -> ( ( j e. A /\ k e. B ) <-> ( k e. C /\ j e. D ) ) )
5 fprodcom2.5 
 |-  ( ( ph /\ ( j e. A /\ k e. B ) ) -> E e. CC )
6 relxp 
 |-  Rel ( { j } X. B )
7 6 rgenw 
 |-  A. j e. A Rel ( { j } X. B )
8 reliun 
 |-  ( Rel U_ j e. A ( { j } X. B ) <-> A. j e. A Rel ( { j } X. B ) )
9 7 8 mpbir 
 |-  Rel U_ j e. A ( { j } X. B )
10 relcnv 
 |-  Rel `' U_ k e. C ( { k } X. D )
11 ancom 
 |-  ( ( x = j /\ y = k ) <-> ( y = k /\ x = j ) )
12 vex 
 |-  x e. _V
13 vex 
 |-  y e. _V
14 12 13 opth 
 |-  ( <. x , y >. = <. j , k >. <-> ( x = j /\ y = k ) )
15 13 12 opth 
 |-  ( <. y , x >. = <. k , j >. <-> ( y = k /\ x = j ) )
16 11 14 15 3bitr4i 
 |-  ( <. x , y >. = <. j , k >. <-> <. y , x >. = <. k , j >. )
17 16 a1i 
 |-  ( ph -> ( <. x , y >. = <. j , k >. <-> <. y , x >. = <. k , j >. ) )
18 17 4 anbi12d 
 |-  ( ph -> ( ( <. x , y >. = <. j , k >. /\ ( j e. A /\ k e. B ) ) <-> ( <. y , x >. = <. k , j >. /\ ( k e. C /\ j e. D ) ) ) )
19 18 2exbidv 
 |-  ( ph -> ( E. j E. k ( <. x , y >. = <. j , k >. /\ ( j e. A /\ k e. B ) ) <-> E. j E. k ( <. y , x >. = <. k , j >. /\ ( k e. C /\ j e. D ) ) ) )
20 eliunxp 
 |-  ( <. x , y >. e. U_ j e. A ( { j } X. B ) <-> E. j E. k ( <. x , y >. = <. j , k >. /\ ( j e. A /\ k e. B ) ) )
21 12 13 opelcnv 
 |-  ( <. x , y >. e. `' U_ k e. C ( { k } X. D ) <-> <. y , x >. e. U_ k e. C ( { k } X. D ) )
22 eliunxp 
 |-  ( <. y , x >. e. U_ k e. C ( { k } X. D ) <-> E. k E. j ( <. y , x >. = <. k , j >. /\ ( k e. C /\ j e. D ) ) )
23 excom 
 |-  ( E. k E. j ( <. y , x >. = <. k , j >. /\ ( k e. C /\ j e. D ) ) <-> E. j E. k ( <. y , x >. = <. k , j >. /\ ( k e. C /\ j e. D ) ) )
24 21 22 23 3bitri 
 |-  ( <. x , y >. e. `' U_ k e. C ( { k } X. D ) <-> E. j E. k ( <. y , x >. = <. k , j >. /\ ( k e. C /\ j e. D ) ) )
25 19 20 24 3bitr4g 
 |-  ( ph -> ( <. x , y >. e. U_ j e. A ( { j } X. B ) <-> <. x , y >. e. `' U_ k e. C ( { k } X. D ) ) )
26 9 10 25 eqrelrdv 
 |-  ( ph -> U_ j e. A ( { j } X. B ) = `' U_ k e. C ( { k } X. D ) )
27 nfcv 
 |-  F/_ x ( { j } X. B )
28 nfcv 
 |-  F/_ j { x }
29 nfcsb1v 
 |-  F/_ j [_ x / j ]_ B
30 28 29 nfxp 
 |-  F/_ j ( { x } X. [_ x / j ]_ B )
31 sneq 
 |-  ( j = x -> { j } = { x } )
32 csbeq1a 
 |-  ( j = x -> B = [_ x / j ]_ B )
33 31 32 xpeq12d 
 |-  ( j = x -> ( { j } X. B ) = ( { x } X. [_ x / j ]_ B ) )
34 27 30 33 cbviun 
 |-  U_ j e. A ( { j } X. B ) = U_ x e. A ( { x } X. [_ x / j ]_ B )
35 nfcv 
 |-  F/_ y ( { k } X. D )
36 nfcv 
 |-  F/_ k { y }
37 nfcsb1v 
 |-  F/_ k [_ y / k ]_ D
38 36 37 nfxp 
 |-  F/_ k ( { y } X. [_ y / k ]_ D )
39 sneq 
 |-  ( k = y -> { k } = { y } )
40 csbeq1a 
 |-  ( k = y -> D = [_ y / k ]_ D )
41 39 40 xpeq12d 
 |-  ( k = y -> ( { k } X. D ) = ( { y } X. [_ y / k ]_ D ) )
42 35 38 41 cbviun 
 |-  U_ k e. C ( { k } X. D ) = U_ y e. C ( { y } X. [_ y / k ]_ D )
43 42 cnveqi 
 |-  `' U_ k e. C ( { k } X. D ) = `' U_ y e. C ( { y } X. [_ y / k ]_ D )
44 26 34 43 3eqtr3g 
 |-  ( ph -> U_ x e. A ( { x } X. [_ x / j ]_ B ) = `' U_ y e. C ( { y } X. [_ y / k ]_ D ) )
45 44 prodeq1d 
 |-  ( ph -> prod_ z e. U_ x e. A ( { x } X. [_ x / j ]_ B ) [_ ( 2nd ` z ) / k ]_ [_ ( 1st ` z ) / j ]_ E = prod_ z e. `' U_ y e. C ( { y } X. [_ y / k ]_ D ) [_ ( 2nd ` z ) / k ]_ [_ ( 1st ` z ) / j ]_ E )
46 13 12 op1std 
 |-  ( w = <. y , x >. -> ( 1st ` w ) = y )
47 46 csbeq1d 
 |-  ( w = <. y , x >. -> [_ ( 1st ` w ) / k ]_ [_ ( 2nd ` w ) / j ]_ E = [_ y / k ]_ [_ ( 2nd ` w ) / j ]_ E )
48 13 12 op2ndd 
 |-  ( w = <. y , x >. -> ( 2nd ` w ) = x )
49 48 csbeq1d 
 |-  ( w = <. y , x >. -> [_ ( 2nd ` w ) / j ]_ E = [_ x / j ]_ E )
50 49 csbeq2dv 
 |-  ( w = <. y , x >. -> [_ y / k ]_ [_ ( 2nd ` w ) / j ]_ E = [_ y / k ]_ [_ x / j ]_ E )
51 47 50 eqtrd 
 |-  ( w = <. y , x >. -> [_ ( 1st ` w ) / k ]_ [_ ( 2nd ` w ) / j ]_ E = [_ y / k ]_ [_ x / j ]_ E )
52 12 13 op2ndd 
 |-  ( z = <. x , y >. -> ( 2nd ` z ) = y )
53 52 csbeq1d 
 |-  ( z = <. x , y >. -> [_ ( 2nd ` z ) / k ]_ [_ ( 1st ` z ) / j ]_ E = [_ y / k ]_ [_ ( 1st ` z ) / j ]_ E )
54 12 13 op1std 
 |-  ( z = <. x , y >. -> ( 1st ` z ) = x )
55 54 csbeq1d 
 |-  ( z = <. x , y >. -> [_ ( 1st ` z ) / j ]_ E = [_ x / j ]_ E )
56 55 csbeq2dv 
 |-  ( z = <. x , y >. -> [_ y / k ]_ [_ ( 1st ` z ) / j ]_ E = [_ y / k ]_ [_ x / j ]_ E )
57 53 56 eqtrd 
 |-  ( z = <. x , y >. -> [_ ( 2nd ` z ) / k ]_ [_ ( 1st ` z ) / j ]_ E = [_ y / k ]_ [_ x / j ]_ E )
58 snfi 
 |-  { y } e. Fin
59 1 adantr 
 |-  ( ( ph /\ y e. C ) -> A e. Fin )
60 37 40 opeliunxp2f 
 |-  ( <. y , x >. e. U_ k e. C ( { k } X. D ) <-> ( y e. C /\ x e. [_ y / k ]_ D ) )
61 21 60 sylbbr 
 |-  ( ( y e. C /\ x e. [_ y / k ]_ D ) -> <. x , y >. e. `' U_ k e. C ( { k } X. D ) )
62 61 adantl 
 |-  ( ( ph /\ ( y e. C /\ x e. [_ y / k ]_ D ) ) -> <. x , y >. e. `' U_ k e. C ( { k } X. D ) )
63 26 adantr 
 |-  ( ( ph /\ ( y e. C /\ x e. [_ y / k ]_ D ) ) -> U_ j e. A ( { j } X. B ) = `' U_ k e. C ( { k } X. D ) )
64 62 63 eleqtrrd 
 |-  ( ( ph /\ ( y e. C /\ x e. [_ y / k ]_ D ) ) -> <. x , y >. e. U_ j e. A ( { j } X. B ) )
65 eliun 
 |-  ( <. x , y >. e. U_ j e. A ( { j } X. B ) <-> E. j e. A <. x , y >. e. ( { j } X. B ) )
66 64 65 sylib 
 |-  ( ( ph /\ ( y e. C /\ x e. [_ y / k ]_ D ) ) -> E. j e. A <. x , y >. e. ( { j } X. B ) )
67 simpr 
 |-  ( ( j e. A /\ <. x , y >. e. ( { j } X. B ) ) -> <. x , y >. e. ( { j } X. B ) )
68 opelxp 
 |-  ( <. x , y >. e. ( { j } X. B ) <-> ( x e. { j } /\ y e. B ) )
69 67 68 sylib 
 |-  ( ( j e. A /\ <. x , y >. e. ( { j } X. B ) ) -> ( x e. { j } /\ y e. B ) )
70 69 simpld 
 |-  ( ( j e. A /\ <. x , y >. e. ( { j } X. B ) ) -> x e. { j } )
71 elsni 
 |-  ( x e. { j } -> x = j )
72 70 71 syl 
 |-  ( ( j e. A /\ <. x , y >. e. ( { j } X. B ) ) -> x = j )
73 simpl 
 |-  ( ( j e. A /\ <. x , y >. e. ( { j } X. B ) ) -> j e. A )
74 72 73 eqeltrd 
 |-  ( ( j e. A /\ <. x , y >. e. ( { j } X. B ) ) -> x e. A )
75 74 rexlimiva 
 |-  ( E. j e. A <. x , y >. e. ( { j } X. B ) -> x e. A )
76 66 75 syl 
 |-  ( ( ph /\ ( y e. C /\ x e. [_ y / k ]_ D ) ) -> x e. A )
77 76 expr 
 |-  ( ( ph /\ y e. C ) -> ( x e. [_ y / k ]_ D -> x e. A ) )
78 77 ssrdv 
 |-  ( ( ph /\ y e. C ) -> [_ y / k ]_ D C_ A )
79 59 78 ssfid 
 |-  ( ( ph /\ y e. C ) -> [_ y / k ]_ D e. Fin )
80 xpfi 
 |-  ( ( { y } e. Fin /\ [_ y / k ]_ D e. Fin ) -> ( { y } X. [_ y / k ]_ D ) e. Fin )
81 58 79 80 sylancr 
 |-  ( ( ph /\ y e. C ) -> ( { y } X. [_ y / k ]_ D ) e. Fin )
82 81 ralrimiva 
 |-  ( ph -> A. y e. C ( { y } X. [_ y / k ]_ D ) e. Fin )
83 iunfi 
 |-  ( ( C e. Fin /\ A. y e. C ( { y } X. [_ y / k ]_ D ) e. Fin ) -> U_ y e. C ( { y } X. [_ y / k ]_ D ) e. Fin )
84 2 82 83 syl2anc 
 |-  ( ph -> U_ y e. C ( { y } X. [_ y / k ]_ D ) e. Fin )
85 reliun 
 |-  ( Rel U_ y e. C ( { y } X. [_ y / k ]_ D ) <-> A. y e. C Rel ( { y } X. [_ y / k ]_ D ) )
86 relxp 
 |-  Rel ( { y } X. [_ y / k ]_ D )
87 86 a1i 
 |-  ( y e. C -> Rel ( { y } X. [_ y / k ]_ D ) )
88 85 87 mprgbir 
 |-  Rel U_ y e. C ( { y } X. [_ y / k ]_ D )
89 88 a1i 
 |-  ( ph -> Rel U_ y e. C ( { y } X. [_ y / k ]_ D ) )
90 csbeq1 
 |-  ( x = ( 2nd ` w ) -> [_ x / j ]_ E = [_ ( 2nd ` w ) / j ]_ E )
91 90 csbeq2dv 
 |-  ( x = ( 2nd ` w ) -> [_ ( 1st ` w ) / k ]_ [_ x / j ]_ E = [_ ( 1st ` w ) / k ]_ [_ ( 2nd ` w ) / j ]_ E )
92 91 eleq1d 
 |-  ( x = ( 2nd ` w ) -> ( [_ ( 1st ` w ) / k ]_ [_ x / j ]_ E e. CC <-> [_ ( 1st ` w ) / k ]_ [_ ( 2nd ` w ) / j ]_ E e. CC ) )
93 csbeq1 
 |-  ( y = ( 1st ` w ) -> [_ y / k ]_ D = [_ ( 1st ` w ) / k ]_ D )
94 csbeq1 
 |-  ( y = ( 1st ` w ) -> [_ y / k ]_ [_ x / j ]_ E = [_ ( 1st ` w ) / k ]_ [_ x / j ]_ E )
95 94 eleq1d 
 |-  ( y = ( 1st ` w ) -> ( [_ y / k ]_ [_ x / j ]_ E e. CC <-> [_ ( 1st ` w ) / k ]_ [_ x / j ]_ E e. CC ) )
96 93 95 raleqbidv 
 |-  ( y = ( 1st ` w ) -> ( A. x e. [_ y / k ]_ D [_ y / k ]_ [_ x / j ]_ E e. CC <-> A. x e. [_ ( 1st ` w ) / k ]_ D [_ ( 1st ` w ) / k ]_ [_ x / j ]_ E e. CC ) )
97 simpl 
 |-  ( ( ph /\ ( y e. C /\ x e. [_ y / k ]_ D ) ) -> ph )
98 29 nfcri 
 |-  F/ j y e. [_ x / j ]_ B
99 71 equcomd 
 |-  ( x e. { j } -> j = x )
100 99 32 syl 
 |-  ( x e. { j } -> B = [_ x / j ]_ B )
101 100 eleq2d 
 |-  ( x e. { j } -> ( y e. B <-> y e. [_ x / j ]_ B ) )
102 101 biimpa 
 |-  ( ( x e. { j } /\ y e. B ) -> y e. [_ x / j ]_ B )
103 68 102 sylbi 
 |-  ( <. x , y >. e. ( { j } X. B ) -> y e. [_ x / j ]_ B )
104 103 a1i 
 |-  ( j e. A -> ( <. x , y >. e. ( { j } X. B ) -> y e. [_ x / j ]_ B ) )
105 98 104 rexlimi 
 |-  ( E. j e. A <. x , y >. e. ( { j } X. B ) -> y e. [_ x / j ]_ B )
106 66 105 syl 
 |-  ( ( ph /\ ( y e. C /\ x e. [_ y / k ]_ D ) ) -> y e. [_ x / j ]_ B )
107 5 ralrimivva 
 |-  ( ph -> A. j e. A A. k e. B E e. CC )
108 nfcsb1v 
 |-  F/_ j [_ x / j ]_ E
109 108 nfel1 
 |-  F/ j [_ x / j ]_ E e. CC
110 29 109 nfralw 
 |-  F/ j A. k e. [_ x / j ]_ B [_ x / j ]_ E e. CC
111 csbeq1a 
 |-  ( j = x -> E = [_ x / j ]_ E )
112 111 eleq1d 
 |-  ( j = x -> ( E e. CC <-> [_ x / j ]_ E e. CC ) )
113 32 112 raleqbidv 
 |-  ( j = x -> ( A. k e. B E e. CC <-> A. k e. [_ x / j ]_ B [_ x / j ]_ E e. CC ) )
114 110 113 rspc 
 |-  ( x e. A -> ( A. j e. A A. k e. B E e. CC -> A. k e. [_ x / j ]_ B [_ x / j ]_ E e. CC ) )
115 107 114 mpan9 
 |-  ( ( ph /\ x e. A ) -> A. k e. [_ x / j ]_ B [_ x / j ]_ E e. CC )
116 nfcsb1v 
 |-  F/_ k [_ y / k ]_ [_ x / j ]_ E
117 116 nfel1 
 |-  F/ k [_ y / k ]_ [_ x / j ]_ E e. CC
118 csbeq1a 
 |-  ( k = y -> [_ x / j ]_ E = [_ y / k ]_ [_ x / j ]_ E )
119 118 eleq1d 
 |-  ( k = y -> ( [_ x / j ]_ E e. CC <-> [_ y / k ]_ [_ x / j ]_ E e. CC ) )
120 117 119 rspc 
 |-  ( y e. [_ x / j ]_ B -> ( A. k e. [_ x / j ]_ B [_ x / j ]_ E e. CC -> [_ y / k ]_ [_ x / j ]_ E e. CC ) )
121 115 120 syl5com 
 |-  ( ( ph /\ x e. A ) -> ( y e. [_ x / j ]_ B -> [_ y / k ]_ [_ x / j ]_ E e. CC ) )
122 121 impr 
 |-  ( ( ph /\ ( x e. A /\ y e. [_ x / j ]_ B ) ) -> [_ y / k ]_ [_ x / j ]_ E e. CC )
123 97 76 106 122 syl12anc 
 |-  ( ( ph /\ ( y e. C /\ x e. [_ y / k ]_ D ) ) -> [_ y / k ]_ [_ x / j ]_ E e. CC )
124 123 ralrimivva 
 |-  ( ph -> A. y e. C A. x e. [_ y / k ]_ D [_ y / k ]_ [_ x / j ]_ E e. CC )
125 124 adantr 
 |-  ( ( ph /\ w e. U_ y e. C ( { y } X. [_ y / k ]_ D ) ) -> A. y e. C A. x e. [_ y / k ]_ D [_ y / k ]_ [_ x / j ]_ E e. CC )
126 simpr 
 |-  ( ( ph /\ w e. U_ y e. C ( { y } X. [_ y / k ]_ D ) ) -> w e. U_ y e. C ( { y } X. [_ y / k ]_ D ) )
127 eliun 
 |-  ( w e. U_ y e. C ( { y } X. [_ y / k ]_ D ) <-> E. y e. C w e. ( { y } X. [_ y / k ]_ D ) )
128 126 127 sylib 
 |-  ( ( ph /\ w e. U_ y e. C ( { y } X. [_ y / k ]_ D ) ) -> E. y e. C w e. ( { y } X. [_ y / k ]_ D ) )
129 xp1st 
 |-  ( w e. ( { y } X. [_ y / k ]_ D ) -> ( 1st ` w ) e. { y } )
130 129 adantl 
 |-  ( ( y e. C /\ w e. ( { y } X. [_ y / k ]_ D ) ) -> ( 1st ` w ) e. { y } )
131 elsni 
 |-  ( ( 1st ` w ) e. { y } -> ( 1st ` w ) = y )
132 130 131 syl 
 |-  ( ( y e. C /\ w e. ( { y } X. [_ y / k ]_ D ) ) -> ( 1st ` w ) = y )
133 simpl 
 |-  ( ( y e. C /\ w e. ( { y } X. [_ y / k ]_ D ) ) -> y e. C )
134 132 133 eqeltrd 
 |-  ( ( y e. C /\ w e. ( { y } X. [_ y / k ]_ D ) ) -> ( 1st ` w ) e. C )
135 134 rexlimiva 
 |-  ( E. y e. C w e. ( { y } X. [_ y / k ]_ D ) -> ( 1st ` w ) e. C )
136 128 135 syl 
 |-  ( ( ph /\ w e. U_ y e. C ( { y } X. [_ y / k ]_ D ) ) -> ( 1st ` w ) e. C )
137 96 125 136 rspcdva 
 |-  ( ( ph /\ w e. U_ y e. C ( { y } X. [_ y / k ]_ D ) ) -> A. x e. [_ ( 1st ` w ) / k ]_ D [_ ( 1st ` w ) / k ]_ [_ x / j ]_ E e. CC )
138 xp2nd 
 |-  ( w e. ( { y } X. [_ y / k ]_ D ) -> ( 2nd ` w ) e. [_ y / k ]_ D )
139 138 adantl 
 |-  ( ( y e. C /\ w e. ( { y } X. [_ y / k ]_ D ) ) -> ( 2nd ` w ) e. [_ y / k ]_ D )
140 132 csbeq1d 
 |-  ( ( y e. C /\ w e. ( { y } X. [_ y / k ]_ D ) ) -> [_ ( 1st ` w ) / k ]_ D = [_ y / k ]_ D )
141 139 140 eleqtrrd 
 |-  ( ( y e. C /\ w e. ( { y } X. [_ y / k ]_ D ) ) -> ( 2nd ` w ) e. [_ ( 1st ` w ) / k ]_ D )
142 141 rexlimiva 
 |-  ( E. y e. C w e. ( { y } X. [_ y / k ]_ D ) -> ( 2nd ` w ) e. [_ ( 1st ` w ) / k ]_ D )
143 128 142 syl 
 |-  ( ( ph /\ w e. U_ y e. C ( { y } X. [_ y / k ]_ D ) ) -> ( 2nd ` w ) e. [_ ( 1st ` w ) / k ]_ D )
144 92 137 143 rspcdva 
 |-  ( ( ph /\ w e. U_ y e. C ( { y } X. [_ y / k ]_ D ) ) -> [_ ( 1st ` w ) / k ]_ [_ ( 2nd ` w ) / j ]_ E e. CC )
145 51 57 84 89 144 fprodcnv 
 |-  ( ph -> prod_ w e. U_ y e. C ( { y } X. [_ y / k ]_ D ) [_ ( 1st ` w ) / k ]_ [_ ( 2nd ` w ) / j ]_ E = prod_ z e. `' U_ y e. C ( { y } X. [_ y / k ]_ D ) [_ ( 2nd ` z ) / k ]_ [_ ( 1st ` z ) / j ]_ E )
146 45 145 eqtr4d 
 |-  ( ph -> prod_ z e. U_ x e. A ( { x } X. [_ x / j ]_ B ) [_ ( 2nd ` z ) / k ]_ [_ ( 1st ` z ) / j ]_ E = prod_ w e. U_ y e. C ( { y } X. [_ y / k ]_ D ) [_ ( 1st ` w ) / k ]_ [_ ( 2nd ` w ) / j ]_ E )
147 3 ralrimiva 
 |-  ( ph -> A. j e. A B e. Fin )
148 29 nfel1 
 |-  F/ j [_ x / j ]_ B e. Fin
149 32 eleq1d 
 |-  ( j = x -> ( B e. Fin <-> [_ x / j ]_ B e. Fin ) )
150 148 149 rspc 
 |-  ( x e. A -> ( A. j e. A B e. Fin -> [_ x / j ]_ B e. Fin ) )
151 147 150 mpan9 
 |-  ( ( ph /\ x e. A ) -> [_ x / j ]_ B e. Fin )
152 57 1 151 122 fprod2d 
 |-  ( ph -> prod_ x e. A prod_ y e. [_ x / j ]_ B [_ y / k ]_ [_ x / j ]_ E = prod_ z e. U_ x e. A ( { x } X. [_ x / j ]_ B ) [_ ( 2nd ` z ) / k ]_ [_ ( 1st ` z ) / j ]_ E )
153 51 2 79 123 fprod2d 
 |-  ( ph -> prod_ y e. C prod_ x e. [_ y / k ]_ D [_ y / k ]_ [_ x / j ]_ E = prod_ w e. U_ y e. C ( { y } X. [_ y / k ]_ D ) [_ ( 1st ` w ) / k ]_ [_ ( 2nd ` w ) / j ]_ E )
154 146 152 153 3eqtr4d 
 |-  ( ph -> prod_ x e. A prod_ y e. [_ x / j ]_ B [_ y / k ]_ [_ x / j ]_ E = prod_ y e. C prod_ x e. [_ y / k ]_ D [_ y / k ]_ [_ x / j ]_ E )
155 nfcv 
 |-  F/_ x prod_ k e. B E
156 nfcv 
 |-  F/_ j y
157 156 108 nfcsbw 
 |-  F/_ j [_ y / k ]_ [_ x / j ]_ E
158 29 157 nfcprod 
 |-  F/_ j prod_ y e. [_ x / j ]_ B [_ y / k ]_ [_ x / j ]_ E
159 nfcv 
 |-  F/_ y E
160 nfcsb1v 
 |-  F/_ k [_ y / k ]_ E
161 csbeq1a 
 |-  ( k = y -> E = [_ y / k ]_ E )
162 159 160 161 cbvprodi 
 |-  prod_ k e. B E = prod_ y e. B [_ y / k ]_ E
163 111 csbeq2dv 
 |-  ( j = x -> [_ y / k ]_ E = [_ y / k ]_ [_ x / j ]_ E )
164 163 adantr 
 |-  ( ( j = x /\ y e. B ) -> [_ y / k ]_ E = [_ y / k ]_ [_ x / j ]_ E )
165 32 164 prodeq12dv 
 |-  ( j = x -> prod_ y e. B [_ y / k ]_ E = prod_ y e. [_ x / j ]_ B [_ y / k ]_ [_ x / j ]_ E )
166 162 165 eqtrid 
 |-  ( j = x -> prod_ k e. B E = prod_ y e. [_ x / j ]_ B [_ y / k ]_ [_ x / j ]_ E )
167 155 158 166 cbvprodi 
 |-  prod_ j e. A prod_ k e. B E = prod_ x e. A prod_ y e. [_ x / j ]_ B [_ y / k ]_ [_ x / j ]_ E
168 nfcv 
 |-  F/_ y prod_ j e. D E
169 37 116 nfcprod 
 |-  F/_ k prod_ x e. [_ y / k ]_ D [_ y / k ]_ [_ x / j ]_ E
170 nfcv 
 |-  F/_ x E
171 170 108 111 cbvprodi 
 |-  prod_ j e. D E = prod_ x e. D [_ x / j ]_ E
172 118 adantr 
 |-  ( ( k = y /\ x e. D ) -> [_ x / j ]_ E = [_ y / k ]_ [_ x / j ]_ E )
173 40 172 prodeq12dv 
 |-  ( k = y -> prod_ x e. D [_ x / j ]_ E = prod_ x e. [_ y / k ]_ D [_ y / k ]_ [_ x / j ]_ E )
174 171 173 eqtrid 
 |-  ( k = y -> prod_ j e. D E = prod_ x e. [_ y / k ]_ D [_ y / k ]_ [_ x / j ]_ E )
175 168 169 174 cbvprodi 
 |-  prod_ k e. C prod_ j e. D E = prod_ y e. C prod_ x e. [_ y / k ]_ D [_ y / k ]_ [_ x / j ]_ E
176 154 167 175 3eqtr4g 
 |-  ( ph -> prod_ j e. A prod_ k e. B E = prod_ k e. C prod_ j e. D E )