Metamath Proof Explorer

Theorem evlslem4

Description: The support of a tensor product of ring element families is contained in the product of the supports. (Contributed by Stefan O'Rear, 8-Mar-2015) (Revised by AV, 18-Jul-2019)

Ref Expression
Hypotheses evlslem4.b 
|- B = ( Base ` R )
evlslem4.z 
|- .0. = ( 0g ` R )
evlslem4.t 
|- .x. = ( .r ` R )
evlslem4.r 
|- ( ph -> R e. Ring )
evlslem4.x 
|- ( ( ph /\ x e. I ) -> X e. B )
evlslem4.y 
|- ( ( ph /\ y e. J ) -> Y e. B )
evlslem4.i 
|- ( ph -> I e. V )
evlslem4.j 
|- ( ph -> J e. W )
Assertion evlslem4 
|- ( ph -> ( ( x e. I , y e. J |-> ( X .x. Y ) ) supp .0. ) C_ ( ( ( x e. I |-> X ) supp .0. ) X. ( ( y e. J |-> Y ) supp .0. ) ) )

Proof

Step Hyp Ref Expression
1 evlslem4.b 
 |-  B = ( Base ` R )
2 evlslem4.z 
 |-  .0. = ( 0g ` R )
3 evlslem4.t 
 |-  .x. = ( .r ` R )
4 evlslem4.r 
 |-  ( ph -> R e. Ring )
5 evlslem4.x 
 |-  ( ( ph /\ x e. I ) -> X e. B )
6 evlslem4.y 
 |-  ( ( ph /\ y e. J ) -> Y e. B )
7 evlslem4.i 
 |-  ( ph -> I e. V )
8 evlslem4.j 
 |-  ( ph -> J e. W )
9 nfcv 
 |-  F/_ i ( ( ( x e. I |-> X ) ` x ) .x. ( ( y e. J |-> Y ) ` y ) )
10 nfcv 
 |-  F/_ j ( ( ( x e. I |-> X ) ` x ) .x. ( ( y e. J |-> Y ) ` y ) )
11 nffvmpt1 
 |-  F/_ x ( ( x e. I |-> X ) ` i )
12 nfcv 
 |-  F/_ x .x.
13 nfcv 
 |-  F/_ x ( ( y e. J |-> Y ) ` j )
14 11 12 13 nfov 
 |-  F/_ x ( ( ( x e. I |-> X ) ` i ) .x. ( ( y e. J |-> Y ) ` j ) )
15 nfcv 
 |-  F/_ y ( ( x e. I |-> X ) ` i )
16 nfcv 
 |-  F/_ y .x.
17 nffvmpt1 
 |-  F/_ y ( ( y e. J |-> Y ) ` j )
18 15 16 17 nfov 
 |-  F/_ y ( ( ( x e. I |-> X ) ` i ) .x. ( ( y e. J |-> Y ) ` j ) )
19 fveq2 
 |-  ( x = i -> ( ( x e. I |-> X ) ` x ) = ( ( x e. I |-> X ) ` i ) )
20 fveq2 
 |-  ( y = j -> ( ( y e. J |-> Y ) ` y ) = ( ( y e. J |-> Y ) ` j ) )
21 19 20 oveqan12d 
 |-  ( ( x = i /\ y = j ) -> ( ( ( x e. I |-> X ) ` x ) .x. ( ( y e. J |-> Y ) ` y ) ) = ( ( ( x e. I |-> X ) ` i ) .x. ( ( y e. J |-> Y ) ` j ) ) )
22 9 10 14 18 21 cbvmpo 
 |-  ( x e. I , y e. J |-> ( ( ( x e. I |-> X ) ` x ) .x. ( ( y e. J |-> Y ) ` y ) ) ) = ( i e. I , j e. J |-> ( ( ( x e. I |-> X ) ` i ) .x. ( ( y e. J |-> Y ) ` j ) ) )
23 vex 
 |-  i e. _V
24 vex 
 |-  j e. _V
25 23 24 eqop2 
 |-  ( z = <. i , j >. <-> ( z e. ( _V X. _V ) /\ ( ( 1st ` z ) = i /\ ( 2nd ` z ) = j ) ) )
26 fveq2 
 |-  ( ( 1st ` z ) = i -> ( ( x e. I |-> X ) ` ( 1st ` z ) ) = ( ( x e. I |-> X ) ` i ) )
27 fveq2 
 |-  ( ( 2nd ` z ) = j -> ( ( y e. J |-> Y ) ` ( 2nd ` z ) ) = ( ( y e. J |-> Y ) ` j ) )
28 26 27 oveqan12d 
 |-  ( ( ( 1st ` z ) = i /\ ( 2nd ` z ) = j ) -> ( ( ( x e. I |-> X ) ` ( 1st ` z ) ) .x. ( ( y e. J |-> Y ) ` ( 2nd ` z ) ) ) = ( ( ( x e. I |-> X ) ` i ) .x. ( ( y e. J |-> Y ) ` j ) ) )
29 25 28 simplbiim 
 |-  ( z = <. i , j >. -> ( ( ( x e. I |-> X ) ` ( 1st ` z ) ) .x. ( ( y e. J |-> Y ) ` ( 2nd ` z ) ) ) = ( ( ( x e. I |-> X ) ` i ) .x. ( ( y e. J |-> Y ) ` j ) ) )
30 29 mpompt 
 |-  ( z e. ( I X. J ) |-> ( ( ( x e. I |-> X ) ` ( 1st ` z ) ) .x. ( ( y e. J |-> Y ) ` ( 2nd ` z ) ) ) ) = ( i e. I , j e. J |-> ( ( ( x e. I |-> X ) ` i ) .x. ( ( y e. J |-> Y ) ` j ) ) )
31 22 30 eqtr4i 
 |-  ( x e. I , y e. J |-> ( ( ( x e. I |-> X ) ` x ) .x. ( ( y e. J |-> Y ) ` y ) ) ) = ( z e. ( I X. J ) |-> ( ( ( x e. I |-> X ) ` ( 1st ` z ) ) .x. ( ( y e. J |-> Y ) ` ( 2nd ` z ) ) ) )
32 simp2 
 |-  ( ( ph /\ x e. I /\ y e. J ) -> x e. I )
33 5 3adant3 
 |-  ( ( ph /\ x e. I /\ y e. J ) -> X e. B )
34 eqid 
 |-  ( x e. I |-> X ) = ( x e. I |-> X )
35 34 fvmpt2 
 |-  ( ( x e. I /\ X e. B ) -> ( ( x e. I |-> X ) ` x ) = X )
36 32 33 35 syl2anc 
 |-  ( ( ph /\ x e. I /\ y e. J ) -> ( ( x e. I |-> X ) ` x ) = X )
37 simp3 
 |-  ( ( ph /\ x e. I /\ y e. J ) -> y e. J )
38 eqid 
 |-  ( y e. J |-> Y ) = ( y e. J |-> Y )
39 38 fvmpt2 
 |-  ( ( y e. J /\ Y e. B ) -> ( ( y e. J |-> Y ) ` y ) = Y )
40 37 6 39 3imp3i2an 
 |-  ( ( ph /\ x e. I /\ y e. J ) -> ( ( y e. J |-> Y ) ` y ) = Y )
41 36 40 oveq12d 
 |-  ( ( ph /\ x e. I /\ y e. J ) -> ( ( ( x e. I |-> X ) ` x ) .x. ( ( y e. J |-> Y ) ` y ) ) = ( X .x. Y ) )
42 41 mpoeq3dva 
 |-  ( ph -> ( x e. I , y e. J |-> ( ( ( x e. I |-> X ) ` x ) .x. ( ( y e. J |-> Y ) ` y ) ) ) = ( x e. I , y e. J |-> ( X .x. Y ) ) )
43 31 42 syl5reqr 
 |-  ( ph -> ( x e. I , y e. J |-> ( X .x. Y ) ) = ( z e. ( I X. J ) |-> ( ( ( x e. I |-> X ) ` ( 1st ` z ) ) .x. ( ( y e. J |-> Y ) ` ( 2nd ` z ) ) ) ) )
44 43 oveq1d 
 |-  ( ph -> ( ( x e. I , y e. J |-> ( X .x. Y ) ) supp .0. ) = ( ( z e. ( I X. J ) |-> ( ( ( x e. I |-> X ) ` ( 1st ` z ) ) .x. ( ( y e. J |-> Y ) ` ( 2nd ` z ) ) ) ) supp .0. ) )
45 difxp 
 |-  ( ( I X. J ) \ ( ( ( x e. I |-> X ) supp .0. ) X. ( ( y e. J |-> Y ) supp .0. ) ) ) = ( ( ( I \ ( ( x e. I |-> X ) supp .0. ) ) X. J ) u. ( I X. ( J \ ( ( y e. J |-> Y ) supp .0. ) ) ) )
46 45 eleq2i 
 |-  ( z e. ( ( I X. J ) \ ( ( ( x e. I |-> X ) supp .0. ) X. ( ( y e. J |-> Y ) supp .0. ) ) ) <-> z e. ( ( ( I \ ( ( x e. I |-> X ) supp .0. ) ) X. J ) u. ( I X. ( J \ ( ( y e. J |-> Y ) supp .0. ) ) ) ) )
47 elun 
 |-  ( z e. ( ( ( I \ ( ( x e. I |-> X ) supp .0. ) ) X. J ) u. ( I X. ( J \ ( ( y e. J |-> Y ) supp .0. ) ) ) ) <-> ( z e. ( ( I \ ( ( x e. I |-> X ) supp .0. ) ) X. J ) \/ z e. ( I X. ( J \ ( ( y e. J |-> Y ) supp .0. ) ) ) ) )
48 46 47 bitri 
 |-  ( z e. ( ( I X. J ) \ ( ( ( x e. I |-> X ) supp .0. ) X. ( ( y e. J |-> Y ) supp .0. ) ) ) <-> ( z e. ( ( I \ ( ( x e. I |-> X ) supp .0. ) ) X. J ) \/ z e. ( I X. ( J \ ( ( y e. J |-> Y ) supp .0. ) ) ) ) )
49 xp1st 
 |-  ( z e. ( ( I \ ( ( x e. I |-> X ) supp .0. ) ) X. J ) -> ( 1st ` z ) e. ( I \ ( ( x e. I |-> X ) supp .0. ) ) )
50 5 fmpttd 
 |-  ( ph -> ( x e. I |-> X ) : I --> B )
51 ssidd 
 |-  ( ph -> ( ( x e. I |-> X ) supp .0. ) C_ ( ( x e. I |-> X ) supp .0. ) )
52 2 fvexi 
 |-  .0. e. _V
53 52 a1i 
 |-  ( ph -> .0. e. _V )
54 50 51 7 53 suppssr 
 |-  ( ( ph /\ ( 1st ` z ) e. ( I \ ( ( x e. I |-> X ) supp .0. ) ) ) -> ( ( x e. I |-> X ) ` ( 1st ` z ) ) = .0. )
55 49 54 sylan2 
 |-  ( ( ph /\ z e. ( ( I \ ( ( x e. I |-> X ) supp .0. ) ) X. J ) ) -> ( ( x e. I |-> X ) ` ( 1st ` z ) ) = .0. )
56 55 oveq1d 
 |-  ( ( ph /\ z e. ( ( I \ ( ( x e. I |-> X ) supp .0. ) ) X. J ) ) -> ( ( ( x e. I |-> X ) ` ( 1st ` z ) ) .x. ( ( y e. J |-> Y ) ` ( 2nd ` z ) ) ) = ( .0. .x. ( ( y e. J |-> Y ) ` ( 2nd ` z ) ) ) )
57 6 fmpttd 
 |-  ( ph -> ( y e. J |-> Y ) : J --> B )
58 xp2nd 
 |-  ( z e. ( ( I \ ( ( x e. I |-> X ) supp .0. ) ) X. J ) -> ( 2nd ` z ) e. J )
59 ffvelrn 
 |-  ( ( ( y e. J |-> Y ) : J --> B /\ ( 2nd ` z ) e. J ) -> ( ( y e. J |-> Y ) ` ( 2nd ` z ) ) e. B )
60 57 58 59 syl2an 
 |-  ( ( ph /\ z e. ( ( I \ ( ( x e. I |-> X ) supp .0. ) ) X. J ) ) -> ( ( y e. J |-> Y ) ` ( 2nd ` z ) ) e. B )
61 1 3 2 ringlz 
 |-  ( ( R e. Ring /\ ( ( y e. J |-> Y ) ` ( 2nd ` z ) ) e. B ) -> ( .0. .x. ( ( y e. J |-> Y ) ` ( 2nd ` z ) ) ) = .0. )
62 4 60 61 syl2an2r 
 |-  ( ( ph /\ z e. ( ( I \ ( ( x e. I |-> X ) supp .0. ) ) X. J ) ) -> ( .0. .x. ( ( y e. J |-> Y ) ` ( 2nd ` z ) ) ) = .0. )
63 56 62 eqtrd 
 |-  ( ( ph /\ z e. ( ( I \ ( ( x e. I |-> X ) supp .0. ) ) X. J ) ) -> ( ( ( x e. I |-> X ) ` ( 1st ` z ) ) .x. ( ( y e. J |-> Y ) ` ( 2nd ` z ) ) ) = .0. )
64 xp2nd 
 |-  ( z e. ( I X. ( J \ ( ( y e. J |-> Y ) supp .0. ) ) ) -> ( 2nd ` z ) e. ( J \ ( ( y e. J |-> Y ) supp .0. ) ) )
65 ssidd 
 |-  ( ph -> ( ( y e. J |-> Y ) supp .0. ) C_ ( ( y e. J |-> Y ) supp .0. ) )
66 57 65 8 53 suppssr 
 |-  ( ( ph /\ ( 2nd ` z ) e. ( J \ ( ( y e. J |-> Y ) supp .0. ) ) ) -> ( ( y e. J |-> Y ) ` ( 2nd ` z ) ) = .0. )
67 64 66 sylan2 
 |-  ( ( ph /\ z e. ( I X. ( J \ ( ( y e. J |-> Y ) supp .0. ) ) ) ) -> ( ( y e. J |-> Y ) ` ( 2nd ` z ) ) = .0. )
68 67 oveq2d 
 |-  ( ( ph /\ z e. ( I X. ( J \ ( ( y e. J |-> Y ) supp .0. ) ) ) ) -> ( ( ( x e. I |-> X ) ` ( 1st ` z ) ) .x. ( ( y e. J |-> Y ) ` ( 2nd ` z ) ) ) = ( ( ( x e. I |-> X ) ` ( 1st ` z ) ) .x. .0. ) )
69 xp1st 
 |-  ( z e. ( I X. ( J \ ( ( y e. J |-> Y ) supp .0. ) ) ) -> ( 1st ` z ) e. I )
70 ffvelrn 
 |-  ( ( ( x e. I |-> X ) : I --> B /\ ( 1st ` z ) e. I ) -> ( ( x e. I |-> X ) ` ( 1st ` z ) ) e. B )
71 50 69 70 syl2an 
 |-  ( ( ph /\ z e. ( I X. ( J \ ( ( y e. J |-> Y ) supp .0. ) ) ) ) -> ( ( x e. I |-> X ) ` ( 1st ` z ) ) e. B )
72 1 3 2 ringrz 
 |-  ( ( R e. Ring /\ ( ( x e. I |-> X ) ` ( 1st ` z ) ) e. B ) -> ( ( ( x e. I |-> X ) ` ( 1st ` z ) ) .x. .0. ) = .0. )
73 4 71 72 syl2an2r 
 |-  ( ( ph /\ z e. ( I X. ( J \ ( ( y e. J |-> Y ) supp .0. ) ) ) ) -> ( ( ( x e. I |-> X ) ` ( 1st ` z ) ) .x. .0. ) = .0. )
74 68 73 eqtrd 
 |-  ( ( ph /\ z e. ( I X. ( J \ ( ( y e. J |-> Y ) supp .0. ) ) ) ) -> ( ( ( x e. I |-> X ) ` ( 1st ` z ) ) .x. ( ( y e. J |-> Y ) ` ( 2nd ` z ) ) ) = .0. )
75 63 74 jaodan 
 |-  ( ( ph /\ ( z e. ( ( I \ ( ( x e. I |-> X ) supp .0. ) ) X. J ) \/ z e. ( I X. ( J \ ( ( y e. J |-> Y ) supp .0. ) ) ) ) ) -> ( ( ( x e. I |-> X ) ` ( 1st ` z ) ) .x. ( ( y e. J |-> Y ) ` ( 2nd ` z ) ) ) = .0. )
76 48 75 sylan2b 
 |-  ( ( ph /\ z e. ( ( I X. J ) \ ( ( ( x e. I |-> X ) supp .0. ) X. ( ( y e. J |-> Y ) supp .0. ) ) ) ) -> ( ( ( x e. I |-> X ) ` ( 1st ` z ) ) .x. ( ( y e. J |-> Y ) ` ( 2nd ` z ) ) ) = .0. )
77 7 8 xpexd 
 |-  ( ph -> ( I X. J ) e. _V )
78 76 77 suppss2 
 |-  ( ph -> ( ( z e. ( I X. J ) |-> ( ( ( x e. I |-> X ) ` ( 1st ` z ) ) .x. ( ( y e. J |-> Y ) ` ( 2nd ` z ) ) ) ) supp .0. ) C_ ( ( ( x e. I |-> X ) supp .0. ) X. ( ( y e. J |-> Y ) supp .0. ) ) )
79 44 78 eqsstrd 
 |-  ( ph -> ( ( x e. I , y e. J |-> ( X .x. Y ) ) supp .0. ) C_ ( ( ( x e. I |-> X ) supp .0. ) X. ( ( y e. J |-> Y ) supp .0. ) ) )