Metamath Proof Explorer

Theorem scmatscmiddistr

Description: Distributive law for scalar and ring multiplication for scalar matrices expressed as multiplications of a scalar with the identity matrix. (Contributed by AV, 19-Dec-2019)

Ref Expression
Hypotheses scmatscmide.a 
|- A = ( N Mat R )
scmatscmide.b 
|- B = ( Base ` R )
scmatscmide.0 
|- .0. = ( 0g ` R )
scmatscmide.1 
|- .1. = ( 1r ` A )
scmatscmide.m 
|- .* = ( .s ` A )
scmatscmiddistr.t 
|- .x. = ( .r ` R )
scmatscmiddistr.m 
|- .X. = ( .r ` A )
Assertion scmatscmiddistr 
|- ( ( ( N e. Fin /\ R e. Ring ) /\ ( S e. B /\ T e. B ) ) -> ( ( S .* .1. ) .X. ( T .* .1. ) ) = ( ( S .x. T ) .* .1. ) )

Proof

Step Hyp Ref Expression
1 scmatscmide.a 
 |-  A = ( N Mat R )
2 scmatscmide.b 
 |-  B = ( Base ` R )
3 scmatscmide.0 
 |-  .0. = ( 0g ` R )
4 scmatscmide.1 
 |-  .1. = ( 1r ` A )
5 scmatscmide.m 
 |-  .* = ( .s ` A )
6 scmatscmiddistr.t 
 |-  .x. = ( .r ` R )
7 scmatscmiddistr.m 
 |-  .X. = ( .r ` A )
8 simprl 
 |-  ( ( ( N e. Fin /\ R e. Ring ) /\ ( S e. B /\ T e. B ) ) -> S e. B )
9 eqid 
 |-  ( Base ` A ) = ( Base ` A )
10 eqid 
 |-  ( N DMat R ) = ( N DMat R )
11 1 9 3 10 dmatid 
 |-  ( ( N e. Fin /\ R e. Ring ) -> ( 1r ` A ) e. ( N DMat R ) )
12 4 11 eqeltrid 
 |-  ( ( N e. Fin /\ R e. Ring ) -> .1. e. ( N DMat R ) )
13 12 adantr 
 |-  ( ( ( N e. Fin /\ R e. Ring ) /\ ( S e. B /\ T e. B ) ) -> .1. e. ( N DMat R ) )
14 8 13 jca 
 |-  ( ( ( N e. Fin /\ R e. Ring ) /\ ( S e. B /\ T e. B ) ) -> ( S e. B /\ .1. e. ( N DMat R ) ) )
15 2 1 9 5 10 dmatscmcl 
 |-  ( ( ( N e. Fin /\ R e. Ring ) /\ ( S e. B /\ .1. e. ( N DMat R ) ) ) -> ( S .* .1. ) e. ( N DMat R ) )
16 14 15 syldan 
 |-  ( ( ( N e. Fin /\ R e. Ring ) /\ ( S e. B /\ T e. B ) ) -> ( S .* .1. ) e. ( N DMat R ) )
17 simprr 
 |-  ( ( ( N e. Fin /\ R e. Ring ) /\ ( S e. B /\ T e. B ) ) -> T e. B )
18 17 13 jca 
 |-  ( ( ( N e. Fin /\ R e. Ring ) /\ ( S e. B /\ T e. B ) ) -> ( T e. B /\ .1. e. ( N DMat R ) ) )
19 2 1 9 5 10 dmatscmcl 
 |-  ( ( ( N e. Fin /\ R e. Ring ) /\ ( T e. B /\ .1. e. ( N DMat R ) ) ) -> ( T .* .1. ) e. ( N DMat R ) )
20 18 19 syldan 
 |-  ( ( ( N e. Fin /\ R e. Ring ) /\ ( S e. B /\ T e. B ) ) -> ( T .* .1. ) e. ( N DMat R ) )
21 16 20 jca 
 |-  ( ( ( N e. Fin /\ R e. Ring ) /\ ( S e. B /\ T e. B ) ) -> ( ( S .* .1. ) e. ( N DMat R ) /\ ( T .* .1. ) e. ( N DMat R ) ) )
22 7 oveqi 
 |-  ( ( S .* .1. ) .X. ( T .* .1. ) ) = ( ( S .* .1. ) ( .r ` A ) ( T .* .1. ) )
23 1 9 3 10 dmatmul 
 |-  ( ( ( N e. Fin /\ R e. Ring ) /\ ( ( S .* .1. ) e. ( N DMat R ) /\ ( T .* .1. ) e. ( N DMat R ) ) ) -> ( ( S .* .1. ) ( .r ` A ) ( T .* .1. ) ) = ( i e. N , j e. N |-> if ( i = j , ( ( i ( S .* .1. ) j ) ( .r ` R ) ( i ( T .* .1. ) j ) ) , .0. ) ) )
24 22 23 eqtrid 
 |-  ( ( ( N e. Fin /\ R e. Ring ) /\ ( ( S .* .1. ) e. ( N DMat R ) /\ ( T .* .1. ) e. ( N DMat R ) ) ) -> ( ( S .* .1. ) .X. ( T .* .1. ) ) = ( i e. N , j e. N |-> if ( i = j , ( ( i ( S .* .1. ) j ) ( .r ` R ) ( i ( T .* .1. ) j ) ) , .0. ) ) )
25 21 24 syldan 
 |-  ( ( ( N e. Fin /\ R e. Ring ) /\ ( S e. B /\ T e. B ) ) -> ( ( S .* .1. ) .X. ( T .* .1. ) ) = ( i e. N , j e. N |-> if ( i = j , ( ( i ( S .* .1. ) j ) ( .r ` R ) ( i ( T .* .1. ) j ) ) , .0. ) ) )
26 simpll 
 |-  ( ( ( N e. Fin /\ R e. Ring ) /\ ( S e. B /\ T e. B ) ) -> N e. Fin )
27 simplr 
 |-  ( ( ( N e. Fin /\ R e. Ring ) /\ ( S e. B /\ T e. B ) ) -> R e. Ring )
28 26 27 8 3jca 
 |-  ( ( ( N e. Fin /\ R e. Ring ) /\ ( S e. B /\ T e. B ) ) -> ( N e. Fin /\ R e. Ring /\ S e. B ) )
29 28 3ad2ant1 
 |-  ( ( ( ( N e. Fin /\ R e. Ring ) /\ ( S e. B /\ T e. B ) ) /\ i e. N /\ j e. N ) -> ( N e. Fin /\ R e. Ring /\ S e. B ) )
30 3simpc 
 |-  ( ( ( ( N e. Fin /\ R e. Ring ) /\ ( S e. B /\ T e. B ) ) /\ i e. N /\ j e. N ) -> ( i e. N /\ j e. N ) )
31 1 2 3 4 5 scmatscmide 
 |-  ( ( ( N e. Fin /\ R e. Ring /\ S e. B ) /\ ( i e. N /\ j e. N ) ) -> ( i ( S .* .1. ) j ) = if ( i = j , S , .0. ) )
32 29 30 31 syl2anc 
 |-  ( ( ( ( N e. Fin /\ R e. Ring ) /\ ( S e. B /\ T e. B ) ) /\ i e. N /\ j e. N ) -> ( i ( S .* .1. ) j ) = if ( i = j , S , .0. ) )
33 26 27 17 3jca 
 |-  ( ( ( N e. Fin /\ R e. Ring ) /\ ( S e. B /\ T e. B ) ) -> ( N e. Fin /\ R e. Ring /\ T e. B ) )
34 33 3ad2ant1 
 |-  ( ( ( ( N e. Fin /\ R e. Ring ) /\ ( S e. B /\ T e. B ) ) /\ i e. N /\ j e. N ) -> ( N e. Fin /\ R e. Ring /\ T e. B ) )
35 1 2 3 4 5 scmatscmide 
 |-  ( ( ( N e. Fin /\ R e. Ring /\ T e. B ) /\ ( i e. N /\ j e. N ) ) -> ( i ( T .* .1. ) j ) = if ( i = j , T , .0. ) )
36 34 30 35 syl2anc 
 |-  ( ( ( ( N e. Fin /\ R e. Ring ) /\ ( S e. B /\ T e. B ) ) /\ i e. N /\ j e. N ) -> ( i ( T .* .1. ) j ) = if ( i = j , T , .0. ) )
37 32 36 oveq12d 
 |-  ( ( ( ( N e. Fin /\ R e. Ring ) /\ ( S e. B /\ T e. B ) ) /\ i e. N /\ j e. N ) -> ( ( i ( S .* .1. ) j ) ( .r ` R ) ( i ( T .* .1. ) j ) ) = ( if ( i = j , S , .0. ) ( .r ` R ) if ( i = j , T , .0. ) ) )
38 37 ifeq1d 
 |-  ( ( ( ( N e. Fin /\ R e. Ring ) /\ ( S e. B /\ T e. B ) ) /\ i e. N /\ j e. N ) -> if ( i = j , ( ( i ( S .* .1. ) j ) ( .r ` R ) ( i ( T .* .1. ) j ) ) , .0. ) = if ( i = j , ( if ( i = j , S , .0. ) ( .r ` R ) if ( i = j , T , .0. ) ) , .0. ) )
39 38 mpoeq3dva 
 |-  ( ( ( N e. Fin /\ R e. Ring ) /\ ( S e. B /\ T e. B ) ) -> ( i e. N , j e. N |-> if ( i = j , ( ( i ( S .* .1. ) j ) ( .r ` R ) ( i ( T .* .1. ) j ) ) , .0. ) ) = ( i e. N , j e. N |-> if ( i = j , ( if ( i = j , S , .0. ) ( .r ` R ) if ( i = j , T , .0. ) ) , .0. ) ) )
40 iftrue 
 |-  ( i = j -> if ( i = j , S , .0. ) = S )
41 iftrue 
 |-  ( i = j -> if ( i = j , T , .0. ) = T )
42 40 41 oveq12d 
 |-  ( i = j -> ( if ( i = j , S , .0. ) ( .r ` R ) if ( i = j , T , .0. ) ) = ( S ( .r ` R ) T ) )
43 42 adantl 
 |-  ( ( ( ( ( N e. Fin /\ R e. Ring ) /\ ( S e. B /\ T e. B ) ) /\ i e. N /\ j e. N ) /\ i = j ) -> ( if ( i = j , S , .0. ) ( .r ` R ) if ( i = j , T , .0. ) ) = ( S ( .r ` R ) T ) )
44 43 ifeq1da 
 |-  ( ( ( ( N e. Fin /\ R e. Ring ) /\ ( S e. B /\ T e. B ) ) /\ i e. N /\ j e. N ) -> if ( i = j , ( if ( i = j , S , .0. ) ( .r ` R ) if ( i = j , T , .0. ) ) , .0. ) = if ( i = j , ( S ( .r ` R ) T ) , .0. ) )
45 44 mpoeq3dva 
 |-  ( ( ( N e. Fin /\ R e. Ring ) /\ ( S e. B /\ T e. B ) ) -> ( i e. N , j e. N |-> if ( i = j , ( if ( i = j , S , .0. ) ( .r ` R ) if ( i = j , T , .0. ) ) , .0. ) ) = ( i e. N , j e. N |-> if ( i = j , ( S ( .r ` R ) T ) , .0. ) ) )
46 eqidd 
 |-  ( ( ( ( N e. Fin /\ R e. Ring ) /\ ( S e. B /\ T e. B ) ) /\ ( x e. N /\ y e. N ) ) -> ( i e. N , j e. N |-> if ( i = j , ( S ( .r ` R ) T ) , .0. ) ) = ( i e. N , j e. N |-> if ( i = j , ( S ( .r ` R ) T ) , .0. ) ) )
47 eqeq12 
 |-  ( ( i = x /\ j = y ) -> ( i = j <-> x = y ) )
48 6 eqcomi 
 |-  ( .r ` R ) = .x.
49 48 oveqi 
 |-  ( S ( .r ` R ) T ) = ( S .x. T )
50 49 a1i 
 |-  ( ( i = x /\ j = y ) -> ( S ( .r ` R ) T ) = ( S .x. T ) )
51 47 50 ifbieq1d 
 |-  ( ( i = x /\ j = y ) -> if ( i = j , ( S ( .r ` R ) T ) , .0. ) = if ( x = y , ( S .x. T ) , .0. ) )
52 51 adantl 
 |-  ( ( ( ( ( N e. Fin /\ R e. Ring ) /\ ( S e. B /\ T e. B ) ) /\ ( x e. N /\ y e. N ) ) /\ ( i = x /\ j = y ) ) -> if ( i = j , ( S ( .r ` R ) T ) , .0. ) = if ( x = y , ( S .x. T ) , .0. ) )
53 simprl 
 |-  ( ( ( ( N e. Fin /\ R e. Ring ) /\ ( S e. B /\ T e. B ) ) /\ ( x e. N /\ y e. N ) ) -> x e. N )
54 simprr 
 |-  ( ( ( ( N e. Fin /\ R e. Ring ) /\ ( S e. B /\ T e. B ) ) /\ ( x e. N /\ y e. N ) ) -> y e. N )
55 ovex 
 |-  ( S .x. T ) e. _V
56 3 fvexi 
 |-  .0. e. _V
57 55 56 ifex 
 |-  if ( x = y , ( S .x. T ) , .0. ) e. _V
58 57 a1i 
 |-  ( ( ( ( N e. Fin /\ R e. Ring ) /\ ( S e. B /\ T e. B ) ) /\ ( x e. N /\ y e. N ) ) -> if ( x = y , ( S .x. T ) , .0. ) e. _V )
59 46 52 53 54 58 ovmpod 
 |-  ( ( ( ( N e. Fin /\ R e. Ring ) /\ ( S e. B /\ T e. B ) ) /\ ( x e. N /\ y e. N ) ) -> ( x ( i e. N , j e. N |-> if ( i = j , ( S ( .r ` R ) T ) , .0. ) ) y ) = if ( x = y , ( S .x. T ) , .0. ) )
60 27 8 17 3jca 
 |-  ( ( ( N e. Fin /\ R e. Ring ) /\ ( S e. B /\ T e. B ) ) -> ( R e. Ring /\ S e. B /\ T e. B ) )
61 2 6 ringcl 
 |-  ( ( R e. Ring /\ S e. B /\ T e. B ) -> ( S .x. T ) e. B )
62 60 61 syl 
 |-  ( ( ( N e. Fin /\ R e. Ring ) /\ ( S e. B /\ T e. B ) ) -> ( S .x. T ) e. B )
63 26 27 62 3jca 
 |-  ( ( ( N e. Fin /\ R e. Ring ) /\ ( S e. B /\ T e. B ) ) -> ( N e. Fin /\ R e. Ring /\ ( S .x. T ) e. B ) )
64 1 2 3 4 5 scmatscmide 
 |-  ( ( ( N e. Fin /\ R e. Ring /\ ( S .x. T ) e. B ) /\ ( x e. N /\ y e. N ) ) -> ( x ( ( S .x. T ) .* .1. ) y ) = if ( x = y , ( S .x. T ) , .0. ) )
65 63 64 sylan 
 |-  ( ( ( ( N e. Fin /\ R e. Ring ) /\ ( S e. B /\ T e. B ) ) /\ ( x e. N /\ y e. N ) ) -> ( x ( ( S .x. T ) .* .1. ) y ) = if ( x = y , ( S .x. T ) , .0. ) )
66 59 65 eqtr4d 
 |-  ( ( ( ( N e. Fin /\ R e. Ring ) /\ ( S e. B /\ T e. B ) ) /\ ( x e. N /\ y e. N ) ) -> ( x ( i e. N , j e. N |-> if ( i = j , ( S ( .r ` R ) T ) , .0. ) ) y ) = ( x ( ( S .x. T ) .* .1. ) y ) )
67 66 ralrimivva 
 |-  ( ( ( N e. Fin /\ R e. Ring ) /\ ( S e. B /\ T e. B ) ) -> A. x e. N A. y e. N ( x ( i e. N , j e. N |-> if ( i = j , ( S ( .r ` R ) T ) , .0. ) ) y ) = ( x ( ( S .x. T ) .* .1. ) y ) )
68 eqid 
 |-  ( .r ` R ) = ( .r ` R )
69 2 68 ringcl 
 |-  ( ( R e. Ring /\ S e. B /\ T e. B ) -> ( S ( .r ` R ) T ) e. B )
70 60 69 syl 
 |-  ( ( ( N e. Fin /\ R e. Ring ) /\ ( S e. B /\ T e. B ) ) -> ( S ( .r ` R ) T ) e. B )
71 2 3 ring0cl 
 |-  ( R e. Ring -> .0. e. B )
72 71 adantl 
 |-  ( ( N e. Fin /\ R e. Ring ) -> .0. e. B )
73 72 adantr 
 |-  ( ( ( N e. Fin /\ R e. Ring ) /\ ( S e. B /\ T e. B ) ) -> .0. e. B )
74 70 73 ifcld 
 |-  ( ( ( N e. Fin /\ R e. Ring ) /\ ( S e. B /\ T e. B ) ) -> if ( i = j , ( S ( .r ` R ) T ) , .0. ) e. B )
75 74 3ad2ant1 
 |-  ( ( ( ( N e. Fin /\ R e. Ring ) /\ ( S e. B /\ T e. B ) ) /\ i e. N /\ j e. N ) -> if ( i = j , ( S ( .r ` R ) T ) , .0. ) e. B )
76 1 2 9 26 27 75 matbas2d 
 |-  ( ( ( N e. Fin /\ R e. Ring ) /\ ( S e. B /\ T e. B ) ) -> ( i e. N , j e. N |-> if ( i = j , ( S ( .r ` R ) T ) , .0. ) ) e. ( Base ` A ) )
77 1 matring 
 |-  ( ( N e. Fin /\ R e. Ring ) -> A e. Ring )
78 9 4 ringidcl 
 |-  ( A e. Ring -> .1. e. ( Base ` A ) )
79 77 78 syl 
 |-  ( ( N e. Fin /\ R e. Ring ) -> .1. e. ( Base ` A ) )
80 79 adantr 
 |-  ( ( ( N e. Fin /\ R e. Ring ) /\ ( S e. B /\ T e. B ) ) -> .1. e. ( Base ` A ) )
81 62 80 jca 
 |-  ( ( ( N e. Fin /\ R e. Ring ) /\ ( S e. B /\ T e. B ) ) -> ( ( S .x. T ) e. B /\ .1. e. ( Base ` A ) ) )
82 2 1 9 5 matvscl 
 |-  ( ( ( N e. Fin /\ R e. Ring ) /\ ( ( S .x. T ) e. B /\ .1. e. ( Base ` A ) ) ) -> ( ( S .x. T ) .* .1. ) e. ( Base ` A ) )
83 81 82 syldan 
 |-  ( ( ( N e. Fin /\ R e. Ring ) /\ ( S e. B /\ T e. B ) ) -> ( ( S .x. T ) .* .1. ) e. ( Base ` A ) )
84 1 9 eqmat 
 |-  ( ( ( i e. N , j e. N |-> if ( i = j , ( S ( .r ` R ) T ) , .0. ) ) e. ( Base ` A ) /\ ( ( S .x. T ) .* .1. ) e. ( Base ` A ) ) -> ( ( i e. N , j e. N |-> if ( i = j , ( S ( .r ` R ) T ) , .0. ) ) = ( ( S .x. T ) .* .1. ) <-> A. x e. N A. y e. N ( x ( i e. N , j e. N |-> if ( i = j , ( S ( .r ` R ) T ) , .0. ) ) y ) = ( x ( ( S .x. T ) .* .1. ) y ) ) )
85 76 83 84 syl2anc 
 |-  ( ( ( N e. Fin /\ R e. Ring ) /\ ( S e. B /\ T e. B ) ) -> ( ( i e. N , j e. N |-> if ( i = j , ( S ( .r ` R ) T ) , .0. ) ) = ( ( S .x. T ) .* .1. ) <-> A. x e. N A. y e. N ( x ( i e. N , j e. N |-> if ( i = j , ( S ( .r ` R ) T ) , .0. ) ) y ) = ( x ( ( S .x. T ) .* .1. ) y ) ) )
86 67 85 mpbird 
 |-  ( ( ( N e. Fin /\ R e. Ring ) /\ ( S e. B /\ T e. B ) ) -> ( i e. N , j e. N |-> if ( i = j , ( S ( .r ` R ) T ) , .0. ) ) = ( ( S .x. T ) .* .1. ) )
87 45 86 eqtrd 
 |-  ( ( ( N e. Fin /\ R e. Ring ) /\ ( S e. B /\ T e. B ) ) -> ( i e. N , j e. N |-> if ( i = j , ( if ( i = j , S , .0. ) ( .r ` R ) if ( i = j , T , .0. ) ) , .0. ) ) = ( ( S .x. T ) .* .1. ) )
88 39 87 eqtrd 
 |-  ( ( ( N e. Fin /\ R e. Ring ) /\ ( S e. B /\ T e. B ) ) -> ( i e. N , j e. N |-> if ( i = j , ( ( i ( S .* .1. ) j ) ( .r ` R ) ( i ( T .* .1. ) j ) ) , .0. ) ) = ( ( S .x. T ) .* .1. ) )
89 25 88 eqtrd 
 |-  ( ( ( N e. Fin /\ R e. Ring ) /\ ( S e. B /\ T e. B ) ) -> ( ( S .* .1. ) .X. ( T .* .1. ) ) = ( ( S .x. T ) .* .1. ) )