Metamath Proof Explorer

Theorem mpomatmul

Description: Multiplication of two N x N matrices given in maps-to notation. (Contributed by AV, 29-Oct-2019)

Ref Expression
Hypotheses mpomatmul.a 
|- A = ( N Mat R )
mpomatmul.b 
|- B = ( Base ` R )
mpomatmul.m 
|- .X. = ( .r ` A )
mpomatmul.t 
|- .x. = ( .r ` R )
mpomatmul.r 
|- ( ph -> R e. V )
mpomatmul.n 
|- ( ph -> N e. Fin )
mpomatmul.x 
|- X = ( i e. N , j e. N |-> C )
mpomatmul.y 
|- Y = ( i e. N , j e. N |-> E )
mpomatmul.c 
|- ( ( ph /\ i e. N /\ j e. N ) -> C e. B )
mpomatmul.e 
|- ( ( ph /\ i e. N /\ j e. N ) -> E e. B )
mpomatmul.d 
|- ( ( ph /\ ( k = i /\ m = j ) ) -> D = C )
mpomatmul.f 
|- ( ( ph /\ ( m = i /\ l = j ) ) -> F = E )
mpomatmul.1 
|- ( ( ph /\ k e. N /\ m e. N ) -> D e. U )
mpomatmul.2 
|- ( ( ph /\ m e. N /\ l e. N ) -> F e. W )
Assertion mpomatmul 
|- ( ph -> ( X .X. Y ) = ( k e. N , l e. N |-> ( R gsum ( m e. N |-> ( D .x. F ) ) ) ) )

Proof

Step Hyp Ref Expression
1 mpomatmul.a 
 |-  A = ( N Mat R )
2 mpomatmul.b 
 |-  B = ( Base ` R )
3 mpomatmul.m 
 |-  .X. = ( .r ` A )
4 mpomatmul.t 
 |-  .x. = ( .r ` R )
5 mpomatmul.r 
 |-  ( ph -> R e. V )
6 mpomatmul.n 
 |-  ( ph -> N e. Fin )
7 mpomatmul.x 
 |-  X = ( i e. N , j e. N |-> C )
8 mpomatmul.y 
 |-  Y = ( i e. N , j e. N |-> E )
9 mpomatmul.c 
 |-  ( ( ph /\ i e. N /\ j e. N ) -> C e. B )
10 mpomatmul.e 
 |-  ( ( ph /\ i e. N /\ j e. N ) -> E e. B )
11 mpomatmul.d 
 |-  ( ( ph /\ ( k = i /\ m = j ) ) -> D = C )
12 mpomatmul.f 
 |-  ( ( ph /\ ( m = i /\ l = j ) ) -> F = E )
13 mpomatmul.1 
 |-  ( ( ph /\ k e. N /\ m e. N ) -> D e. U )
14 mpomatmul.2 
 |-  ( ( ph /\ m e. N /\ l e. N ) -> F e. W )
15 eqid 
 |-  ( R maMul <. N , N , N >. ) = ( R maMul <. N , N , N >. )
16 1 15 matmulr 
 |-  ( ( N e. Fin /\ R e. V ) -> ( R maMul <. N , N , N >. ) = ( .r ` A ) )
17 16 3 eqtr4di 
 |-  ( ( N e. Fin /\ R e. V ) -> ( R maMul <. N , N , N >. ) = .X. )
18 17 oveqd 
 |-  ( ( N e. Fin /\ R e. V ) -> ( X ( R maMul <. N , N , N >. ) Y ) = ( X .X. Y ) )
19 18 eqcomd 
 |-  ( ( N e. Fin /\ R e. V ) -> ( X .X. Y ) = ( X ( R maMul <. N , N , N >. ) Y ) )
20 6 5 19 syl2anc 
 |-  ( ph -> ( X .X. Y ) = ( X ( R maMul <. N , N , N >. ) Y ) )
21 eqid 
 |-  ( Base ` R ) = ( Base ` R )
22 eqid 
 |-  ( Base ` A ) = ( Base ` A )
23 9 2 eleqtrdi 
 |-  ( ( ph /\ i e. N /\ j e. N ) -> C e. ( Base ` R ) )
24 1 21 22 6 5 23 matbas2d 
 |-  ( ph -> ( i e. N , j e. N |-> C ) e. ( Base ` A ) )
25 7 24 eqeltrid 
 |-  ( ph -> X e. ( Base ` A ) )
26 1 21 matbas2 
 |-  ( ( N e. Fin /\ R e. V ) -> ( ( Base ` R ) ^m ( N X. N ) ) = ( Base ` A ) )
27 6 5 26 syl2anc 
 |-  ( ph -> ( ( Base ` R ) ^m ( N X. N ) ) = ( Base ` A ) )
28 25 27 eleqtrrd 
 |-  ( ph -> X e. ( ( Base ` R ) ^m ( N X. N ) ) )
29 10 2 eleqtrdi 
 |-  ( ( ph /\ i e. N /\ j e. N ) -> E e. ( Base ` R ) )
30 1 21 22 6 5 29 matbas2d 
 |-  ( ph -> ( i e. N , j e. N |-> E ) e. ( Base ` A ) )
31 8 30 eqeltrid 
 |-  ( ph -> Y e. ( Base ` A ) )
32 31 27 eleqtrrd 
 |-  ( ph -> Y e. ( ( Base ` R ) ^m ( N X. N ) ) )
33 15 21 4 5 6 6 6 28 32 mamuval 
 |-  ( ph -> ( X ( R maMul <. N , N , N >. ) Y ) = ( k e. N , l e. N |-> ( R gsum ( m e. N |-> ( ( k X m ) .x. ( m Y l ) ) ) ) ) )
34 7 a1i 
 |-  ( ( ( ph /\ k e. N /\ l e. N ) /\ m e. N ) -> X = ( i e. N , j e. N |-> C ) )
35 equcom 
 |-  ( i = k <-> k = i )
36 equcom 
 |-  ( j = m <-> m = j )
37 35 36 anbi12i 
 |-  ( ( i = k /\ j = m ) <-> ( k = i /\ m = j ) )
38 37 11 sylan2b 
 |-  ( ( ph /\ ( i = k /\ j = m ) ) -> D = C )
39 38 eqcomd 
 |-  ( ( ph /\ ( i = k /\ j = m ) ) -> C = D )
40 39 ex 
 |-  ( ph -> ( ( i = k /\ j = m ) -> C = D ) )
41 40 3ad2ant1 
 |-  ( ( ph /\ k e. N /\ l e. N ) -> ( ( i = k /\ j = m ) -> C = D ) )
42 41 adantr 
 |-  ( ( ( ph /\ k e. N /\ l e. N ) /\ m e. N ) -> ( ( i = k /\ j = m ) -> C = D ) )
43 42 imp 
 |-  ( ( ( ( ph /\ k e. N /\ l e. N ) /\ m e. N ) /\ ( i = k /\ j = m ) ) -> C = D )
44 simpl2 
 |-  ( ( ( ph /\ k e. N /\ l e. N ) /\ m e. N ) -> k e. N )
45 simpr 
 |-  ( ( ( ph /\ k e. N /\ l e. N ) /\ m e. N ) -> m e. N )
46 simpl1 
 |-  ( ( ( ph /\ k e. N /\ l e. N ) /\ m e. N ) -> ph )
47 46 44 45 13 syl3anc 
 |-  ( ( ( ph /\ k e. N /\ l e. N ) /\ m e. N ) -> D e. U )
48 34 43 44 45 47 ovmpod 
 |-  ( ( ( ph /\ k e. N /\ l e. N ) /\ m e. N ) -> ( k X m ) = D )
49 8 a1i 
 |-  ( ( ( ph /\ k e. N /\ l e. N ) /\ m e. N ) -> Y = ( i e. N , j e. N |-> E ) )
50 equcomi 
 |-  ( i = m -> m = i )
51 equcomi 
 |-  ( j = l -> l = j )
52 50 51 anim12i 
 |-  ( ( i = m /\ j = l ) -> ( m = i /\ l = j ) )
53 52 12 sylan2 
 |-  ( ( ph /\ ( i = m /\ j = l ) ) -> F = E )
54 53 ex 
 |-  ( ph -> ( ( i = m /\ j = l ) -> F = E ) )
55 54 3ad2ant1 
 |-  ( ( ph /\ k e. N /\ l e. N ) -> ( ( i = m /\ j = l ) -> F = E ) )
56 55 adantr 
 |-  ( ( ( ph /\ k e. N /\ l e. N ) /\ m e. N ) -> ( ( i = m /\ j = l ) -> F = E ) )
57 56 imp 
 |-  ( ( ( ( ph /\ k e. N /\ l e. N ) /\ m e. N ) /\ ( i = m /\ j = l ) ) -> F = E )
58 57 eqcomd 
 |-  ( ( ( ( ph /\ k e. N /\ l e. N ) /\ m e. N ) /\ ( i = m /\ j = l ) ) -> E = F )
59 simpl3 
 |-  ( ( ( ph /\ k e. N /\ l e. N ) /\ m e. N ) -> l e. N )
60 46 45 59 14 syl3anc 
 |-  ( ( ( ph /\ k e. N /\ l e. N ) /\ m e. N ) -> F e. W )
61 49 58 45 59 60 ovmpod 
 |-  ( ( ( ph /\ k e. N /\ l e. N ) /\ m e. N ) -> ( m Y l ) = F )
62 48 61 oveq12d 
 |-  ( ( ( ph /\ k e. N /\ l e. N ) /\ m e. N ) -> ( ( k X m ) .x. ( m Y l ) ) = ( D .x. F ) )
63 62 mpteq2dva 
 |-  ( ( ph /\ k e. N /\ l e. N ) -> ( m e. N |-> ( ( k X m ) .x. ( m Y l ) ) ) = ( m e. N |-> ( D .x. F ) ) )
64 63 oveq2d 
 |-  ( ( ph /\ k e. N /\ l e. N ) -> ( R gsum ( m e. N |-> ( ( k X m ) .x. ( m Y l ) ) ) ) = ( R gsum ( m e. N |-> ( D .x. F ) ) ) )
65 64 mpoeq3dva 
 |-  ( ph -> ( k e. N , l e. N |-> ( R gsum ( m e. N |-> ( ( k X m ) .x. ( m Y l ) ) ) ) ) = ( k e. N , l e. N |-> ( R gsum ( m e. N |-> ( D .x. F ) ) ) ) )
66 20 33 65 3eqtrd 
 |-  ( ph -> ( X .X. Y ) = ( k e. N , l e. N |-> ( R gsum ( m e. N |-> ( D .x. F ) ) ) ) )