This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 opelxp 
 |-  ( <. x , y >. e. ( { j } X. B ) <-> ( x e. { j } /\ y e. B ) )
68 67 bilani 
 |-  ( ( j e. A /\ <. x , y >. e. ( { j } X. B ) ) -> ( x e. { j } /\ y e. B ) )
69 68 simpld 
 |-  ( ( j e. A /\ <. x , y >. e. ( { j } X. B ) ) -> x e. { j } )
70 elsni 
 |-  ( x e. { j } -> x = j )
71 69 70 syl 
 |-  ( ( j e. A /\ <. x , y >. e. ( { j } X. B ) ) -> x = j )
72 simpl 
 |-  ( ( j e. A /\ <. x , y >. e. ( { j } X. B ) ) -> j e. A )
73 71 72 eqeltrd 
 |-  ( ( j e. A /\ <. x , y >. e. ( { j } X. B ) ) -> x e. A )
74 73 rexlimiva 
 |-  ( E. j e. A <. x , y >. e. ( { j } X. B ) -> x e. A )
75 66 74 syl 
 |-  ( ( ph /\ ( y e. C /\ x e. [_ y / k ]_ D ) ) -> x e. A )
76 75 expr 
 |-  ( ( ph /\ y e. C ) -> ( x e. [_ y / k ]_ D -> x e. A ) )
77 76 ssrdv 
 |-  ( ( ph /\ y e. C ) -> [_ y / k ]_ D C_ A )
78 59 77 ssfid 
 |-  ( ( ph /\ y e. C ) -> [_ y / k ]_ D e. Fin )
79 xpfi 
 |-  ( ( { y } e. Fin /\ [_ y / k ]_ D e. Fin ) -> ( { y } X. [_ y / k ]_ D ) e. Fin )
80 58 78 79 sylancr 
 |-  ( ( ph /\ y e. C ) -> ( { y } X. [_ y / k ]_ D ) e. Fin )
81 80 ralrimiva 
 |-  ( ph -> A. y e. C ( { y } X. [_ y / k ]_ D ) e. Fin )
82 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 )
83 2 81 82 syl2anc 
 |-  ( ph -> U_ y e. C ( { y } X. [_ y / k ]_ D ) e. Fin )
84 reliun 
 |-  ( Rel U_ y e. C ( { y } X. [_ y / k ]_ D ) <-> A. y e. C Rel ( { y } X. [_ y / k ]_ D ) )
85 relxp 
 |-  Rel ( { y } X. [_ y / k ]_ D )
86 85 a1i 
 |-  ( y e. C -> Rel ( { y } X. [_ y / k ]_ D ) )
87 84 86 mprgbir 
 |-  Rel U_ y e. C ( { y } X. [_ y / k ]_ D )
88 87 a1i 
 |-  ( ph -> Rel U_ y e. C ( { y } X. [_ y / k ]_ D ) )
89 csbeq1 
 |-  ( x = ( 2nd ` w ) -> [_ x / j ]_ E = [_ ( 2nd ` w ) / j ]_ E )
90 89 csbeq2dv 
 |-  ( x = ( 2nd ` w ) -> [_ ( 1st ` w ) / k ]_ [_ x / j ]_ E = [_ ( 1st ` w ) / k ]_ [_ ( 2nd ` w ) / j ]_ E )
91 90 eleq1d 
 |-  ( x = ( 2nd ` w ) -> ( [_ ( 1st ` w ) / k ]_ [_ x / j ]_ E e. CC <-> [_ ( 1st ` w ) / k ]_ [_ ( 2nd ` w ) / j ]_ E e. CC ) )
92 csbeq1 
 |-  ( y = ( 1st ` w ) -> [_ y / k ]_ D = [_ ( 1st ` w ) / k ]_ D )
93 csbeq1 
 |-  ( y = ( 1st ` w ) -> [_ y / k ]_ [_ x / j ]_ E = [_ ( 1st ` w ) / k ]_ [_ x / j ]_ E )
94 93 eleq1d 
 |-  ( y = ( 1st ` w ) -> ( [_ y / k ]_ [_ x / j ]_ E e. CC <-> [_ ( 1st ` w ) / k ]_ [_ x / j ]_ E e. CC ) )
95 92 94 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 ) )
96 simpl 
 |-  ( ( ph /\ ( y e. C /\ x e. [_ y / k ]_ D ) ) -> ph )
97 29 nfcri 
 |-  F/ j y e. [_ x / j ]_ B
98 70 equcomd 
 |-  ( x e. { j } -> j = x )
99 98 32 syl 
 |-  ( x e. { j } -> B = [_ x / j ]_ B )
100 99 eleq2d 
 |-  ( x e. { j } -> ( y e. B <-> y e. [_ x / j ]_ B ) )
101 100 biimpa 
 |-  ( ( x e. { j } /\ y e. B ) -> y e. [_ x / j ]_ B )
102 67 101 sylbi 
 |-  ( <. x , y >. e. ( { j } X. B ) -> y e. [_ x / j ]_ B )
103 102 a1i 
 |-  ( j e. A -> ( <. x , y >. e. ( { j } X. B ) -> y e. [_ x / j ]_ B ) )
104 97 103 rexlimi 
 |-  ( E. j e. A <. x , y >. e. ( { j } X. B ) -> y e. [_ x / j ]_ B )
105 66 104 syl 
 |-  ( ( ph /\ ( y e. C /\ x e. [_ y / k ]_ D ) ) -> y e. [_ x / j ]_ B )
106 5 ralrimivva 
 |-  ( ph -> A. j e. A A. k e. B E e. CC )
107 nfcsb1v 
 |-  F/_ j [_ x / j ]_ E
108 107 nfel1 
 |-  F/ j [_ x / j ]_ E e. CC
109 29 108 nfralw 
 |-  F/ j A. k e. [_ x / j ]_ B [_ x / j ]_ E e. CC
110 csbeq1a 
 |-  ( j = x -> E = [_ x / j ]_ E )
111 110 eleq1d 
 |-  ( j = x -> ( E e. CC <-> [_ x / j ]_ E e. CC ) )
112 32 111 raleqbidv 
 |-  ( j = x -> ( A. k e. B E e. CC <-> A. k e. [_ x / j ]_ B [_ x / j ]_ E e. CC ) )
113 109 112 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 ) )
114 106 113 mpan9 
 |-  ( ( ph /\ x e. A ) -> A. k e. [_ x / j ]_ B [_ x / j ]_ E e. CC )
115 nfcsb1v 
 |-  F/_ k [_ y / k ]_ [_ x / j ]_ E
116 115 nfel1 
 |-  F/ k [_ y / k ]_ [_ x / j ]_ E e. CC
117 csbeq1a 
 |-  ( k = y -> [_ x / j ]_ E = [_ y / k ]_ [_ x / j ]_ E )
118 117 eleq1d 
 |-  ( k = y -> ( [_ x / j ]_ E e. CC <-> [_ y / k ]_ [_ x / j ]_ E e. CC ) )
119 116 118 rspc 
 |-  ( y e. [_ x / j ]_ B -> ( A. k e. [_ x / j ]_ B [_ x / j ]_ E e. CC -> [_ y / k ]_ [_ x / j ]_ E e. CC ) )
120 114 119 syl5com 
 |-  ( ( ph /\ x e. A ) -> ( y e. [_ x / j ]_ B -> [_ y / k ]_ [_ x / j ]_ E e. CC ) )
121 120 impr 
 |-  ( ( ph /\ ( x e. A /\ y e. [_ x / j ]_ B ) ) -> [_ y / k ]_ [_ x / j ]_ E e. CC )
122 96 75 105 121 syl12anc 
 |-  ( ( ph /\ ( y e. C /\ x e. [_ y / k ]_ D ) ) -> [_ y / k ]_ [_ x / j ]_ E e. CC )
123 122 ralrimivva 
 |-  ( ph -> A. y e. C A. x e. [_ y / k ]_ D [_ y / k ]_ [_ x / j ]_ E e. CC )
124 123 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 )
125 eliun 
 |-  ( w e. U_ y e. C ( { y } X. [_ y / k ]_ D ) <-> E. y e. C w e. ( { y } X. [_ y / k ]_ D ) )
126 125 bilani 
 |-  ( ( ph /\ w e. U_ y e. C ( { y } X. [_ y / k ]_ D ) ) -> E. y e. C w e. ( { y } X. [_ y / k ]_ D ) )
127 xp1st 
 |-  ( w e. ( { y } X. [_ y / k ]_ D ) -> ( 1st ` w ) e. { y } )
128 127 adantl 
 |-  ( ( y e. C /\ w e. ( { y } X. [_ y / k ]_ D ) ) -> ( 1st ` w ) e. { y } )
129 elsni 
 |-  ( ( 1st ` w ) e. { y } -> ( 1st ` w ) = y )
130 128 129 syl 
 |-  ( ( y e. C /\ w e. ( { y } X. [_ y / k ]_ D ) ) -> ( 1st ` w ) = y )
131 simpl 
 |-  ( ( y e. C /\ w e. ( { y } X. [_ y / k ]_ D ) ) -> y e. C )
132 130 131 eqeltrd 
 |-  ( ( y e. C /\ w e. ( { y } X. [_ y / k ]_ D ) ) -> ( 1st ` w ) e. C )
133 132 rexlimiva 
 |-  ( E. y e. C w e. ( { y } X. [_ y / k ]_ D ) -> ( 1st ` w ) e. C )
134 126 133 syl 
 |-  ( ( ph /\ w e. U_ y e. C ( { y } X. [_ y / k ]_ D ) ) -> ( 1st ` w ) e. C )
135 95 124 134 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 )
136 xp2nd 
 |-  ( w e. ( { y } X. [_ y / k ]_ D ) -> ( 2nd ` w ) e. [_ y / k ]_ D )
137 136 adantl 
 |-  ( ( y e. C /\ w e. ( { y } X. [_ y / k ]_ D ) ) -> ( 2nd ` w ) e. [_ y / k ]_ D )
138 130 csbeq1d 
 |-  ( ( y e. C /\ w e. ( { y } X. [_ y / k ]_ D ) ) -> [_ ( 1st ` w ) / k ]_ D = [_ y / k ]_ D )
139 137 138 eleqtrrd 
 |-  ( ( y e. C /\ w e. ( { y } X. [_ y / k ]_ D ) ) -> ( 2nd ` w ) e. [_ ( 1st ` w ) / k ]_ D )
140 139 rexlimiva 
 |-  ( E. y e. C w e. ( { y } X. [_ y / k ]_ D ) -> ( 2nd ` w ) e. [_ ( 1st ` w ) / k ]_ D )
141 126 140 syl 
 |-  ( ( ph /\ w e. U_ y e. C ( { y } X. [_ y / k ]_ D ) ) -> ( 2nd ` w ) e. [_ ( 1st ` w ) / k ]_ D )
142 91 135 141 rspcdva 
 |-  ( ( ph /\ w e. U_ y e. C ( { y } X. [_ y / k ]_ D ) ) -> [_ ( 1st ` w ) / k ]_ [_ ( 2nd ` w ) / j ]_ E e. CC )
143 51 57 83 88 142 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 )
144 45 143 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 )
145 3 ralrimiva 
 |-  ( ph -> A. j e. A B e. Fin )
146 29 nfel1 
 |-  F/ j [_ x / j ]_ B e. Fin
147 32 eleq1d 
 |-  ( j = x -> ( B e. Fin <-> [_ x / j ]_ B e. Fin ) )
148 146 147 rspc 
 |-  ( x e. A -> ( A. j e. A B e. Fin -> [_ x / j ]_ B e. Fin ) )
149 145 148 mpan9 
 |-  ( ( ph /\ x e. A ) -> [_ x / j ]_ B e. Fin )
150 57 1 149 121 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 )
151 51 2 78 122 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 )
152 144 150 151 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 )
153 nfcv 
 |-  F/_ x prod_ k e. B E
154 nfcv 
 |-  F/_ j y
155 154 107 nfcsbw 
 |-  F/_ j [_ y / k ]_ [_ x / j ]_ E
156 29 155 nfcprod 
 |-  F/_ j prod_ y e. [_ x / j ]_ B [_ y / k ]_ [_ x / j ]_ E
157 nfcv 
 |-  F/_ y E
158 nfcsb1v 
 |-  F/_ k [_ y / k ]_ E
159 csbeq1a 
 |-  ( k = y -> E = [_ y / k ]_ E )
160 157 158 159 cbvprodi 
 |-  prod_ k e. B E = prod_ y e. B [_ y / k ]_ E
161 110 csbeq2dv 
 |-  ( j = x -> [_ y / k ]_ E = [_ y / k ]_ [_ x / j ]_ E )
162 161 adantr 
 |-  ( ( j = x /\ y e. B ) -> [_ y / k ]_ E = [_ y / k ]_ [_ x / j ]_ E )
163 32 162 prodeq12dv 
 |-  ( j = x -> prod_ y e. B [_ y / k ]_ E = prod_ y e. [_ x / j ]_ B [_ y / k ]_ [_ x / j ]_ E )
164 160 163 eqtrid 
 |-  ( j = x -> prod_ k e. B E = prod_ y e. [_ x / j ]_ B [_ y / k ]_ [_ x / j ]_ E )
165 153 156 164 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
166 nfcv 
 |-  F/_ y prod_ j e. D E
167 37 115 nfcprod 
 |-  F/_ k prod_ x e. [_ y / k ]_ D [_ y / k ]_ [_ x / j ]_ E
168 nfcv 
 |-  F/_ x E
169 168 107 110 cbvprodi 
 |-  prod_ j e. D E = prod_ x e. D [_ x / j ]_ E
170 117 adantr 
 |-  ( ( k = y /\ x e. D ) -> [_ x / j ]_ E = [_ y / k ]_ [_ x / j ]_ E )
171 40 170 prodeq12dv 
 |-  ( k = y -> prod_ x e. D [_ x / j ]_ E = prod_ x e. [_ y / k ]_ D [_ y / k ]_ [_ x / j ]_ E )
172 169 171 eqtrid 
 |-  ( k = y -> prod_ j e. D E = prod_ x e. [_ y / k ]_ D [_ y / k ]_ [_ x / j ]_ E )
173 166 167 172 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
174 152 165 173 3eqtr4g 
 |-  ( ph -> prod_ j e. A prod_ k e. B E = prod_ k e. C prod_ j e. D E )