Metamath Proof Explorer

Theorem dmatmulcl

Description: The product of two diagonal matrices is a diagonal matrix. (Contributed by AV, 20-Aug-2019) (Revised by AV, 18-Dec-2019)

Ref Expression
Hypotheses dmatid.a 
|- A = ( N Mat R )
dmatid.b 
|- B = ( Base ` A )
dmatid.0 
|- .0. = ( 0g ` R )
dmatid.d 
|- D = ( N DMat R )
Assertion dmatmulcl 
|- ( ( ( N e. Fin /\ R e. Ring ) /\ ( X e. D /\ Y e. D ) ) -> ( X ( .r ` A ) Y ) e. D )

Proof

Step Hyp Ref Expression
1 dmatid.a 
 |-  A = ( N Mat R )
2 dmatid.b 
 |-  B = ( Base ` A )
3 dmatid.0 
 |-  .0. = ( 0g ` R )
4 dmatid.d 
 |-  D = ( N DMat R )
5 oveq 
 |-  ( m = ( x e. N , y e. N |-> if ( x = y , ( ( x X y ) ( .r ` R ) ( x Y y ) ) , .0. ) ) -> ( i m j ) = ( i ( x e. N , y e. N |-> if ( x = y , ( ( x X y ) ( .r ` R ) ( x Y y ) ) , .0. ) ) j ) )
6 5 eqeq1d 
 |-  ( m = ( x e. N , y e. N |-> if ( x = y , ( ( x X y ) ( .r ` R ) ( x Y y ) ) , .0. ) ) -> ( ( i m j ) = .0. <-> ( i ( x e. N , y e. N |-> if ( x = y , ( ( x X y ) ( .r ` R ) ( x Y y ) ) , .0. ) ) j ) = .0. ) )
7 6 imbi2d 
 |-  ( m = ( x e. N , y e. N |-> if ( x = y , ( ( x X y ) ( .r ` R ) ( x Y y ) ) , .0. ) ) -> ( ( i =/= j -> ( i m j ) = .0. ) <-> ( i =/= j -> ( i ( x e. N , y e. N |-> if ( x = y , ( ( x X y ) ( .r ` R ) ( x Y y ) ) , .0. ) ) j ) = .0. ) ) )
8 7 2ralbidv 
 |-  ( m = ( x e. N , y e. N |-> if ( x = y , ( ( x X y ) ( .r ` R ) ( x Y y ) ) , .0. ) ) -> ( A. i e. N A. j e. N ( i =/= j -> ( i m j ) = .0. ) <-> A. i e. N A. j e. N ( i =/= j -> ( i ( x e. N , y e. N |-> if ( x = y , ( ( x X y ) ( .r ` R ) ( x Y y ) ) , .0. ) ) j ) = .0. ) ) )
9 eqid 
 |-  ( Base ` R ) = ( Base ` R )
10 simpll 
 |-  ( ( ( N e. Fin /\ R e. Ring ) /\ ( X e. D /\ Y e. D ) ) -> N e. Fin )
11 simplr 
 |-  ( ( ( N e. Fin /\ R e. Ring ) /\ ( X e. D /\ Y e. D ) ) -> R e. Ring )
12 11 3ad2ant1 
 |-  ( ( ( ( N e. Fin /\ R e. Ring ) /\ ( X e. D /\ Y e. D ) ) /\ x e. N /\ y e. N ) -> R e. Ring )
13 eqid 
 |-  ( Base ` A ) = ( Base ` A )
14 simp2 
 |-  ( ( ( ( N e. Fin /\ R e. Ring ) /\ ( X e. D /\ Y e. D ) ) /\ x e. N /\ y e. N ) -> x e. N )
15 simp3 
 |-  ( ( ( ( N e. Fin /\ R e. Ring ) /\ ( X e. D /\ Y e. D ) ) /\ x e. N /\ y e. N ) -> y e. N )
16 1 13 3 4 dmatmat 
 |-  ( ( N e. Fin /\ R e. Ring ) -> ( X e. D -> X e. ( Base ` A ) ) )
17 16 imp 
 |-  ( ( ( N e. Fin /\ R e. Ring ) /\ X e. D ) -> X e. ( Base ` A ) )
18 17 adantrr 
 |-  ( ( ( N e. Fin /\ R e. Ring ) /\ ( X e. D /\ Y e. D ) ) -> X e. ( Base ` A ) )
19 18 3ad2ant1 
 |-  ( ( ( ( N e. Fin /\ R e. Ring ) /\ ( X e. D /\ Y e. D ) ) /\ x e. N /\ y e. N ) -> X e. ( Base ` A ) )
20 1 9 13 14 15 19 matecld 
 |-  ( ( ( ( N e. Fin /\ R e. Ring ) /\ ( X e. D /\ Y e. D ) ) /\ x e. N /\ y e. N ) -> ( x X y ) e. ( Base ` R ) )
21 1 13 3 4 dmatmat 
 |-  ( ( N e. Fin /\ R e. Ring ) -> ( Y e. D -> Y e. ( Base ` A ) ) )
22 21 imp 
 |-  ( ( ( N e. Fin /\ R e. Ring ) /\ Y e. D ) -> Y e. ( Base ` A ) )
23 22 adantrl 
 |-  ( ( ( N e. Fin /\ R e. Ring ) /\ ( X e. D /\ Y e. D ) ) -> Y e. ( Base ` A ) )
24 23 3ad2ant1 
 |-  ( ( ( ( N e. Fin /\ R e. Ring ) /\ ( X e. D /\ Y e. D ) ) /\ x e. N /\ y e. N ) -> Y e. ( Base ` A ) )
25 1 9 13 14 15 24 matecld 
 |-  ( ( ( ( N e. Fin /\ R e. Ring ) /\ ( X e. D /\ Y e. D ) ) /\ x e. N /\ y e. N ) -> ( x Y y ) e. ( Base ` R ) )
26 eqid 
 |-  ( .r ` R ) = ( .r ` R )
27 9 26 ringcl 
 |-  ( ( R e. Ring /\ ( x X y ) e. ( Base ` R ) /\ ( x Y y ) e. ( Base ` R ) ) -> ( ( x X y ) ( .r ` R ) ( x Y y ) ) e. ( Base ` R ) )
28 12 20 25 27 syl3anc 
 |-  ( ( ( ( N e. Fin /\ R e. Ring ) /\ ( X e. D /\ Y e. D ) ) /\ x e. N /\ y e. N ) -> ( ( x X y ) ( .r ` R ) ( x Y y ) ) e. ( Base ` R ) )
29 9 3 ring0cl 
 |-  ( R e. Ring -> .0. e. ( Base ` R ) )
30 29 adantl 
 |-  ( ( N e. Fin /\ R e. Ring ) -> .0. e. ( Base ` R ) )
31 30 adantr 
 |-  ( ( ( N e. Fin /\ R e. Ring ) /\ ( X e. D /\ Y e. D ) ) -> .0. e. ( Base ` R ) )
32 31 3ad2ant1 
 |-  ( ( ( ( N e. Fin /\ R e. Ring ) /\ ( X e. D /\ Y e. D ) ) /\ x e. N /\ y e. N ) -> .0. e. ( Base ` R ) )
33 28 32 ifcld 
 |-  ( ( ( ( N e. Fin /\ R e. Ring ) /\ ( X e. D /\ Y e. D ) ) /\ x e. N /\ y e. N ) -> if ( x = y , ( ( x X y ) ( .r ` R ) ( x Y y ) ) , .0. ) e. ( Base ` R ) )
34 1 9 2 10 11 33 matbas2d 
 |-  ( ( ( N e. Fin /\ R e. Ring ) /\ ( X e. D /\ Y e. D ) ) -> ( x e. N , y e. N |-> if ( x = y , ( ( x X y ) ( .r ` R ) ( x Y y ) ) , .0. ) ) e. B )
35 eqidd 
 |-  ( ( ( ( ( N e. Fin /\ R e. Ring ) /\ ( X e. D /\ Y e. D ) ) /\ ( i e. N /\ j e. N ) ) /\ i =/= j ) -> ( x e. N , y e. N |-> if ( x = y , ( ( x X y ) ( .r ` R ) ( x Y y ) ) , .0. ) ) = ( x e. N , y e. N |-> if ( x = y , ( ( x X y ) ( .r ` R ) ( x Y y ) ) , .0. ) ) )
36 eqeq12 
 |-  ( ( x = i /\ y = j ) -> ( x = y <-> i = j ) )
37 oveq12 
 |-  ( ( x = i /\ y = j ) -> ( x X y ) = ( i X j ) )
38 oveq12 
 |-  ( ( x = i /\ y = j ) -> ( x Y y ) = ( i Y j ) )
39 37 38 oveq12d 
 |-  ( ( x = i /\ y = j ) -> ( ( x X y ) ( .r ` R ) ( x Y y ) ) = ( ( i X j ) ( .r ` R ) ( i Y j ) ) )
40 36 39 ifbieq1d 
 |-  ( ( x = i /\ y = j ) -> if ( x = y , ( ( x X y ) ( .r ` R ) ( x Y y ) ) , .0. ) = if ( i = j , ( ( i X j ) ( .r ` R ) ( i Y j ) ) , .0. ) )
41 40 adantl 
 |-  ( ( ( ( ( ( N e. Fin /\ R e. Ring ) /\ ( X e. D /\ Y e. D ) ) /\ ( i e. N /\ j e. N ) ) /\ i =/= j ) /\ ( x = i /\ y = j ) ) -> if ( x = y , ( ( x X y ) ( .r ` R ) ( x Y y ) ) , .0. ) = if ( i = j , ( ( i X j ) ( .r ` R ) ( i Y j ) ) , .0. ) )
42 simplrl 
 |-  ( ( ( ( ( N e. Fin /\ R e. Ring ) /\ ( X e. D /\ Y e. D ) ) /\ ( i e. N /\ j e. N ) ) /\ i =/= j ) -> i e. N )
43 simplrr 
 |-  ( ( ( ( ( N e. Fin /\ R e. Ring ) /\ ( X e. D /\ Y e. D ) ) /\ ( i e. N /\ j e. N ) ) /\ i =/= j ) -> j e. N )
44 ovex 
 |-  ( ( i X j ) ( .r ` R ) ( i Y j ) ) e. _V
45 3 fvexi 
 |-  .0. e. _V
46 44 45 ifex 
 |-  if ( i = j , ( ( i X j ) ( .r ` R ) ( i Y j ) ) , .0. ) e. _V
47 46 a1i 
 |-  ( ( ( ( ( N e. Fin /\ R e. Ring ) /\ ( X e. D /\ Y e. D ) ) /\ ( i e. N /\ j e. N ) ) /\ i =/= j ) -> if ( i = j , ( ( i X j ) ( .r ` R ) ( i Y j ) ) , .0. ) e. _V )
48 35 41 42 43 47 ovmpod 
 |-  ( ( ( ( ( N e. Fin /\ R e. Ring ) /\ ( X e. D /\ Y e. D ) ) /\ ( i e. N /\ j e. N ) ) /\ i =/= j ) -> ( i ( x e. N , y e. N |-> if ( x = y , ( ( x X y ) ( .r ` R ) ( x Y y ) ) , .0. ) ) j ) = if ( i = j , ( ( i X j ) ( .r ` R ) ( i Y j ) ) , .0. ) )
49 ifnefalse 
 |-  ( i =/= j -> if ( i = j , ( ( i X j ) ( .r ` R ) ( i Y j ) ) , .0. ) = .0. )
50 49 adantl 
 |-  ( ( ( ( ( N e. Fin /\ R e. Ring ) /\ ( X e. D /\ Y e. D ) ) /\ ( i e. N /\ j e. N ) ) /\ i =/= j ) -> if ( i = j , ( ( i X j ) ( .r ` R ) ( i Y j ) ) , .0. ) = .0. )
51 48 50 eqtrd 
 |-  ( ( ( ( ( N e. Fin /\ R e. Ring ) /\ ( X e. D /\ Y e. D ) ) /\ ( i e. N /\ j e. N ) ) /\ i =/= j ) -> ( i ( x e. N , y e. N |-> if ( x = y , ( ( x X y ) ( .r ` R ) ( x Y y ) ) , .0. ) ) j ) = .0. )
52 51 ex 
 |-  ( ( ( ( N e. Fin /\ R e. Ring ) /\ ( X e. D /\ Y e. D ) ) /\ ( i e. N /\ j e. N ) ) -> ( i =/= j -> ( i ( x e. N , y e. N |-> if ( x = y , ( ( x X y ) ( .r ` R ) ( x Y y ) ) , .0. ) ) j ) = .0. ) )
53 52 ralrimivva 
 |-  ( ( ( N e. Fin /\ R e. Ring ) /\ ( X e. D /\ Y e. D ) ) -> A. i e. N A. j e. N ( i =/= j -> ( i ( x e. N , y e. N |-> if ( x = y , ( ( x X y ) ( .r ` R ) ( x Y y ) ) , .0. ) ) j ) = .0. ) )
54 8 34 53 elrabd 
 |-  ( ( ( N e. Fin /\ R e. Ring ) /\ ( X e. D /\ Y e. D ) ) -> ( x e. N , y e. N |-> if ( x = y , ( ( x X y ) ( .r ` R ) ( x Y y ) ) , .0. ) ) e. { m e. B | A. i e. N A. j e. N ( i =/= j -> ( i m j ) = .0. ) } )
55 1 2 3 4 dmatmul 
 |-  ( ( ( N e. Fin /\ R e. Ring ) /\ ( X e. D /\ Y e. D ) ) -> ( X ( .r ` A ) Y ) = ( x e. N , y e. N |-> if ( x = y , ( ( x X y ) ( .r ` R ) ( x Y y ) ) , .0. ) ) )
56 1 2 3 4 dmatval 
 |-  ( ( N e. Fin /\ R e. Ring ) -> D = { m e. B | A. i e. N A. j e. N ( i =/= j -> ( i m j ) = .0. ) } )
57 56 adantr 
 |-  ( ( ( N e. Fin /\ R e. Ring ) /\ ( X e. D /\ Y e. D ) ) -> D = { m e. B | A. i e. N A. j e. N ( i =/= j -> ( i m j ) = .0. ) } )
58 54 55 57 3eltr4d 
 |-  ( ( ( N e. Fin /\ R e. Ring ) /\ ( X e. D /\ Y e. D ) ) -> ( X ( .r ` A ) Y ) e. D )