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	$⊢ \underset{˙}{0} = 0_{R}$
	evlslem4.t	$⊢ \underset{˙}{\cdot} = \cdot_{R}$
	evlslem4.r	$⊢ φ \to R \in Ring$
	evlslem4.x	$⊢ (φ \land x \in I) \to X \in B$
	evlslem4.y	$⊢ (φ \land y \in J) \to Y \in B$
	evlslem4.i	$⊢ φ \to I \in V$
	evlslem4.j	$⊢ φ \to J \in W$
Assertion	evlslem4	$⊢ φ \to (x \in I, y \in J ⟼ X \underset{˙}{\cdot} Y) supp \underset{˙}{0} \subseteq {supp}_{\underset{˙}{0}} ((x \in I ⟼ X)) \times {supp}_{\underset{˙}{0}} ((y \in J ⟼ Y))$

Proof

Step	Hyp	Ref	Expression
1		evlslem4.b	$⊢ B = {Base}_{R}$
2		evlslem4.z	$⊢ \underset{˙}{0} = 0_{R}$
3		evlslem4.t	$⊢ \underset{˙}{\cdot} = \cdot_{R}$
4		evlslem4.r	$⊢ φ \to R \in Ring$
5		evlslem4.x	$⊢ (φ \land x \in I) \to X \in B$
6		evlslem4.y	$⊢ (φ \land y \in J) \to Y \in B$
7		evlslem4.i	$⊢ φ \to I \in V$
8		evlslem4.j	$⊢ φ \to J \in W$
9		simp2	$⊢ (φ \land x \in I \land y \in J) \to x \in I$
10	5	3adant3	$⊢ (φ \land x \in I \land y \in J) \to X \in B$
11		eqid	$⊢ (x \in I ⟼ X) = (x \in I ⟼ X)$
12	11	fvmpt2	$⊢ (x \in I \land X \in B) \to (x \in I ⟼ X) (x) = X$
13	9 10 12	syl2anc	$⊢ (φ \land x \in I \land y \in J) \to (x \in I ⟼ X) (x) = X$
14		simp3	$⊢ (φ \land x \in I \land y \in J) \to y \in J$
15		eqid	$⊢ (y \in J ⟼ Y) = (y \in J ⟼ Y)$
16	15	fvmpt2	$⊢ (y \in J \land Y \in B) \to (y \in J ⟼ Y) (y) = Y$
17	14 6 16	3imp3i2an	$⊢ (φ \land x \in I \land y \in J) \to (y \in J ⟼ Y) (y) = Y$
18	13 17	oveq12d	$⊢ (φ \land x \in I \land y \in J) \to (x \in I ⟼ X) (x) \underset{˙}{\cdot} (y \in J ⟼ Y) (y) = X \underset{˙}{\cdot} Y$
19	18	mpoeq3dva	$⊢ φ \to (x \in I, y \in J ⟼ (x \in I ⟼ X) (x) \underset{˙}{\cdot} (y \in J ⟼ Y) (y)) = (x \in I, y \in J ⟼ X \underset{˙}{\cdot} Y)$
20		nfcv	$⊢ \underline{Ⅎ} i ((x \in I ⟼ X) (x) \underset{˙}{\cdot} (y \in J ⟼ Y) (y))$
21		nfcv	$⊢ \underline{Ⅎ} j ((x \in I ⟼ X) (x) \underset{˙}{\cdot} (y \in J ⟼ Y) (y))$
22		nffvmpt1	$⊢ \underline{Ⅎ} x (x \in I ⟼ X) (i)$
23		nfcv	$⊢ \underline{Ⅎ} x \underset{˙}{\cdot}$
24		nfcv	$⊢ \underline{Ⅎ} x (y \in J ⟼ Y) (j)$
25	22 23 24	nfov	$⊢ \underline{Ⅎ} x ((x \in I ⟼ X) (i) \underset{˙}{\cdot} (y \in J ⟼ Y) (j))$
26		nfcv	$⊢ \underline{Ⅎ} y (x \in I ⟼ X) (i)$
27		nfcv	$⊢ \underline{Ⅎ} y \underset{˙}{\cdot}$
28		nffvmpt1	$⊢ \underline{Ⅎ} y (y \in J ⟼ Y) (j)$
29	26 27 28	nfov	$⊢ \underline{Ⅎ} y ((x \in I ⟼ X) (i) \underset{˙}{\cdot} (y \in J ⟼ Y) (j))$
30		fveq2	$⊢ x = i \to (x \in I ⟼ X) (x) = (x \in I ⟼ X) (i)$
31		fveq2	$⊢ y = j \to (y \in J ⟼ Y) (y) = (y \in J ⟼ Y) (j)$
32	30 31	oveqan12d	$⊢ (x = i \land y = j) \to (x \in I ⟼ X) (x) \underset{˙}{\cdot} (y \in J ⟼ Y) (y) = (x \in I ⟼ X) (i) \underset{˙}{\cdot} (y \in J ⟼ Y) (j)$
33	20 21 25 29 32	cbvmpo	$⊢ (x \in I, y \in J ⟼ (x \in I ⟼ X) (x) \underset{˙}{\cdot} (y \in J ⟼ Y) (y)) = (i \in I, j \in J ⟼ (x \in I ⟼ X) (i) \underset{˙}{\cdot} (y \in J ⟼ Y) (j))$
34		vex	$⊢ i \in V$
35		vex	$⊢ j \in V$
36	34 35	eqop2	$⊢ z = ⟨i, j⟩ \leftrightarrow (z \in (V \times V) \land (1^{st} (z) = i \land 2^{nd} (z) = j))$
37		fveq2	$⊢ 1^{st} (z) = i \to (x \in I ⟼ X) (1^{st} (z)) = (x \in I ⟼ X) (i)$
38		fveq2	$⊢ 2^{nd} (z) = j \to (y \in J ⟼ Y) (2^{nd} (z)) = (y \in J ⟼ Y) (j)$
39	37 38	oveqan12d	$⊢ (1^{st} (z) = i \land 2^{nd} (z) = j) \to (x \in I ⟼ X) (1^{st} (z)) \underset{˙}{\cdot} (y \in J ⟼ Y) (2^{nd} (z)) = (x \in I ⟼ X) (i) \underset{˙}{\cdot} (y \in J ⟼ Y) (j)$
40	36 39	simplbiim	$⊢ z = ⟨i, j⟩ \to (x \in I ⟼ X) (1^{st} (z)) \underset{˙}{\cdot} (y \in J ⟼ Y) (2^{nd} (z)) = (x \in I ⟼ X) (i) \underset{˙}{\cdot} (y \in J ⟼ Y) (j)$
41	40	mpompt	$⊢ (z \in (I \times J) ⟼ (x \in I ⟼ X) (1^{st} (z)) \underset{˙}{\cdot} (y \in J ⟼ Y) (2^{nd} (z))) = (i \in I, j \in J ⟼ (x \in I ⟼ X) (i) \underset{˙}{\cdot} (y \in J ⟼ Y) (j))$
42	33 41	eqtr4i	$⊢ (x \in I, y \in J ⟼ (x \in I ⟼ X) (x) \underset{˙}{\cdot} (y \in J ⟼ Y) (y)) = (z \in (I \times J) ⟼ (x \in I ⟼ X) (1^{st} (z)) \underset{˙}{\cdot} (y \in J ⟼ Y) (2^{nd} (z)))$
43	19 42	eqtr3di	$⊢ φ \to (x \in I, y \in J ⟼ X \underset{˙}{\cdot} Y) = (z \in (I \times J) ⟼ (x \in I ⟼ X) (1^{st} (z)) \underset{˙}{\cdot} (y \in J ⟼ Y) (2^{nd} (z)))$
44	43	oveq1d	$⊢ φ \to (x \in I, y \in J ⟼ X \underset{˙}{\cdot} Y) supp \underset{˙}{0} = (z \in (I \times J) ⟼ (x \in I ⟼ X) (1^{st} (z)) \underset{˙}{\cdot} (y \in J ⟼ Y) (2^{nd} (z))) supp \underset{˙}{0}$
45		difxp	$⊢ (I \times J) ∖ ({supp}_{\underset{˙}{0}} ((x \in I ⟼ X)) \times {supp}_{\underset{˙}{0}} ((y \in J ⟼ Y))) = ((I ∖ {supp}_{\underset{˙}{0}} ((x \in I ⟼ X))) \times J) \cup (I \times (J ∖ {supp}_{\underset{˙}{0}} ((y \in J ⟼ Y))))$
46	45	eleq2i	$⊢ z \in ((I \times J) ∖ ({supp}_{\underset{˙}{0}} ((x \in I ⟼ X)) \times {supp}_{\underset{˙}{0}} ((y \in J ⟼ Y)))) \leftrightarrow z \in (((I ∖ {supp}_{\underset{˙}{0}} ((x \in I ⟼ X))) \times J) \cup (I \times (J ∖ {supp}_{\underset{˙}{0}} ((y \in J ⟼ Y)))))$
47		elun	$⊢ z \in (((I ∖ {supp}_{\underset{˙}{0}} ((x \in I ⟼ X))) \times J) \cup (I \times (J ∖ {supp}_{\underset{˙}{0}} ((y \in J ⟼ Y))))) \leftrightarrow (z \in ((I ∖ {supp}_{\underset{˙}{0}} ((x \in I ⟼ X))) \times J) \lor z \in (I \times (J ∖ {supp}_{\underset{˙}{0}} ((y \in J ⟼ Y)))))$
48	46 47	bitri	$⊢ z \in ((I \times J) ∖ ({supp}_{\underset{˙}{0}} ((x \in I ⟼ X)) \times {supp}_{\underset{˙}{0}} ((y \in J ⟼ Y)))) \leftrightarrow (z \in ((I ∖ {supp}_{\underset{˙}{0}} ((x \in I ⟼ X))) \times J) \lor z \in (I \times (J ∖ {supp}_{\underset{˙}{0}} ((y \in J ⟼ Y)))))$
49		xp1st	$⊢ z \in ((I ∖ {supp}_{\underset{˙}{0}} ((x \in I ⟼ X))) \times J) \to 1^{st} (z) \in (I ∖ {supp}_{\underset{˙}{0}} ((x \in I ⟼ X)))$
50	5	fmpttd	$⊢ φ \to (x \in I ⟼ X) : I ⟶ B$
51		ssidd	$⊢ φ \to (x \in I ⟼ X) supp \underset{˙}{0} \subseteq (x \in I ⟼ X) supp \underset{˙}{0}$
52	2	fvexi	$⊢ \underset{˙}{0} \in V$
53	52	a1i	$⊢ φ \to \underset{˙}{0} \in V$
54	50 51 7 53	suppssr	$⊢ (φ \land 1^{st} (z) \in (I ∖ {supp}_{\underset{˙}{0}} ((x \in I ⟼ X)))) \to (x \in I ⟼ X) (1^{st} (z)) = \underset{˙}{0}$
55	49 54	sylan2	$⊢ (φ \land z \in ((I ∖ {supp}_{\underset{˙}{0}} ((x \in I ⟼ X))) \times J)) \to (x \in I ⟼ X) (1^{st} (z)) = \underset{˙}{0}$
56	55	oveq1d	$⊢ (φ \land z \in ((I ∖ {supp}_{\underset{˙}{0}} ((x \in I ⟼ X))) \times J)) \to (x \in I ⟼ X) (1^{st} (z)) \underset{˙}{\cdot} (y \in J ⟼ Y) (2^{nd} (z)) = \underset{˙}{0} \underset{˙}{\cdot} (y \in J ⟼ Y) (2^{nd} (z))$
57	6	fmpttd	$⊢ φ \to (y \in J ⟼ Y) : J ⟶ B$
58		xp2nd	$⊢ z \in ((I ∖ {supp}_{\underset{˙}{0}} ((x \in I ⟼ X))) \times J) \to 2^{nd} (z) \in J$
59		ffvelcdm	$⊢ ((y \in J ⟼ Y) : J ⟶ B \land 2^{nd} (z) \in J) \to (y \in J ⟼ Y) (2^{nd} (z)) \in B$
60	57 58 59	syl2an	$⊢ (φ \land z \in ((I ∖ {supp}_{\underset{˙}{0}} ((x \in I ⟼ X))) \times J)) \to (y \in J ⟼ Y) (2^{nd} (z)) \in B$
61	1 3 2	ringlz	$⊢ (R \in Ring \land (y \in J ⟼ Y) (2^{nd} (z)) \in B) \to \underset{˙}{0} \underset{˙}{\cdot} (y \in J ⟼ Y) (2^{nd} (z)) = \underset{˙}{0}$
62	4 60 61	syl2an2r	$⊢ (φ \land z \in ((I ∖ {supp}_{\underset{˙}{0}} ((x \in I ⟼ X))) \times J)) \to \underset{˙}{0} \underset{˙}{\cdot} (y \in J ⟼ Y) (2^{nd} (z)) = \underset{˙}{0}$
63	56 62	eqtrd	$⊢ (φ \land z \in ((I ∖ {supp}_{\underset{˙}{0}} ((x \in I ⟼ X))) \times J)) \to (x \in I ⟼ X) (1^{st} (z)) \underset{˙}{\cdot} (y \in J ⟼ Y) (2^{nd} (z)) = \underset{˙}{0}$
64		xp2nd	$⊢ z \in (I \times (J ∖ {supp}_{\underset{˙}{0}} ((y \in J ⟼ Y)))) \to 2^{nd} (z) \in (J ∖ {supp}_{\underset{˙}{0}} ((y \in J ⟼ Y)))$
65		ssidd	$⊢ φ \to (y \in J ⟼ Y) supp \underset{˙}{0} \subseteq (y \in J ⟼ Y) supp \underset{˙}{0}$
66	57 65 8 53	suppssr	$⊢ (φ \land 2^{nd} (z) \in (J ∖ {supp}_{\underset{˙}{0}} ((y \in J ⟼ Y)))) \to (y \in J ⟼ Y) (2^{nd} (z)) = \underset{˙}{0}$
67	64 66	sylan2	$⊢ (φ \land z \in (I \times (J ∖ {supp}_{\underset{˙}{0}} ((y \in J ⟼ Y))))) \to (y \in J ⟼ Y) (2^{nd} (z)) = \underset{˙}{0}$
68	67	oveq2d	$⊢ (φ \land z \in (I \times (J ∖ {supp}_{\underset{˙}{0}} ((y \in J ⟼ Y))))) \to (x \in I ⟼ X) (1^{st} (z)) \underset{˙}{\cdot} (y \in J ⟼ Y) (2^{nd} (z)) = (x \in I ⟼ X) (1^{st} (z)) \underset{˙}{\cdot} \underset{˙}{0}$
69		xp1st	$⊢ z \in (I \times (J ∖ {supp}_{\underset{˙}{0}} ((y \in J ⟼ Y)))) \to 1^{st} (z) \in I$
70		ffvelcdm	$⊢ ((x \in I ⟼ X) : I ⟶ B \land 1^{st} (z) \in I) \to (x \in I ⟼ X) (1^{st} (z)) \in B$
71	50 69 70	syl2an	$⊢ (φ \land z \in (I \times (J ∖ {supp}_{\underset{˙}{0}} ((y \in J ⟼ Y))))) \to (x \in I ⟼ X) (1^{st} (z)) \in B$
72	1 3 2	ringrz	$⊢ (R \in Ring \land (x \in I ⟼ X) (1^{st} (z)) \in B) \to (x \in I ⟼ X) (1^{st} (z)) \underset{˙}{\cdot} \underset{˙}{0} = \underset{˙}{0}$
73	4 71 72	syl2an2r	$⊢ (φ \land z \in (I \times (J ∖ {supp}_{\underset{˙}{0}} ((y \in J ⟼ Y))))) \to (x \in I ⟼ X) (1^{st} (z)) \underset{˙}{\cdot} \underset{˙}{0} = \underset{˙}{0}$
74	68 73	eqtrd	$⊢ (φ \land z \in (I \times (J ∖ {supp}_{\underset{˙}{0}} ((y \in J ⟼ Y))))) \to (x \in I ⟼ X) (1^{st} (z)) \underset{˙}{\cdot} (y \in J ⟼ Y) (2^{nd} (z)) = \underset{˙}{0}$
75	63 74	jaodan	$⊢ (φ \land (z \in ((I ∖ {supp}_{\underset{˙}{0}} ((x \in I ⟼ X))) \times J) \lor z \in (I \times (J ∖ {supp}_{\underset{˙}{0}} ((y \in J ⟼ Y)))))) \to (x \in I ⟼ X) (1^{st} (z)) \underset{˙}{\cdot} (y \in J ⟼ Y) (2^{nd} (z)) = \underset{˙}{0}$
76	48 75	sylan2b	$⊢ (φ \land z \in ((I \times J) ∖ ({supp}_{\underset{˙}{0}} ((x \in I ⟼ X)) \times {supp}_{\underset{˙}{0}} ((y \in J ⟼ Y))))) \to (x \in I ⟼ X) (1^{st} (z)) \underset{˙}{\cdot} (y \in J ⟼ Y) (2^{nd} (z)) = \underset{˙}{0}$
77	7 8	xpexd	$⊢ φ \to I \times J \in V$
78	76 77	suppss2	$⊢ φ \to (z \in (I \times J) ⟼ (x \in I ⟼ X) (1^{st} (z)) \underset{˙}{\cdot} (y \in J ⟼ Y) (2^{nd} (z))) supp \underset{˙}{0} \subseteq {supp}_{\underset{˙}{0}} ((x \in I ⟼ X)) \times {supp}_{\underset{˙}{0}} ((y \in J ⟼ Y))$
79	44 78	eqsstrd	$⊢ φ \to (x \in I, y \in J ⟼ X \underset{˙}{\cdot} Y) supp \underset{˙}{0} \subseteq {supp}_{\underset{˙}{0}} ((x \in I ⟼ X)) \times {supp}_{\underset{˙}{0}} ((y \in J ⟼ Y))$

Metamath Proof Explorer

Theorem evlslem4

Proof