Metamath Proof Explorer

Theorem mamuass

Description: Matrix multiplication is associative, see also statement in Lang p. 505. (Contributed by Stefan O'Rear, 5-Sep-2015)

Ref Expression
Hypotheses mamucl.b 
|- B = ( Base ` R )
mamucl.r 
|- ( ph -> R e. Ring )
mamuass.m 
|- ( ph -> M e. Fin )
mamuass.n 
|- ( ph -> N e. Fin )
mamuass.o 
|- ( ph -> O e. Fin )
mamuass.p 
|- ( ph -> P e. Fin )
mamuass.x 
|- ( ph -> X e. ( B ^m ( M X. N ) ) )
mamuass.y 
|- ( ph -> Y e. ( B ^m ( N X. O ) ) )
mamuass.z 
|- ( ph -> Z e. ( B ^m ( O X. P ) ) )
mamuass.f 
|- F = ( R maMul <. M , N , O >. )
mamuass.g 
|- G = ( R maMul <. M , O , P >. )
mamuass.h 
|- H = ( R maMul <. M , N , P >. )
mamuass.i 
|- I = ( R maMul <. N , O , P >. )
Assertion mamuass 
|- ( ph -> ( ( X F Y ) G Z ) = ( X H ( Y I Z ) ) )

Proof

Step Hyp Ref Expression
1 mamucl.b 
 |-  B = ( Base ` R )
2 mamucl.r 
 |-  ( ph -> R e. Ring )
3 mamuass.m 
 |-  ( ph -> M e. Fin )
4 mamuass.n 
 |-  ( ph -> N e. Fin )
5 mamuass.o 
 |-  ( ph -> O e. Fin )
6 mamuass.p 
 |-  ( ph -> P e. Fin )
7 mamuass.x 
 |-  ( ph -> X e. ( B ^m ( M X. N ) ) )
8 mamuass.y 
 |-  ( ph -> Y e. ( B ^m ( N X. O ) ) )
9 mamuass.z 
 |-  ( ph -> Z e. ( B ^m ( O X. P ) ) )
10 mamuass.f 
 |-  F = ( R maMul <. M , N , O >. )
11 mamuass.g 
 |-  G = ( R maMul <. M , O , P >. )
12 mamuass.h 
 |-  H = ( R maMul <. M , N , P >. )
13 mamuass.i 
 |-  I = ( R maMul <. N , O , P >. )
14 ringcmn 
 |-  ( R e. Ring -> R e. CMnd )
15 2 14 syl 
 |-  ( ph -> R e. CMnd )
16 15 adantr 
 |-  ( ( ph /\ ( i e. M /\ k e. P ) ) -> R e. CMnd )
17 5 adantr 
 |-  ( ( ph /\ ( i e. M /\ k e. P ) ) -> O e. Fin )
18 4 adantr 
 |-  ( ( ph /\ ( i e. M /\ k e. P ) ) -> N e. Fin )
19 2 ad2antrr 
 |-  ( ( ( ph /\ ( i e. M /\ k e. P ) ) /\ ( j e. O /\ l e. N ) ) -> R e. Ring )
20 elmapi 
 |-  ( X e. ( B ^m ( M X. N ) ) -> X : ( M X. N ) --> B )
21 7 20 syl 
 |-  ( ph -> X : ( M X. N ) --> B )
22 21 ad2antrr 
 |-  ( ( ( ph /\ ( i e. M /\ k e. P ) ) /\ l e. N ) -> X : ( M X. N ) --> B )
23 simplrl 
 |-  ( ( ( ph /\ ( i e. M /\ k e. P ) ) /\ l e. N ) -> i e. M )
24 simpr 
 |-  ( ( ( ph /\ ( i e. M /\ k e. P ) ) /\ l e. N ) -> l e. N )
25 22 23 24 fovrnd 
 |-  ( ( ( ph /\ ( i e. M /\ k e. P ) ) /\ l e. N ) -> ( i X l ) e. B )
26 25 adantrl 
 |-  ( ( ( ph /\ ( i e. M /\ k e. P ) ) /\ ( j e. O /\ l e. N ) ) -> ( i X l ) e. B )
27 elmapi 
 |-  ( Y e. ( B ^m ( N X. O ) ) -> Y : ( N X. O ) --> B )
28 8 27 syl 
 |-  ( ph -> Y : ( N X. O ) --> B )
29 28 ad2antrr 
 |-  ( ( ( ph /\ ( i e. M /\ k e. P ) ) /\ ( j e. O /\ l e. N ) ) -> Y : ( N X. O ) --> B )
30 simprr 
 |-  ( ( ( ph /\ ( i e. M /\ k e. P ) ) /\ ( j e. O /\ l e. N ) ) -> l e. N )
31 simprl 
 |-  ( ( ( ph /\ ( i e. M /\ k e. P ) ) /\ ( j e. O /\ l e. N ) ) -> j e. O )
32 29 30 31 fovrnd 
 |-  ( ( ( ph /\ ( i e. M /\ k e. P ) ) /\ ( j e. O /\ l e. N ) ) -> ( l Y j ) e. B )
33 elmapi 
 |-  ( Z e. ( B ^m ( O X. P ) ) -> Z : ( O X. P ) --> B )
34 9 33 syl 
 |-  ( ph -> Z : ( O X. P ) --> B )
35 34 ad2antrr 
 |-  ( ( ( ph /\ ( i e. M /\ k e. P ) ) /\ j e. O ) -> Z : ( O X. P ) --> B )
36 simpr 
 |-  ( ( ( ph /\ ( i e. M /\ k e. P ) ) /\ j e. O ) -> j e. O )
37 simplrr 
 |-  ( ( ( ph /\ ( i e. M /\ k e. P ) ) /\ j e. O ) -> k e. P )
38 35 36 37 fovrnd 
 |-  ( ( ( ph /\ ( i e. M /\ k e. P ) ) /\ j e. O ) -> ( j Z k ) e. B )
39 38 adantrr 
 |-  ( ( ( ph /\ ( i e. M /\ k e. P ) ) /\ ( j e. O /\ l e. N ) ) -> ( j Z k ) e. B )
40 eqid 
 |-  ( .r ` R ) = ( .r ` R )
41 1 40 ringcl 
 |-  ( ( R e. Ring /\ ( l Y j ) e. B /\ ( j Z k ) e. B ) -> ( ( l Y j ) ( .r ` R ) ( j Z k ) ) e. B )
42 19 32 39 41 syl3anc 
 |-  ( ( ( ph /\ ( i e. M /\ k e. P ) ) /\ ( j e. O /\ l e. N ) ) -> ( ( l Y j ) ( .r ` R ) ( j Z k ) ) e. B )
43 1 40 ringcl 
 |-  ( ( R e. Ring /\ ( i X l ) e. B /\ ( ( l Y j ) ( .r ` R ) ( j Z k ) ) e. B ) -> ( ( i X l ) ( .r ` R ) ( ( l Y j ) ( .r ` R ) ( j Z k ) ) ) e. B )
44 19 26 42 43 syl3anc 
 |-  ( ( ( ph /\ ( i e. M /\ k e. P ) ) /\ ( j e. O /\ l e. N ) ) -> ( ( i X l ) ( .r ` R ) ( ( l Y j ) ( .r ` R ) ( j Z k ) ) ) e. B )
45 1 16 17 18 44 gsumcom3fi 
 |-  ( ( ph /\ ( i e. M /\ k e. P ) ) -> ( R gsum ( j e. O |-> ( R gsum ( l e. N |-> ( ( i X l ) ( .r ` R ) ( ( l Y j ) ( .r ` R ) ( j Z k ) ) ) ) ) ) ) = ( R gsum ( l e. N |-> ( R gsum ( j e. O |-> ( ( i X l ) ( .r ` R ) ( ( l Y j ) ( .r ` R ) ( j Z k ) ) ) ) ) ) ) )
46 2 ad2antrr 
 |-  ( ( ( ph /\ ( i e. M /\ k e. P ) ) /\ j e. O ) -> R e. Ring )
47 3 ad2antrr 
 |-  ( ( ( ph /\ ( i e. M /\ k e. P ) ) /\ j e. O ) -> M e. Fin )
48 4 ad2antrr 
 |-  ( ( ( ph /\ ( i e. M /\ k e. P ) ) /\ j e. O ) -> N e. Fin )
49 5 ad2antrr 
 |-  ( ( ( ph /\ ( i e. M /\ k e. P ) ) /\ j e. O ) -> O e. Fin )
50 7 ad2antrr 
 |-  ( ( ( ph /\ ( i e. M /\ k e. P ) ) /\ j e. O ) -> X e. ( B ^m ( M X. N ) ) )
51 8 ad2antrr 
 |-  ( ( ( ph /\ ( i e. M /\ k e. P ) ) /\ j e. O ) -> Y e. ( B ^m ( N X. O ) ) )
52 simplrl 
 |-  ( ( ( ph /\ ( i e. M /\ k e. P ) ) /\ j e. O ) -> i e. M )
53 10 1 40 46 47 48 49 50 51 52 36 mamufv 
 |-  ( ( ( ph /\ ( i e. M /\ k e. P ) ) /\ j e. O ) -> ( i ( X F Y ) j ) = ( R gsum ( l e. N |-> ( ( i X l ) ( .r ` R ) ( l Y j ) ) ) ) )
54 53 oveq1d 
 |-  ( ( ( ph /\ ( i e. M /\ k e. P ) ) /\ j e. O ) -> ( ( i ( X F Y ) j ) ( .r ` R ) ( j Z k ) ) = ( ( R gsum ( l e. N |-> ( ( i X l ) ( .r ` R ) ( l Y j ) ) ) ) ( .r ` R ) ( j Z k ) ) )
55 eqid 
 |-  ( 0g ` R ) = ( 0g ` R )
56 eqid 
 |-  ( +g ` R ) = ( +g ` R )
57 1 40 ringcl 
 |-  ( ( R e. Ring /\ ( i X l ) e. B /\ ( l Y j ) e. B ) -> ( ( i X l ) ( .r ` R ) ( l Y j ) ) e. B )
58 19 26 32 57 syl3anc 
 |-  ( ( ( ph /\ ( i e. M /\ k e. P ) ) /\ ( j e. O /\ l e. N ) ) -> ( ( i X l ) ( .r ` R ) ( l Y j ) ) e. B )
59 58 anassrs 
 |-  ( ( ( ( ph /\ ( i e. M /\ k e. P ) ) /\ j e. O ) /\ l e. N ) -> ( ( i X l ) ( .r ` R ) ( l Y j ) ) e. B )
60 eqid 
 |-  ( l e. N |-> ( ( i X l ) ( .r ` R ) ( l Y j ) ) ) = ( l e. N |-> ( ( i X l ) ( .r ` R ) ( l Y j ) ) )
61 ovexd 
 |-  ( ( ( ( ph /\ ( i e. M /\ k e. P ) ) /\ j e. O ) /\ l e. N ) -> ( ( i X l ) ( .r ` R ) ( l Y j ) ) e. _V )
62 fvexd 
 |-  ( ( ( ph /\ ( i e. M /\ k e. P ) ) /\ j e. O ) -> ( 0g ` R ) e. _V )
63 60 48 61 62 fsuppmptdm 
 |-  ( ( ( ph /\ ( i e. M /\ k e. P ) ) /\ j e. O ) -> ( l e. N |-> ( ( i X l ) ( .r ` R ) ( l Y j ) ) ) finSupp ( 0g ` R ) )
64 1 55 56 40 46 48 38 59 63 gsummulc1 
 |-  ( ( ( ph /\ ( i e. M /\ k e. P ) ) /\ j e. O ) -> ( R gsum ( l e. N |-> ( ( ( i X l ) ( .r ` R ) ( l Y j ) ) ( .r ` R ) ( j Z k ) ) ) ) = ( ( R gsum ( l e. N |-> ( ( i X l ) ( .r ` R ) ( l Y j ) ) ) ) ( .r ` R ) ( j Z k ) ) )
65 1 40 ringass 
 |-  ( ( R e. Ring /\ ( ( i X l ) e. B /\ ( l Y j ) e. B /\ ( j Z k ) e. B ) ) -> ( ( ( i X l ) ( .r ` R ) ( l Y j ) ) ( .r ` R ) ( j Z k ) ) = ( ( i X l ) ( .r ` R ) ( ( l Y j ) ( .r ` R ) ( j Z k ) ) ) )
66 19 26 32 39 65 syl13anc 
 |-  ( ( ( ph /\ ( i e. M /\ k e. P ) ) /\ ( j e. O /\ l e. N ) ) -> ( ( ( i X l ) ( .r ` R ) ( l Y j ) ) ( .r ` R ) ( j Z k ) ) = ( ( i X l ) ( .r ` R ) ( ( l Y j ) ( .r ` R ) ( j Z k ) ) ) )
67 66 anassrs 
 |-  ( ( ( ( ph /\ ( i e. M /\ k e. P ) ) /\ j e. O ) /\ l e. N ) -> ( ( ( i X l ) ( .r ` R ) ( l Y j ) ) ( .r ` R ) ( j Z k ) ) = ( ( i X l ) ( .r ` R ) ( ( l Y j ) ( .r ` R ) ( j Z k ) ) ) )
68 67 mpteq2dva 
 |-  ( ( ( ph /\ ( i e. M /\ k e. P ) ) /\ j e. O ) -> ( l e. N |-> ( ( ( i X l ) ( .r ` R ) ( l Y j ) ) ( .r ` R ) ( j Z k ) ) ) = ( l e. N |-> ( ( i X l ) ( .r ` R ) ( ( l Y j ) ( .r ` R ) ( j Z k ) ) ) ) )
69 68 oveq2d 
 |-  ( ( ( ph /\ ( i e. M /\ k e. P ) ) /\ j e. O ) -> ( R gsum ( l e. N |-> ( ( ( i X l ) ( .r ` R ) ( l Y j ) ) ( .r ` R ) ( j Z k ) ) ) ) = ( R gsum ( l e. N |-> ( ( i X l ) ( .r ` R ) ( ( l Y j ) ( .r ` R ) ( j Z k ) ) ) ) ) )
70 54 64 69 3eqtr2d 
 |-  ( ( ( ph /\ ( i e. M /\ k e. P ) ) /\ j e. O ) -> ( ( i ( X F Y ) j ) ( .r ` R ) ( j Z k ) ) = ( R gsum ( l e. N |-> ( ( i X l ) ( .r ` R ) ( ( l Y j ) ( .r ` R ) ( j Z k ) ) ) ) ) )
71 70 mpteq2dva 
 |-  ( ( ph /\ ( i e. M /\ k e. P ) ) -> ( j e. O |-> ( ( i ( X F Y ) j ) ( .r ` R ) ( j Z k ) ) ) = ( j e. O |-> ( R gsum ( l e. N |-> ( ( i X l ) ( .r ` R ) ( ( l Y j ) ( .r ` R ) ( j Z k ) ) ) ) ) ) )
72 71 oveq2d 
 |-  ( ( ph /\ ( i e. M /\ k e. P ) ) -> ( R gsum ( j e. O |-> ( ( i ( X F Y ) j ) ( .r ` R ) ( j Z k ) ) ) ) = ( R gsum ( j e. O |-> ( R gsum ( l e. N |-> ( ( i X l ) ( .r ` R ) ( ( l Y j ) ( .r ` R ) ( j Z k ) ) ) ) ) ) ) )
73 2 ad2antrr 
 |-  ( ( ( ph /\ ( i e. M /\ k e. P ) ) /\ l e. N ) -> R e. Ring )
74 4 ad2antrr 
 |-  ( ( ( ph /\ ( i e. M /\ k e. P ) ) /\ l e. N ) -> N e. Fin )
75 5 ad2antrr 
 |-  ( ( ( ph /\ ( i e. M /\ k e. P ) ) /\ l e. N ) -> O e. Fin )
76 6 ad2antrr 
 |-  ( ( ( ph /\ ( i e. M /\ k e. P ) ) /\ l e. N ) -> P e. Fin )
77 8 ad2antrr 
 |-  ( ( ( ph /\ ( i e. M /\ k e. P ) ) /\ l e. N ) -> Y e. ( B ^m ( N X. O ) ) )
78 9 ad2antrr 
 |-  ( ( ( ph /\ ( i e. M /\ k e. P ) ) /\ l e. N ) -> Z e. ( B ^m ( O X. P ) ) )
79 simplrr 
 |-  ( ( ( ph /\ ( i e. M /\ k e. P ) ) /\ l e. N ) -> k e. P )
80 13 1 40 73 74 75 76 77 78 24 79 mamufv 
 |-  ( ( ( ph /\ ( i e. M /\ k e. P ) ) /\ l e. N ) -> ( l ( Y I Z ) k ) = ( R gsum ( j e. O |-> ( ( l Y j ) ( .r ` R ) ( j Z k ) ) ) ) )
81 80 oveq2d 
 |-  ( ( ( ph /\ ( i e. M /\ k e. P ) ) /\ l e. N ) -> ( ( i X l ) ( .r ` R ) ( l ( Y I Z ) k ) ) = ( ( i X l ) ( .r ` R ) ( R gsum ( j e. O |-> ( ( l Y j ) ( .r ` R ) ( j Z k ) ) ) ) ) )
82 42 anass1rs 
 |-  ( ( ( ( ph /\ ( i e. M /\ k e. P ) ) /\ l e. N ) /\ j e. O ) -> ( ( l Y j ) ( .r ` R ) ( j Z k ) ) e. B )
83 eqid 
 |-  ( j e. O |-> ( ( l Y j ) ( .r ` R ) ( j Z k ) ) ) = ( j e. O |-> ( ( l Y j ) ( .r ` R ) ( j Z k ) ) )
84 ovexd 
 |-  ( ( ( ( ph /\ ( i e. M /\ k e. P ) ) /\ l e. N ) /\ j e. O ) -> ( ( l Y j ) ( .r ` R ) ( j Z k ) ) e. _V )
85 fvexd 
 |-  ( ( ( ph /\ ( i e. M /\ k e. P ) ) /\ l e. N ) -> ( 0g ` R ) e. _V )
86 83 75 84 85 fsuppmptdm 
 |-  ( ( ( ph /\ ( i e. M /\ k e. P ) ) /\ l e. N ) -> ( j e. O |-> ( ( l Y j ) ( .r ` R ) ( j Z k ) ) ) finSupp ( 0g ` R ) )
87 1 55 56 40 73 75 25 82 86 gsummulc2 
 |-  ( ( ( ph /\ ( i e. M /\ k e. P ) ) /\ l e. N ) -> ( R gsum ( j e. O |-> ( ( i X l ) ( .r ` R ) ( ( l Y j ) ( .r ` R ) ( j Z k ) ) ) ) ) = ( ( i X l ) ( .r ` R ) ( R gsum ( j e. O |-> ( ( l Y j ) ( .r ` R ) ( j Z k ) ) ) ) ) )
88 81 87 eqtr4d 
 |-  ( ( ( ph /\ ( i e. M /\ k e. P ) ) /\ l e. N ) -> ( ( i X l ) ( .r ` R ) ( l ( Y I Z ) k ) ) = ( R gsum ( j e. O |-> ( ( i X l ) ( .r ` R ) ( ( l Y j ) ( .r ` R ) ( j Z k ) ) ) ) ) )
89 88 mpteq2dva 
 |-  ( ( ph /\ ( i e. M /\ k e. P ) ) -> ( l e. N |-> ( ( i X l ) ( .r ` R ) ( l ( Y I Z ) k ) ) ) = ( l e. N |-> ( R gsum ( j e. O |-> ( ( i X l ) ( .r ` R ) ( ( l Y j ) ( .r ` R ) ( j Z k ) ) ) ) ) ) )
90 89 oveq2d 
 |-  ( ( ph /\ ( i e. M /\ k e. P ) ) -> ( R gsum ( l e. N |-> ( ( i X l ) ( .r ` R ) ( l ( Y I Z ) k ) ) ) ) = ( R gsum ( l e. N |-> ( R gsum ( j e. O |-> ( ( i X l ) ( .r ` R ) ( ( l Y j ) ( .r ` R ) ( j Z k ) ) ) ) ) ) ) )
91 45 72 90 3eqtr4d 
 |-  ( ( ph /\ ( i e. M /\ k e. P ) ) -> ( R gsum ( j e. O |-> ( ( i ( X F Y ) j ) ( .r ` R ) ( j Z k ) ) ) ) = ( R gsum ( l e. N |-> ( ( i X l ) ( .r ` R ) ( l ( Y I Z ) k ) ) ) ) )
92 2 adantr 
 |-  ( ( ph /\ ( i e. M /\ k e. P ) ) -> R e. Ring )
93 3 adantr 
 |-  ( ( ph /\ ( i e. M /\ k e. P ) ) -> M e. Fin )
94 6 adantr 
 |-  ( ( ph /\ ( i e. M /\ k e. P ) ) -> P e. Fin )
95 1 2 10 3 4 5 7 8 mamucl 
 |-  ( ph -> ( X F Y ) e. ( B ^m ( M X. O ) ) )
96 95 adantr 
 |-  ( ( ph /\ ( i e. M /\ k e. P ) ) -> ( X F Y ) e. ( B ^m ( M X. O ) ) )
97 9 adantr 
 |-  ( ( ph /\ ( i e. M /\ k e. P ) ) -> Z e. ( B ^m ( O X. P ) ) )
98 simprl 
 |-  ( ( ph /\ ( i e. M /\ k e. P ) ) -> i e. M )
99 simprr 
 |-  ( ( ph /\ ( i e. M /\ k e. P ) ) -> k e. P )
100 11 1 40 92 93 17 94 96 97 98 99 mamufv 
 |-  ( ( ph /\ ( i e. M /\ k e. P ) ) -> ( i ( ( X F Y ) G Z ) k ) = ( R gsum ( j e. O |-> ( ( i ( X F Y ) j ) ( .r ` R ) ( j Z k ) ) ) ) )
101 7 adantr 
 |-  ( ( ph /\ ( i e. M /\ k e. P ) ) -> X e. ( B ^m ( M X. N ) ) )
102 1 2 13 4 5 6 8 9 mamucl 
 |-  ( ph -> ( Y I Z ) e. ( B ^m ( N X. P ) ) )
103 102 adantr 
 |-  ( ( ph /\ ( i e. M /\ k e. P ) ) -> ( Y I Z ) e. ( B ^m ( N X. P ) ) )
104 12 1 40 92 93 18 94 101 103 98 99 mamufv 
 |-  ( ( ph /\ ( i e. M /\ k e. P ) ) -> ( i ( X H ( Y I Z ) ) k ) = ( R gsum ( l e. N |-> ( ( i X l ) ( .r ` R ) ( l ( Y I Z ) k ) ) ) ) )
105 91 100 104 3eqtr4d 
 |-  ( ( ph /\ ( i e. M /\ k e. P ) ) -> ( i ( ( X F Y ) G Z ) k ) = ( i ( X H ( Y I Z ) ) k ) )
106 105 ralrimivva 
 |-  ( ph -> A. i e. M A. k e. P ( i ( ( X F Y ) G Z ) k ) = ( i ( X H ( Y I Z ) ) k ) )
107 1 2 11 3 5 6 95 9 mamucl 
 |-  ( ph -> ( ( X F Y ) G Z ) e. ( B ^m ( M X. P ) ) )
108 elmapi 
 |-  ( ( ( X F Y ) G Z ) e. ( B ^m ( M X. P ) ) -> ( ( X F Y ) G Z ) : ( M X. P ) --> B )
109 ffn 
 |-  ( ( ( X F Y ) G Z ) : ( M X. P ) --> B -> ( ( X F Y ) G Z ) Fn ( M X. P ) )
110 107 108 109 3syl 
 |-  ( ph -> ( ( X F Y ) G Z ) Fn ( M X. P ) )
111 1 2 12 3 4 6 7 102 mamucl 
 |-  ( ph -> ( X H ( Y I Z ) ) e. ( B ^m ( M X. P ) ) )
112 elmapi 
 |-  ( ( X H ( Y I Z ) ) e. ( B ^m ( M X. P ) ) -> ( X H ( Y I Z ) ) : ( M X. P ) --> B )
113 ffn 
 |-  ( ( X H ( Y I Z ) ) : ( M X. P ) --> B -> ( X H ( Y I Z ) ) Fn ( M X. P ) )
114 111 112 113 3syl 
 |-  ( ph -> ( X H ( Y I Z ) ) Fn ( M X. P ) )
115 eqfnov2 
 |-  ( ( ( ( X F Y ) G Z ) Fn ( M X. P ) /\ ( X H ( Y I Z ) ) Fn ( M X. P ) ) -> ( ( ( X F Y ) G Z ) = ( X H ( Y I Z ) ) <-> A. i e. M A. k e. P ( i ( ( X F Y ) G Z ) k ) = ( i ( X H ( Y I Z ) ) k ) ) )
116 110 114 115 syl2anc 
 |-  ( ph -> ( ( ( X F Y ) G Z ) = ( X H ( Y I Z ) ) <-> A. i e. M A. k e. P ( i ( ( X F Y ) G Z ) k ) = ( i ( X H ( Y I Z ) ) k ) ) )
117 106 116 mpbird 
 |-  ( ph -> ( ( X F Y ) G Z ) = ( X H ( Y I Z ) ) )