MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  mamuvs1 Structured version   Visualization version   Unicode version
Theorem mamuvs1 20211
Description: Matrix multiplication distributes over scalar multiplication on the left. (Contributed by Stefan O'Rear, 5-Sep-2015.)
Hypotheses
Ref Expression
mamucl.b |- B = ( Base ` R )
mamucl.r |- ( ph -> R e. Ring )
mamudi.f |- F = ( R maMul <. M , N , O >. )
mamudi.m |- ( ph -> M e. Fin )
mamudi.n |- ( ph -> N e. Fin )
mamudi.o |- ( ph -> O e. Fin )
mamuvs1.t |- .x. = ( .r ` R )
mamuvs1.x |- ( ph -> X e. B )
mamuvs1.y |- ( ph -> Y e. ( B ^m ( M X. N ) ) )
mamuvs1.z |- ( ph -> Z e. ( B ^m ( N X. O ) ) )
Assertion
Ref Expression
mamuvs1 |- ( ph -> ( ( ( ( M X. N ) X. { X } ) oF .x. Y ) F Z ) = ( ( ( M X. O ) X. { X } ) oF .x. ( Y F Z ) ) )
Proof of Theorem mamuvs1
Dummy variables i k j are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 mamucl.b . . . . . 6 |- B = ( Base ` R )
2 eqid 2622 . . . . . 6 |- ( 0g ` R ) = ( 0g ` R )
3 eqid 2622 . . . . . 6 |- ( +g ` R ) = ( +g ` R )
4 mamuvs1.t . . . . . 6 |- .x. = ( .r ` R )
5 mamucl.r . . . . . . 7 |- ( ph -> R e. Ring )
65adantr 481 . . . . . 6 |- ( ( ph /\ ( i e. M /\ k e. O ) ) -> R e. Ring )
7 mamudi.n . . . . . . 7 |- ( ph -> N e. Fin )
87adantr 481 . . . . . 6 |- ( ( ph /\ ( i e. M /\ k e. O ) ) -> N e. Fin )
9 mamuvs1.x . . . . . . 7 |- ( ph -> X e. B )
109adantr 481 . . . . . 6 |- ( ( ph /\ ( i e. M /\ k e. O ) ) -> X e. B )
115ad2antrr 762 . . . . . . 7 |- ( ( ( ph /\ ( i e. M /\ k e. O ) ) /\ j e. N ) -> R e. Ring )
12 mamuvs1.y . . . . . . . . . 10 |- ( ph -> Y e. ( B ^m ( M X. N ) ) )
13 elmapi 7879 . . . . . . . . . 10 |- ( Y e. ( B ^m ( M X. N ) ) -> Y : ( M X. N ) --> B )
1412, 13syl 17 . . . . . . . . 9 |- ( ph -> Y : ( M X. N ) --> B )
1514ad2antrr 762 . . . . . . . 8 |- ( ( ( ph /\ ( i e. M /\ k e. O ) ) /\ j e. N ) -> Y : ( M X. N ) --> B )
16 simplrl 800 . . . . . . . 8 |- ( ( ( ph /\ ( i e. M /\ k e. O ) ) /\ j e. N ) -> i e. M )
17 simpr 477 . . . . . . . 8 |- ( ( ( ph /\ ( i e. M /\ k e. O ) ) /\ j e. N ) -> j e. N )
1815, 16, 17fovrnd 6806 . . . . . . 7 |- ( ( ( ph /\ ( i e. M /\ k e. O ) ) /\ j e. N ) -> ( i Y j ) e. B )
19 mamuvs1.z . . . . . . . . . 10 |- ( ph -> Z e. ( B ^m ( N X. O ) ) )
20 elmapi 7879 . . . . . . . . . 10 |- ( Z e. ( B ^m ( N X. O ) ) -> Z : ( N X. O ) --> B )
2119, 20syl 17 . . . . . . . . 9 |- ( ph -> Z : ( N X. O ) --> B )
2221ad2antrr 762 . . . . . . . 8 |- ( ( ( ph /\ ( i e. M /\ k e. O ) ) /\ j e. N ) -> Z : ( N X. O ) --> B )
23 simplrr 801 . . . . . . . 8 |- ( ( ( ph /\ ( i e. M /\ k e. O ) ) /\ j e. N ) -> k e. O )
2422, 17, 23fovrnd 6806 . . . . . . 7 |- ( ( ( ph /\ ( i e. M /\ k e. O ) ) /\ j e. N ) -> ( j Z k ) e. B )
251, 4ringcl 18561 . . . . . . 7 |- ( ( R e. Ring /\ ( i Y j ) e. B /\ ( j Z k ) e. B ) -> ( ( i Y j ) .x. ( j Z k ) ) e. B )
2611, 18, 24, 25syl3anc 1326 . . . . . 6 |- ( ( ( ph /\ ( i e. M /\ k e. O ) ) /\ j e. N ) -> ( ( i Y j ) .x. ( j Z k ) ) e. B )
27 eqid 2622 . . . . . . 7 |- ( j e. N |-> ( ( i Y j ) .x. ( j Z k ) ) ) = ( j e. N |-> ( ( i Y j ) .x. ( j Z k ) ) )
28 ovexd 6680 . . . . . . 7 |- ( ( ( ph /\ ( i e. M /\ k e. O ) ) /\ j e. N ) -> ( ( i Y j ) .x. ( j Z k ) ) e. _V )
29 fvexd 6203 . . . . . . 7 |- ( ( ph /\ ( i e. M /\ k e. O ) ) -> ( 0g ` R ) e. _V )
3027, 8, 28, 29fsuppmptdm 8286 . . . . . 6 |- ( ( ph /\ ( i e. M /\ k e. O ) ) -> ( j e. N |-> ( ( i Y j ) .x. ( j Z k ) ) ) finSupp ( 0g ` R ) )
311, 2, 3, 4, 6, 8, 10, 26, 30gsummulc2 18607 . . . . 5 |- ( ( ph /\ ( i e. M /\ k e. O ) ) -> ( R gsumg ( j e. N |-> ( X .x. ( ( i Y j ) .x. ( j Z k ) ) ) ) ) = ( X .x. ( R gsumg ( j e. N |-> ( ( i Y j ) .x. ( j Z k ) ) ) ) ) )
32 df-ov 6653 . . . . . . . . . 10 |- ( i ( ( ( M X. N ) X. { X } ) oF .x. Y ) j ) = ( ( ( ( M X. N ) X. { X } ) oF .x. Y ) ` <. i , j >. )
33 simprl 794 . . . . . . . . . . . 12 |- ( ( ph /\ ( i e. M /\ k e. O ) ) -> i e. M )
34 opelxpi 5148 . . . . . . . . . . . 12 |- ( ( i e. M /\ j e. N ) -> <. i , j >. e. ( M X. N ) )
3533, 34sylan 488 . . . . . . . . . . 11 |- ( ( ( ph /\ ( i e. M /\ k e. O ) ) /\ j e. N ) -> <. i , j >. e. ( M X. N ) )
36 mamudi.m . . . . . . . . . . . . . 14 |- ( ph -> M e. Fin )
37 xpfi 8231 . . . . . . . . . . . . . 14 |- ( ( M e. Fin /\ N e. Fin ) -> ( M X. N ) e. Fin )
3836, 7, 37syl2anc 693 . . . . . . . . . . . . 13 |- ( ph -> ( M X. N ) e. Fin )
3938ad2antrr 762 . . . . . . . . . . . 12 |- ( ( ( ph /\ ( i e. M /\ k e. O ) ) /\ j e. N ) -> ( M X. N ) e. Fin )
409ad2antrr 762 . . . . . . . . . . . 12 |- ( ( ( ph /\ ( i e. M /\ k e. O ) ) /\ j e. N ) -> X e. B )
41 ffn 6045 . . . . . . . . . . . . . 14 |- ( Y : ( M X. N ) --> B -> Y Fn ( M X. N ) )
4212, 13, 413syl 18 . . . . . . . . . . . . 13 |- ( ph -> Y Fn ( M X. N ) )
4342ad2antrr 762 . . . . . . . . . . . 12 |- ( ( ( ph /\ ( i e. M /\ k e. O ) ) /\ j e. N ) -> Y Fn ( M X. N ) )
44 df-ov 6653 . . . . . . . . . . . . . 14 |- ( i Y j ) = ( Y ` <. i , j >. )
4544eqcomi 2631 . . . . . . . . . . . . 13 |- ( Y ` <. i , j >. ) = ( i Y j )
4645a1i 11 . . . . . . . . . . . 12 |- ( ( ( ( ph /\ ( i e. M /\ k e. O ) ) /\ j e. N ) /\ <. i , j >. e. ( M X. N ) ) -> ( Y ` <. i , j >. ) = ( i Y j ) )
4739, 40, 43, 46ofc1 6920 . . . . . . . . . . 11 |- ( ( ( ( ph /\ ( i e. M /\ k e. O ) ) /\ j e. N ) /\ <. i , j >. e. ( M X. N ) ) -> ( ( ( ( M X. N ) X. { X } ) oF .x. Y ) ` <. i , j >. ) = ( X .x. ( i Y j ) ) )
4835, 47mpdan 702 . . . . . . . . . 10 |- ( ( ( ph /\ ( i e. M /\ k e. O ) ) /\ j e. N ) -> ( ( ( ( M X. N ) X. { X } ) oF .x. Y ) ` <. i , j >. ) = ( X .x. ( i Y j ) ) )
4932, 48syl5eq 2668 . . . . . . . . 9 |- ( ( ( ph /\ ( i e. M /\ k e. O ) ) /\ j e. N ) -> ( i ( ( ( M X. N ) X. { X } ) oF .x. Y ) j ) = ( X .x. ( i Y j ) ) )
5049oveq1d 6665 . . . . . . . 8 |- ( ( ( ph /\ ( i e. M /\ k e. O ) ) /\ j e. N ) -> ( ( i ( ( ( M X. N ) X. { X } ) oF .x. Y ) j ) .x. ( j Z k ) ) = ( ( X .x. ( i Y j ) ) .x. ( j Z k ) ) )
511, 4ringass 18564 . . . . . . . . 9 |- ( ( R e. Ring /\ ( X e. B /\ ( i Y j ) e. B /\ ( j Z k ) e. B ) ) -> ( ( X .x. ( i Y j ) ) .x. ( j Z k ) ) = ( X .x. ( ( i Y j ) .x. ( j Z k ) ) ) )
5211, 40, 18, 24, 51syl13anc 1328 . . . . . . . 8 |- ( ( ( ph /\ ( i e. M /\ k e. O ) ) /\ j e. N ) -> ( ( X .x. ( i Y j ) ) .x. ( j Z k ) ) = ( X .x. ( ( i Y j ) .x. ( j Z k ) ) ) )
5350, 52eqtrd 2656 . . . . . . 7 |- ( ( ( ph /\ ( i e. M /\ k e. O ) ) /\ j e. N ) -> ( ( i ( ( ( M X. N ) X. { X } ) oF .x. Y ) j ) .x. ( j Z k ) ) = ( X .x. ( ( i Y j ) .x. ( j Z k ) ) ) )
5453mpteq2dva 4744 . . . . . 6 |- ( ( ph /\ ( i e. M /\ k e. O ) ) -> ( j e. N |-> ( ( i ( ( ( M X. N ) X. { X } ) oF .x. Y ) j ) .x. ( j Z k ) ) ) = ( j e. N |-> ( X .x. ( ( i Y j ) .x. ( j Z k ) ) ) ) )
5554oveq2d 6666 . . . . 5 |- ( ( ph /\ ( i e. M /\ k e. O ) ) -> ( R gsumg ( j e. N |-> ( ( i ( ( ( M X. N ) X. { X } ) oF .x. Y ) j ) .x. ( j Z k ) ) ) ) = ( R gsumg ( j e. N |-> ( X .x. ( ( i Y j ) .x. ( j Z k ) ) ) ) ) )
56 mamudi.f . . . . . . 7 |- F = ( R maMul <. M , N , O >. )
5736adantr 481 . . . . . . 7 |- ( ( ph /\ ( i e. M /\ k e. O ) ) -> M e. Fin )
58 mamudi.o . . . . . . . 8 |- ( ph -> O e. Fin )
5958adantr 481 . . . . . . 7 |- ( ( ph /\ ( i e. M /\ k e. O ) ) -> O e. Fin )
6012adantr 481 . . . . . . 7 |- ( ( ph /\ ( i e. M /\ k e. O ) ) -> Y e. ( B ^m ( M X. N ) ) )
6119adantr 481 . . . . . . 7 |- ( ( ph /\ ( i e. M /\ k e. O ) ) -> Z e. ( B ^m ( N X. O ) ) )
62 simprr 796 . . . . . . 7 |- ( ( ph /\ ( i e. M /\ k e. O ) ) -> k e. O )
6356, 1, 4, 6, 57, 8, 59, 60, 61, 33, 62mamufv 20193 . . . . . 6 |- ( ( ph /\ ( i e. M /\ k e. O ) ) -> ( i ( Y F Z ) k ) = ( R gsumg ( j e. N |-> ( ( i Y j ) .x. ( j Z k ) ) ) ) )
6463oveq2d 6666 . . . . 5 |- ( ( ph /\ ( i e. M /\ k e. O ) ) -> ( X .x. ( i ( Y F Z ) k ) ) = ( X .x. ( R gsumg ( j e. N |-> ( ( i Y j ) .x. ( j Z k ) ) ) ) ) )
6531, 55, 643eqtr4d 2666 . . . 4 |- ( ( ph /\ ( i e. M /\ k e. O ) ) -> ( R gsumg ( j e. N |-> ( ( i ( ( ( M X. N ) X. { X } ) oF .x. Y ) j ) .x. ( j Z k ) ) ) ) = ( X .x. ( i ( Y F Z ) k ) ) )
66 fconst6g 6094 . . . . . . . . 9 |- ( X e. B -> ( ( M X. N ) X. { X } ) : ( M X. N ) --> B )
679, 66syl 17 . . . . . . . 8 |- ( ph -> ( ( M X. N ) X. { X } ) : ( M X. N ) --> B )
68 fvex 6201 . . . . . . . . . 10 |- ( Base ` R ) e. _V
691, 68eqeltri 2697 . . . . . . . . 9 |- B e. _V
70 elmapg 7870 . . . . . . . . 9 |- ( ( B e. _V /\ ( M X. N ) e. Fin ) -> ( ( ( M X. N ) X. { X } ) e. ( B ^m ( M X. N ) ) <-> ( ( M X. N ) X. { X } ) : ( M X. N ) --> B ) )
7169, 38, 70sylancr 695 . . . . . . . 8 |- ( ph -> ( ( ( M X. N ) X. { X } ) e. ( B ^m ( M X. N ) ) <-> ( ( M X. N ) X. { X } ) : ( M X. N ) --> B ) )
7267, 71mpbird 247 . . . . . . 7 |- ( ph -> ( ( M X. N ) X. { X } ) e. ( B ^m ( M X. N ) ) )
731, 4ringvcl 20204 . . . . . . 7 |- ( ( R e. Ring /\ ( ( M X. N ) X. { X } ) e. ( B ^m ( M X. N ) ) /\ Y e. ( B ^m ( M X. N ) ) ) -> ( ( ( M X. N ) X. { X } ) oF .x. Y ) e. ( B ^m ( M X. N ) ) )
745, 72, 12, 73syl3anc 1326 . . . . . 6 |- ( ph -> ( ( ( M X. N ) X. { X } ) oF .x. Y ) e. ( B ^m ( M X. N ) ) )
7574adantr 481 . . . . 5 |- ( ( ph /\ ( i e. M /\ k e. O ) ) -> ( ( ( M X. N ) X. { X } ) oF .x. Y ) e. ( B ^m ( M X. N ) ) )
7656, 1, 4, 6, 57, 8, 59, 75, 61, 33, 62mamufv 20193 . . . 4 |- ( ( ph /\ ( i e. M /\ k e. O ) ) -> ( i ( ( ( ( M X. N ) X. { X } ) oF .x. Y ) F Z ) k ) = ( R gsumg ( j e. N |-> ( ( i ( ( ( M X. N ) X. { X } ) oF .x. Y ) j ) .x. ( j Z k ) ) ) ) )
77 df-ov 6653 . . . . 5 |- ( i ( ( ( M X. O ) X. { X } ) oF .x. ( Y F Z ) ) k ) = ( ( ( ( M X. O ) X. { X } ) oF .x. ( Y F Z ) ) ` <. i , k >. )
78 opelxpi 5148 . . . . . . 7 |- ( ( i e. M /\ k e. O ) -> <. i , k >. e. ( M X. O ) )
7978adantl 482 . . . . . 6 |- ( ( ph /\ ( i e. M /\ k e. O ) ) -> <. i , k >. e. ( M X. O ) )
80 xpfi 8231 . . . . . . . . 9 |- ( ( M e. Fin /\ O e. Fin ) -> ( M X. O ) e. Fin )
8136, 58, 80syl2anc 693 . . . . . . . 8 |- ( ph -> ( M X. O ) e. Fin )
8281adantr 481 . . . . . . 7 |- ( ( ph /\ ( i e. M /\ k e. O ) ) -> ( M X. O ) e. Fin )
831, 5, 56, 36, 7, 58, 12, 19mamucl 20207 . . . . . . . . 9 |- ( ph -> ( Y F Z ) e. ( B ^m ( M X. O ) ) )
84 elmapi 7879 . . . . . . . . 9 |- ( ( Y F Z ) e. ( B ^m ( M X. O ) ) -> ( Y F Z ) : ( M X. O ) --> B )
85 ffn 6045 . . . . . . . . 9 |- ( ( Y F Z ) : ( M X. O ) --> B -> ( Y F Z ) Fn ( M X. O ) )
8683, 84, 853syl 18 . . . . . . . 8 |- ( ph -> ( Y F Z ) Fn ( M X. O ) )
8786adantr 481 . . . . . . 7 |- ( ( ph /\ ( i e. M /\ k e. O ) ) -> ( Y F Z ) Fn ( M X. O ) )
88 df-ov 6653 . . . . . . . . 9 |- ( i ( Y F Z ) k ) = ( ( Y F Z ) ` <. i , k >. )
8988eqcomi 2631 . . . . . . . 8 |- ( ( Y F Z ) ` <. i , k >. ) = ( i ( Y F Z ) k )
9089a1i 11 . . . . . . 7 |- ( ( ( ph /\ ( i e. M /\ k e. O ) ) /\ <. i , k >. e. ( M X. O ) ) -> ( ( Y F Z ) ` <. i , k >. ) = ( i ( Y F Z ) k ) )
9182, 10, 87, 90ofc1 6920 . . . . . 6 |- ( ( ( ph /\ ( i e. M /\ k e. O ) ) /\ <. i , k >. e. ( M X. O ) ) -> ( ( ( ( M X. O ) X. { X } ) oF .x. ( Y F Z ) ) ` <. i , k >. ) = ( X .x. ( i ( Y F Z ) k ) ) )
9279, 91mpdan 702 . . . . 5 |- ( ( ph /\ ( i e. M /\ k e. O ) ) -> ( ( ( ( M X. O ) X. { X } ) oF .x. ( Y F Z ) ) ` <. i , k >. ) = ( X .x. ( i ( Y F Z ) k ) ) )
9377, 92syl5eq 2668 . . . 4 |- ( ( ph /\ ( i e. M /\ k e. O ) ) -> ( i ( ( ( M X. O ) X. { X } ) oF .x. ( Y F Z ) ) k ) = ( X .x. ( i ( Y F Z ) k ) ) )
9465, 76, 933eqtr4d 2666 . . 3 |- ( ( ph /\ ( i e. M /\ k e. O ) ) -> ( i ( ( ( ( M X. N ) X. { X } ) oF .x. Y ) F Z ) k ) = ( i ( ( ( M X. O ) X. { X } ) oF .x. ( Y F Z ) ) k ) )
9594ralrimivva 2971 . 2 |- ( ph -> A. i e. M A. k e. O ( i ( ( ( ( M X. N ) X. { X } ) oF .x. Y ) F Z ) k ) = ( i ( ( ( M X. O ) X. { X } ) oF .x. ( Y F Z ) ) k ) )
961, 5, 56, 36, 7, 58, 74, 19mamucl 20207 . . . 4 |- ( ph -> ( ( ( ( M X. N ) X. { X } ) oF .x. Y ) F Z ) e. ( B ^m ( M X. O ) ) )
97 elmapi 7879 . . . 4 |- ( ( ( ( ( M X. N ) X. { X } ) oF .x. Y ) F Z ) e. ( B ^m ( M X. O ) ) -> ( ( ( ( M X. N ) X. { X } ) oF .x. Y ) F Z ) : ( M X. O ) --> B )
98 ffn 6045 . . . 4 |- ( ( ( ( ( M X. N ) X. { X } ) oF .x. Y ) F Z ) : ( M X. O ) --> B -> ( ( ( ( M X. N ) X. { X } ) oF .x. Y ) F Z ) Fn ( M X. O ) )
9996, 97, 983syl 18 . . 3 |- ( ph -> ( ( ( ( M X. N ) X. { X } ) oF .x. Y ) F Z ) Fn ( M X. O ) )
100 fconst6g 6094 . . . . . . 7 |- ( X e. B -> ( ( M X. O ) X. { X } ) : ( M X. O ) --> B )
1019, 100syl 17 . . . . . 6 |- ( ph -> ( ( M X. O ) X. { X } ) : ( M X. O ) --> B )
102 elmapg 7870 . . . . . . 7 |- ( ( B e. _V /\ ( M X. O ) e. Fin ) -> ( ( ( M X. O ) X. { X } ) e. ( B ^m ( M X. O ) ) <-> ( ( M X. O ) X. { X } ) : ( M X. O ) --> B ) )
10369, 81, 102sylancr 695 . . . . . 6 |- ( ph -> ( ( ( M X. O ) X. { X } ) e. ( B ^m ( M X. O ) ) <-> ( ( M X. O ) X. { X } ) : ( M X. O ) --> B ) )
104101, 103mpbird 247 . . . . 5 |- ( ph -> ( ( M X. O ) X. { X } ) e. ( B ^m ( M X. O ) ) )
1051, 4ringvcl 20204 . . . . 5 |- ( ( R e. Ring /\ ( ( M X. O ) X. { X } ) e. ( B ^m ( M X. O ) ) /\ ( Y F Z ) e. ( B ^m ( M X. O ) ) ) -> ( ( ( M X. O ) X. { X } ) oF .x. ( Y F Z ) ) e. ( B ^m ( M X. O ) ) )
1065, 104, 83, 105syl3anc 1326 . . . 4 |- ( ph -> ( ( ( M X. O ) X. { X } ) oF .x. ( Y F Z ) ) e. ( B ^m ( M X. O ) ) )
107 elmapi 7879 . . . 4 |- ( ( ( ( M X. O ) X. { X } ) oF .x. ( Y F Z ) ) e. ( B ^m ( M X. O ) ) -> ( ( ( M X. O ) X. { X } ) oF .x. ( Y F Z ) ) : ( M X. O ) --> B )
108 ffn 6045 . . . 4 |- ( ( ( ( M X. O ) X. { X } ) oF .x. ( Y F Z ) ) : ( M X. O ) --> B -> ( ( ( M X. O ) X. { X } ) oF .x. ( Y F Z ) ) Fn ( M X. O ) )
109106, 107, 1083syl 18 . . 3 |- ( ph -> ( ( ( M X. O ) X. { X } ) oF .x. ( Y F Z ) ) Fn ( M X. O ) )
110 eqfnov2 6767 . . 3 |- ( ( ( ( ( ( M X. N ) X. { X } ) oF .x. Y ) F Z ) Fn ( M X. O ) /\ ( ( ( M X. O ) X. { X } ) oF .x. ( Y F Z ) ) Fn ( M X. O ) ) -> ( ( ( ( ( M X. N ) X. { X } ) oF .x. Y ) F Z ) = ( ( ( M X. O ) X. { X } ) oF .x. ( Y F Z ) ) <-> A. i e. M A. k e. O ( i ( ( ( ( M X. N ) X. { X } ) oF .x. Y ) F Z ) k ) = ( i ( ( ( M X. O ) X. { X } ) oF .x. ( Y F Z ) ) k ) ) )
11199, 109, 110syl2anc 693 . 2 |- ( ph -> ( ( ( ( ( M X. N ) X. { X } ) oF .x. Y ) F Z ) = ( ( ( M X. O ) X. { X } ) oF .x. ( Y F Z ) ) <-> A. i e. M A. k e. O ( i ( ( ( ( M X. N ) X. { X } ) oF .x. Y ) F Z ) k ) = ( i ( ( ( M X. O ) X. { X } ) oF .x. ( Y F Z ) ) k ) ) )
11295, 111mpbird 247 1 |- ( ph -> ( ( ( ( M X. N ) X. { X } ) oF .x. Y ) F Z ) = ( ( ( M X. O ) X. { X } ) oF .x. ( Y F Z ) ) )
Colors of variables: wff setvar class
Syntax hints:   -> wi 4   <-> wb 196   /\ wa 384   = wceq 1483   e. wcel 1990   A.wral 2912   _Vcvv 3200   {csn 4177   <.cop 4183   <.cotp 4185   |-> cmpt 4729   X. cxp 5112   Fn wfn 5883   -->wf 5884   ` cfv 5888  (class class class)co 6650   oFcof 6895   ^m cmap 7857   Fincfn 7955   Basecbs 15857   +g cplusg 15941   .rcmulr 15942   0gc0g 16100   gsumg cgsu 16101   Ringcrg 18547   maMul cmmul 20189
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1722  ax-4 1737  ax-5 1839  ax-6 1888  ax-7 1935  ax-8 1992  ax-9 1999  ax-10 2019  ax-11 2034  ax-12 2047  ax-13 2246  ax-ext 2602  ax-rep 4771  ax-sep 4781  ax-nul 4789  ax-pow 4843  ax-pr 4906  ax-un 6949  ax-cnex 9992  ax-resscn 9993  ax-1cn 9994  ax-icn 9995  ax-addcl 9996  ax-addrcl 9997  ax-mulcl 9998  ax-mulrcl 9999  ax-mulcom 10000  ax-addass 10001  ax-mulass 10002  ax-distr 10003  ax-i2m1 10004  ax-1ne0 10005  ax-1rid 10006  ax-rnegex 10007  ax-rrecex 10008  ax-cnre 10009  ax-pre-lttri 10010  ax-pre-lttrn 10011  ax-pre-ltadd 10012  ax-pre-mulgt0 10013
This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-3or 1038  df-3an 1039  df-tru 1486  df-ex 1705  df-nf 1710  df-sb 1881  df-eu 2474  df-mo 2475  df-clab 2609  df-cleq 2615  df-clel 2618  df-nfc 2753  df-ne 2795  df-nel 2898  df-ral 2917  df-rex 2918  df-reu 2919  df-rmo 2920  df-rab 2921  df-v 3202  df-sbc 3436  df-csb 3534  df-dif 3577  df-un 3579  df-in 3581  df-ss 3588  df-pss 3590  df-nul 3916  df-if 4087  df-pw 4160  df-sn 4178  df-pr 4180  df-tp 4182  df-op 4184  df-ot 4186  df-uni 4437  df-int 4476  df-iun 4522  df-br 4654  df-opab 4713  df-mpt 4730  df-tr 4753  df-id 5024  df-eprel 5029  df-po 5035  df-so 5036  df-fr 5073  df-se 5074  df-we 5075  df-xp 5120  df-rel 5121  df-cnv 5122  df-co 5123  df-dm 5124  df-rn 5125  df-res 5126  df-ima 5127  df-pred 5680  df-ord 5726  df-on 5727  df-lim 5728  df-suc 5729  df-iota 5851  df-fun 5890  df-fn 5891  df-f 5892  df-f1 5893  df-fo 5894  df-f1o 5895  df-fv 5896  df-isom 5897  df-riota 6611  df-ov 6653  df-oprab 6654  df-mpt2 6655  df-of 6897  df-om 7066  df-1st 7168  df-2nd 7169  df-supp 7296  df-wrecs 7407  df-recs 7468  df-rdg 7506  df-1o 7560  df-oadd 7564  df-er 7742  df-map 7859  df-en 7956  df-dom 7957  df-sdom 7958  df-fin 7959  df-fsupp 8276  df-oi 8415  df-card 8765  df-pnf 10076  df-mnf 10077  df-xr 10078  df-ltxr 10079  df-le 10080  df-sub 10268  df-neg 10269  df-nn 11021  df-2 11079  df-n0 11293  df-z 11378  df-uz 11688  df-fz 12327  df-fzo 12466  df-seq 12802  df-hash 13118  df-ndx 15860  df-slot 15861  df-base 15863  df-sets 15864  df-plusg 15954  df-0g 16102  df-gsum 16103  df-mgm 17242  df-sgrp 17284  df-mnd 17295  df-mhm 17335  df-grp 17425  df-minusg 17426  df-ghm 17658  df-cntz 17750  df-cmn 18195  df-abl 18196  df-mgp 18490  df-ur 18502  df-ring 18549  df-mamu 20190
This theorem is referenced by:  matassa  20250  mdetmul  20429
  Copyright terms: Public domain W3C validator