fprod2dlem

Description: Lemma for fprod2d - induction step. (Contributed by Scott Fenton, 30-Jan-2018)

	Ref	Expression
Hypotheses	fprod2d.1	$⊢ z = ⟨j, k⟩ \to D = C$
	fprod2d.2	$⊢ φ \to A \in Fin$
	fprod2d.3	$⊢ (φ \land j \in A) \to B \in Fin$
	fprod2d.4	$⊢ (φ \land (j \in A \land k \in B)) \to C \in ℂ$
	fprod2d.5	$⊢ φ \to \neg y \in x$
	fprod2d.6	$⊢ φ \to x \cup \{y\} \subseteq A$
	fprod2d.7	$⊢ ψ \leftrightarrow \prod_{j \in x} \prod_{k \in B} C = \prod_{z \in ⋃_{j \in x} (\{j\} \times B)} D$
Assertion	fprod2dlem	$⊢ (φ \land ψ) \to \prod_{j \in x \cup \{y\}} \prod_{k \in B} C = \prod_{z \in ⋃_{j \in x \cup \{y\}} (\{j\} \times B)} D$

Proof

Step	Hyp	Ref	Expression
1		fprod2d.1	$⊢ z = ⟨j, k⟩ \to D = C$
2		fprod2d.2	$⊢ φ \to A \in Fin$
3		fprod2d.3	$⊢ (φ \land j \in A) \to B \in Fin$
4		fprod2d.4	$⊢ (φ \land (j \in A \land k \in B)) \to C \in ℂ$
5		fprod2d.5	$⊢ φ \to \neg y \in x$
6		fprod2d.6	$⊢ φ \to x \cup \{y\} \subseteq A$
7		fprod2d.7	$⊢ ψ \leftrightarrow \prod_{j \in x} \prod_{k \in B} C = \prod_{z \in ⋃_{j \in x} (\{j\} \times B)} D$
8		simpr	$⊢ (φ \land ψ) \to ψ$
9	8 7	sylib	$⊢ (φ \land ψ) \to \prod_{j \in x} \prod_{k \in B} C = \prod_{z \in ⋃_{j \in x} (\{j\} \times B)} D$
10		nfcv	$⊢ \underline{Ⅎ} m \prod_{k \in B} C$
11		nfcsb1v	$⊢ \underline{Ⅎ} j ⦋ m / j ⦌ B$
12		nfcsb1v	$⊢ \underline{Ⅎ} j ⦋ m / j ⦌ C$
13	11 12	nfcprod	$⊢ \underline{Ⅎ} j \prod_{k \in ⦋ m / j ⦌ B} ⦋ m / j ⦌ C$
14		csbeq1a	$⊢ j = m \to B = ⦋ m / j ⦌ B$
15		csbeq1a	$⊢ j = m \to C = ⦋ m / j ⦌ C$
16	15	adantr	$⊢ (j = m \land k \in B) \to C = ⦋ m / j ⦌ C$
17	14 16	prodeq12dv	$⊢ j = m \to \prod_{k \in B} C = \prod_{k \in ⦋ m / j ⦌ B} ⦋ m / j ⦌ C$
18	10 13 17	cbvprodi	$⊢ \prod_{j \in \{y\}} \prod_{k \in B} C = \prod_{m \in \{y\}} \prod_{k \in ⦋ m / j ⦌ B} ⦋ m / j ⦌ C$
19	6	unssbd	$⊢ φ \to \{y\} \subseteq A$
20		vex	$⊢ y \in V$
21	20	snss	$⊢ y \in A \leftrightarrow \{y\} \subseteq A$
22	19 21	sylibr	$⊢ φ \to y \in A$
23	3	ralrimiva	$⊢ φ \to \forall j \in A B \in Fin$
24		nfcsb1v	$⊢ \underline{Ⅎ} j ⦋ y / j ⦌ B$
25	24	nfel1	$⊢ Ⅎ j ⦋ y / j ⦌ B \in Fin$
26		csbeq1a	$⊢ j = y \to B = ⦋ y / j ⦌ B$
27	26	eleq1d	$⊢ j = y \to (B \in Fin \leftrightarrow ⦋ y / j ⦌ B \in Fin)$
28	25 27	rspc	$⊢ y \in A \to (\forall j \in A B \in Fin \to ⦋ y / j ⦌ B \in Fin)$
29	22 23 28	sylc	$⊢ φ \to ⦋ y / j ⦌ B \in Fin$
30	4	ralrimivva	$⊢ φ \to \forall j \in A \forall k \in B C \in ℂ$
31		nfcsb1v	$⊢ \underline{Ⅎ} j ⦋ y / j ⦌ C$
32	31	nfel1	$⊢ Ⅎ j ⦋ y / j ⦌ C \in ℂ$
33	24 32	nfralw	$⊢ Ⅎ j \forall k \in ⦋ y / j ⦌ B ⦋ y / j ⦌ C \in ℂ$
34		csbeq1a	$⊢ j = y \to C = ⦋ y / j ⦌ C$
35	34	eleq1d	$⊢ j = y \to (C \in ℂ \leftrightarrow ⦋ y / j ⦌ C \in ℂ)$
36	26 35	raleqbidv	$⊢ j = y \to (\forall k \in B C \in ℂ \leftrightarrow \forall k \in ⦋ y / j ⦌ B ⦋ y / j ⦌ C \in ℂ)$
37	33 36	rspc	$⊢ y \in A \to (\forall j \in A \forall k \in B C \in ℂ \to \forall k \in ⦋ y / j ⦌ B ⦋ y / j ⦌ C \in ℂ)$
38	22 30 37	sylc	$⊢ φ \to \forall k \in ⦋ y / j ⦌ B ⦋ y / j ⦌ C \in ℂ$
39	38	r19.21bi	$⊢ (φ \land k \in ⦋ y / j ⦌ B) \to ⦋ y / j ⦌ C \in ℂ$
40	29 39	fprodcl	$⊢ φ \to \prod_{k \in ⦋ y / j ⦌ B} ⦋ y / j ⦌ C \in ℂ$
41		csbeq1	$⊢ m = y \to ⦋ m / j ⦌ B = ⦋ y / j ⦌ B$
42		csbeq1	$⊢ m = y \to ⦋ m / j ⦌ C = ⦋ y / j ⦌ C$
43	42	adantr	$⊢ (m = y \land k \in ⦋ m / j ⦌ B) \to ⦋ m / j ⦌ C = ⦋ y / j ⦌ C$
44	41 43	prodeq12dv	$⊢ m = y \to \prod_{k \in ⦋ m / j ⦌ B} ⦋ m / j ⦌ C = \prod_{k \in ⦋ y / j ⦌ B} ⦋ y / j ⦌ C$
45	44	prodsn	$⊢ (y \in A \land \prod_{k \in ⦋ y / j ⦌ B} ⦋ y / j ⦌ C \in ℂ) \to \prod_{m \in \{y\}} \prod_{k \in ⦋ m / j ⦌ B} ⦋ m / j ⦌ C = \prod_{k \in ⦋ y / j ⦌ B} ⦋ y / j ⦌ C$
46	22 40 45	syl2anc	$⊢ φ \to \prod_{m \in \{y\}} \prod_{k \in ⦋ m / j ⦌ B} ⦋ m / j ⦌ C = \prod_{k \in ⦋ y / j ⦌ B} ⦋ y / j ⦌ C$
47		nfcv	$⊢ \underline{Ⅎ} m ⦋ y / j ⦌ C$
48		nfcsb1v	$⊢ \underline{Ⅎ} k ⦋ m / k ⦌ ⦋ y / j ⦌ C$
49		csbeq1a	$⊢ k = m \to ⦋ y / j ⦌ C = ⦋ m / k ⦌ ⦋ y / j ⦌ C$
50	47 48 49	cbvprodi	$⊢ \prod_{k \in ⦋ y / j ⦌ B} ⦋ y / j ⦌ C = \prod_{m \in ⦋ y / j ⦌ B} ⦋ m / k ⦌ ⦋ y / j ⦌ C$
51		csbeq1	$⊢ m = 2^{nd} (z) \to ⦋ m / k ⦌ ⦋ y / j ⦌ C = ⦋ 2^{nd} (z) / k ⦌ ⦋ y / j ⦌ C$
52		snfi	$⊢ \{y\} \in Fin$
53		xpfi	$⊢ (\{y\} \in Fin \land ⦋ y / j ⦌ B \in Fin) \to \{y\} \times ⦋ y / j ⦌ B \in Fin$
54	52 29 53	sylancr	$⊢ φ \to \{y\} \times ⦋ y / j ⦌ B \in Fin$
55		2ndconst	$⊢ y \in A \to ({2^{nd} ↾}_{(\{y\} \times ⦋ y / j ⦌ B)}) : \{y\} \times ⦋ y / j ⦌ B \underset{1-1 onto}{⟶} ⦋ y / j ⦌ B$
56	22 55	syl	$⊢ φ \to ({2^{nd} ↾}_{(\{y\} \times ⦋ y / j ⦌ B)}) : \{y\} \times ⦋ y / j ⦌ B \underset{1-1 onto}{⟶} ⦋ y / j ⦌ B$
57		fvres	$⊢ z \in (\{y\} \times ⦋ y / j ⦌ B) \to ({2^{nd} ↾}_{(\{y\} \times ⦋ y / j ⦌ B)}) (z) = 2^{nd} (z)$
58	57	adantl	$⊢ (φ \land z \in (\{y\} \times ⦋ y / j ⦌ B)) \to ({2^{nd} ↾}_{(\{y\} \times ⦋ y / j ⦌ B)}) (z) = 2^{nd} (z)$
59	48	nfel1	$⊢ Ⅎ k ⦋ m / k ⦌ ⦋ y / j ⦌ C \in ℂ$
60	49	eleq1d	$⊢ k = m \to (⦋ y / j ⦌ C \in ℂ \leftrightarrow ⦋ m / k ⦌ ⦋ y / j ⦌ C \in ℂ)$
61	59 60	rspc	$⊢ m \in ⦋ y / j ⦌ B \to (\forall k \in ⦋ y / j ⦌ B ⦋ y / j ⦌ C \in ℂ \to ⦋ m / k ⦌ ⦋ y / j ⦌ C \in ℂ)$
62	38 61	mpan9	$⊢ (φ \land m \in ⦋ y / j ⦌ B) \to ⦋ m / k ⦌ ⦋ y / j ⦌ C \in ℂ$
63	51 54 56 58 62	fprodf1o	$⊢ φ \to \prod_{m \in ⦋ y / j ⦌ B} ⦋ m / k ⦌ ⦋ y / j ⦌ C = \prod_{z \in \{y\} \times ⦋ y / j ⦌ B} ⦋ 2^{nd} (z) / k ⦌ ⦋ y / j ⦌ C$
64		elxp	$⊢ z \in (\{y\} \times ⦋ y / j ⦌ B) \leftrightarrow \exists m \exists k (z = ⟨m, k⟩ \land (m \in \{y\} \land k \in ⦋ y / j ⦌ B))$
65		nfv	$⊢ Ⅎ j z = ⟨m, k⟩$
66		nfv	$⊢ Ⅎ j m \in \{y\}$
67	24	nfcri	$⊢ Ⅎ j k \in ⦋ y / j ⦌ B$
68	66 67	nfan	$⊢ Ⅎ j (m \in \{y\} \land k \in ⦋ y / j ⦌ B)$
69	65 68	nfan	$⊢ Ⅎ j (z = ⟨m, k⟩ \land (m \in \{y\} \land k \in ⦋ y / j ⦌ B))$
70	69	nfex	$⊢ Ⅎ j \exists k (z = ⟨m, k⟩ \land (m \in \{y\} \land k \in ⦋ y / j ⦌ B))$
71		nfv	$⊢ Ⅎ m \exists k (z = ⟨j, k⟩ \land (j = y \land k \in B))$
72		opeq1	$⊢ m = j \to ⟨m, k⟩ = ⟨j, k⟩$
73	72	eqeq2d	$⊢ m = j \to (z = ⟨m, k⟩ \leftrightarrow z = ⟨j, k⟩)$
74		eleq1w	$⊢ m = j \to (m \in \{y\} \leftrightarrow j \in \{y\})$
75		velsn	$⊢ j \in \{y\} \leftrightarrow j = y$
76	74 75	bitrdi	$⊢ m = j \to (m \in \{y\} \leftrightarrow j = y)$
77	76	anbi1d	$⊢ m = j \to ((m \in \{y\} \land k \in ⦋ y / j ⦌ B) \leftrightarrow (j = y \land k \in ⦋ y / j ⦌ B))$
78	26	eleq2d	$⊢ j = y \to (k \in B \leftrightarrow k \in ⦋ y / j ⦌ B)$
79	78	pm5.32i	$⊢ (j = y \land k \in B) \leftrightarrow (j = y \land k \in ⦋ y / j ⦌ B)$
80	77 79	bitr4di	$⊢ m = j \to ((m \in \{y\} \land k \in ⦋ y / j ⦌ B) \leftrightarrow (j = y \land k \in B))$
81	73 80	anbi12d	$⊢ m = j \to ((z = ⟨m, k⟩ \land (m \in \{y\} \land k \in ⦋ y / j ⦌ B)) \leftrightarrow (z = ⟨j, k⟩ \land (j = y \land k \in B)))$
82	81	exbidv	$⊢ m = j \to (\exists k (z = ⟨m, k⟩ \land (m \in \{y\} \land k \in ⦋ y / j ⦌ B)) \leftrightarrow \exists k (z = ⟨j, k⟩ \land (j = y \land k \in B)))$
83	70 71 82	cbvexv1	$⊢ \exists m \exists k (z = ⟨m, k⟩ \land (m \in \{y\} \land k \in ⦋ y / j ⦌ B)) \leftrightarrow \exists j \exists k (z = ⟨j, k⟩ \land (j = y \land k \in B))$
84	64 83	bitri	$⊢ z \in (\{y\} \times ⦋ y / j ⦌ B) \leftrightarrow \exists j \exists k (z = ⟨j, k⟩ \land (j = y \land k \in B))$
85		nfv	$⊢ Ⅎ j φ$
86		nfcv	$⊢ \underline{Ⅎ} j 2^{nd} (z)$
87	86 31	nfcsbw	$⊢ \underline{Ⅎ} j ⦋ 2^{nd} (z) / k ⦌ ⦋ y / j ⦌ C$
88	87	nfeq2	$⊢ Ⅎ j D = ⦋ 2^{nd} (z) / k ⦌ ⦋ y / j ⦌ C$
89		nfv	$⊢ Ⅎ k φ$
90		nfcsb1v	$⊢ \underline{Ⅎ} k ⦋ 2^{nd} (z) / k ⦌ ⦋ y / j ⦌ C$
91	90	nfeq2	$⊢ Ⅎ k D = ⦋ 2^{nd} (z) / k ⦌ ⦋ y / j ⦌ C$
92	1	ad2antlr	$⊢ ((φ \land z = ⟨j, k⟩) \land (j = y \land k \in B)) \to D = C$
93	34	ad2antrl	$⊢ ((φ \land z = ⟨j, k⟩) \land (j = y \land k \in B)) \to C = ⦋ y / j ⦌ C$
94		fveq2	$⊢ z = ⟨j, k⟩ \to 2^{nd} (z) = 2^{nd} (⟨j, k⟩)$
95		vex	$⊢ j \in V$
96		vex	$⊢ k \in V$
97	95 96	op2nd	$⊢ 2^{nd} (⟨j, k⟩) = k$
98	94 97	eqtr2di	$⊢ z = ⟨j, k⟩ \to k = 2^{nd} (z)$
99	98	ad2antlr	$⊢ ((φ \land z = ⟨j, k⟩) \land (j = y \land k \in B)) \to k = 2^{nd} (z)$
100		csbeq1a	$⊢ k = 2^{nd} (z) \to ⦋ y / j ⦌ C = ⦋ 2^{nd} (z) / k ⦌ ⦋ y / j ⦌ C$
101	99 100	syl	$⊢ ((φ \land z = ⟨j, k⟩) \land (j = y \land k \in B)) \to ⦋ y / j ⦌ C = ⦋ 2^{nd} (z) / k ⦌ ⦋ y / j ⦌ C$
102	92 93 101	3eqtrd	$⊢ ((φ \land z = ⟨j, k⟩) \land (j = y \land k \in B)) \to D = ⦋ 2^{nd} (z) / k ⦌ ⦋ y / j ⦌ C$
103	102	expl	$⊢ φ \to ((z = ⟨j, k⟩ \land (j = y \land k \in B)) \to D = ⦋ 2^{nd} (z) / k ⦌ ⦋ y / j ⦌ C)$
104	89 91 103	exlimd	$⊢ φ \to (\exists k (z = ⟨j, k⟩ \land (j = y \land k \in B)) \to D = ⦋ 2^{nd} (z) / k ⦌ ⦋ y / j ⦌ C)$
105	85 88 104	exlimd	$⊢ φ \to (\exists j \exists k (z = ⟨j, k⟩ \land (j = y \land k \in B)) \to D = ⦋ 2^{nd} (z) / k ⦌ ⦋ y / j ⦌ C)$
106	84 105	biimtrid	$⊢ φ \to (z \in (\{y\} \times ⦋ y / j ⦌ B) \to D = ⦋ 2^{nd} (z) / k ⦌ ⦋ y / j ⦌ C)$
107	106	imp	$⊢ (φ \land z \in (\{y\} \times ⦋ y / j ⦌ B)) \to D = ⦋ 2^{nd} (z) / k ⦌ ⦋ y / j ⦌ C$
108	107	prodeq2dv	$⊢ φ \to \prod_{z \in \{y\} \times ⦋ y / j ⦌ B} D = \prod_{z \in \{y\} \times ⦋ y / j ⦌ B} ⦋ 2^{nd} (z) / k ⦌ ⦋ y / j ⦌ C$
109	63 108	eqtr4d	$⊢ φ \to \prod_{m \in ⦋ y / j ⦌ B} ⦋ m / k ⦌ ⦋ y / j ⦌ C = \prod_{z \in \{y\} \times ⦋ y / j ⦌ B} D$
110	50 109	eqtrid	$⊢ φ \to \prod_{k \in ⦋ y / j ⦌ B} ⦋ y / j ⦌ C = \prod_{z \in \{y\} \times ⦋ y / j ⦌ B} D$
111	46 110	eqtrd	$⊢ φ \to \prod_{m \in \{y\}} \prod_{k \in ⦋ m / j ⦌ B} ⦋ m / j ⦌ C = \prod_{z \in \{y\} \times ⦋ y / j ⦌ B} D$
112	18 111	eqtrid	$⊢ φ \to \prod_{j \in \{y\}} \prod_{k \in B} C = \prod_{z \in \{y\} \times ⦋ y / j ⦌ B} D$
113	112	adantr	$⊢ (φ \land ψ) \to \prod_{j \in \{y\}} \prod_{k \in B} C = \prod_{z \in \{y\} \times ⦋ y / j ⦌ B} D$
114	9 113	oveq12d	$⊢ (φ \land ψ) \to \prod_{j \in x} \prod_{k \in B} C \prod_{j \in \{y\}} \prod_{k \in B} C = \prod_{z \in ⋃_{j \in x} (\{j\} \times B)} D \prod_{z \in \{y\} \times ⦋ y / j ⦌ B} D$
115		disjsn	$⊢ x \cap \{y\} = \emptyset \leftrightarrow \neg y \in x$
116	5 115	sylibr	$⊢ φ \to x \cap \{y\} = \emptyset$
117		eqidd	$⊢ φ \to x \cup \{y\} = x \cup \{y\}$
118	2 6	ssfid	$⊢ φ \to x \cup \{y\} \in Fin$
119	6	sselda	$⊢ (φ \land j \in (x \cup \{y\})) \to j \in A$
120	4	anassrs	$⊢ ((φ \land j \in A) \land k \in B) \to C \in ℂ$
121	3 120	fprodcl	$⊢ (φ \land j \in A) \to \prod_{k \in B} C \in ℂ$
122	119 121	syldan	$⊢ (φ \land j \in (x \cup \{y\})) \to \prod_{k \in B} C \in ℂ$
123	116 117 118 122	fprodsplit	$⊢ φ \to \prod_{j \in x \cup \{y\}} \prod_{k \in B} C = \prod_{j \in x} \prod_{k \in B} C \prod_{j \in \{y\}} \prod_{k \in B} C$
124	123	adantr	$⊢ (φ \land ψ) \to \prod_{j \in x \cup \{y\}} \prod_{k \in B} C = \prod_{j \in x} \prod_{k \in B} C \prod_{j \in \{y\}} \prod_{k \in B} C$
125		eliun	$⊢ z \in ⋃_{j \in x} (\{j\} \times B) \leftrightarrow \exists j \in x z \in (\{j\} \times B)$
126		xp1st	$⊢ z \in (\{j\} \times B) \to 1^{st} (z) \in \{j\}$
127		elsni	$⊢ 1^{st} (z) \in \{j\} \to 1^{st} (z) = j$
128	126 127	syl	$⊢ z \in (\{j\} \times B) \to 1^{st} (z) = j$
129	128	eleq1d	$⊢ z \in (\{j\} \times B) \to (1^{st} (z) \in x \leftrightarrow j \in x)$
130	129	biimparc	$⊢ (j \in x \land z \in (\{j\} \times B)) \to 1^{st} (z) \in x$
131	130	rexlimiva	$⊢ \exists j \in x z \in (\{j\} \times B) \to 1^{st} (z) \in x$
132	125 131	sylbi	$⊢ z \in ⋃_{j \in x} (\{j\} \times B) \to 1^{st} (z) \in x$
133		xp1st	$⊢ z \in (\{y\} \times ⦋ y / j ⦌ B) \to 1^{st} (z) \in \{y\}$
134	132 133	anim12i	$⊢ (z \in ⋃_{j \in x} (\{j\} \times B) \land z \in (\{y\} \times ⦋ y / j ⦌ B)) \to (1^{st} (z) \in x \land 1^{st} (z) \in \{y\})$
135		elin	$⊢ z \in (⋃_{j \in x} (\{j\} \times B) \cap (\{y\} \times ⦋ y / j ⦌ B)) \leftrightarrow (z \in ⋃_{j \in x} (\{j\} \times B) \land z \in (\{y\} \times ⦋ y / j ⦌ B))$
136		elin	$⊢ 1^{st} (z) \in (x \cap \{y\}) \leftrightarrow (1^{st} (z) \in x \land 1^{st} (z) \in \{y\})$
137	134 135 136	3imtr4i	$⊢ z \in (⋃_{j \in x} (\{j\} \times B) \cap (\{y\} \times ⦋ y / j ⦌ B)) \to 1^{st} (z) \in (x \cap \{y\})$
138	116	eleq2d	$⊢ φ \to (1^{st} (z) \in (x \cap \{y\}) \leftrightarrow 1^{st} (z) \in \emptyset)$
139		noel	$⊢ \neg 1^{st} (z) \in \emptyset$
140	139	pm2.21i	$⊢ 1^{st} (z) \in \emptyset \to z \in \emptyset$
141	138 140	syl6bi	$⊢ φ \to (1^{st} (z) \in (x \cap \{y\}) \to z \in \emptyset)$
142	137 141	syl5	$⊢ φ \to (z \in (⋃_{j \in x} (\{j\} \times B) \cap (\{y\} \times ⦋ y / j ⦌ B)) \to z \in \emptyset)$
143	142	ssrdv	$⊢ φ \to ⋃_{j \in x} (\{j\} \times B) \cap (\{y\} \times ⦋ y / j ⦌ B) \subseteq \emptyset$
144		ss0	$⊢ ⋃_{j \in x} (\{j\} \times B) \cap (\{y\} \times ⦋ y / j ⦌ B) \subseteq \emptyset \to ⋃_{j \in x} (\{j\} \times B) \cap (\{y\} \times ⦋ y / j ⦌ B) = \emptyset$
145	143 144	syl	$⊢ φ \to ⋃_{j \in x} (\{j\} \times B) \cap (\{y\} \times ⦋ y / j ⦌ B) = \emptyset$
146		iunxun	$⊢ ⋃_{j \in x \cup \{y\}} (\{j\} \times B) = ⋃_{j \in x} (\{j\} \times B) \cup ⋃_{j \in \{y\}} (\{j\} \times B)$
147		nfcv	$⊢ \underline{Ⅎ} m (\{j\} \times B)$
148		nfcv	$⊢ \underline{Ⅎ} j \{m\}$
149	148 11	nfxp	$⊢ \underline{Ⅎ} j (\{m\} \times ⦋ m / j ⦌ B)$
150		sneq	$⊢ j = m \to \{j\} = \{m\}$
151	150 14	xpeq12d	$⊢ j = m \to \{j\} \times B = \{m\} \times ⦋ m / j ⦌ B$
152	147 149 151	cbviun	$⊢ ⋃_{j \in \{y\}} (\{j\} \times B) = ⋃_{m \in \{y\}} (\{m\} \times ⦋ m / j ⦌ B)$
153		sneq	$⊢ m = y \to \{m\} = \{y\}$
154	153 41	xpeq12d	$⊢ m = y \to \{m\} \times ⦋ m / j ⦌ B = \{y\} \times ⦋ y / j ⦌ B$
155	20 154	iunxsn	$⊢ ⋃_{m \in \{y\}} (\{m\} \times ⦋ m / j ⦌ B) = \{y\} \times ⦋ y / j ⦌ B$
156	152 155	eqtri	$⊢ ⋃_{j \in \{y\}} (\{j\} \times B) = \{y\} \times ⦋ y / j ⦌ B$
157	156	uneq2i	$⊢ ⋃_{j \in x} (\{j\} \times B) \cup ⋃_{j \in \{y\}} (\{j\} \times B) = ⋃_{j \in x} (\{j\} \times B) \cup (\{y\} \times ⦋ y / j ⦌ B)$
158	146 157	eqtri	$⊢ ⋃_{j \in x \cup \{y\}} (\{j\} \times B) = ⋃_{j \in x} (\{j\} \times B) \cup (\{y\} \times ⦋ y / j ⦌ B)$
159	158	a1i	$⊢ φ \to ⋃_{j \in x \cup \{y\}} (\{j\} \times B) = ⋃_{j \in x} (\{j\} \times B) \cup (\{y\} \times ⦋ y / j ⦌ B)$
160		snfi	$⊢ \{j\} \in Fin$
161	119 3	syldan	$⊢ (φ \land j \in (x \cup \{y\})) \to B \in Fin$
162		xpfi	$⊢ (\{j\} \in Fin \land B \in Fin) \to \{j\} \times B \in Fin$
163	160 161 162	sylancr	$⊢ (φ \land j \in (x \cup \{y\})) \to \{j\} \times B \in Fin$
164	163	ralrimiva	$⊢ φ \to \forall j \in (x \cup \{y\}) \{j\} \times B \in Fin$
165		iunfi	$⊢ (x \cup \{y\} \in Fin \land \forall j \in (x \cup \{y\}) \{j\} \times B \in Fin) \to ⋃_{j \in x \cup \{y\}} (\{j\} \times B) \in Fin$
166	118 164 165	syl2anc	$⊢ φ \to ⋃_{j \in x \cup \{y\}} (\{j\} \times B) \in Fin$
167		eliun	$⊢ z \in ⋃_{j \in x \cup \{y\}} (\{j\} \times B) \leftrightarrow \exists j \in (x \cup \{y\}) z \in (\{j\} \times B)$
168		elxp	$⊢ z \in (\{j\} \times B) \leftrightarrow \exists m \exists k (z = ⟨m, k⟩ \land (m \in \{j\} \land k \in B))$
169		simprl	$⊢ ((φ \land j \in (x \cup \{y\})) \land (z = ⟨m, k⟩ \land (m \in \{j\} \land k \in B))) \to z = ⟨m, k⟩$
170		simprrl	$⊢ ((φ \land j \in (x \cup \{y\})) \land (z = ⟨m, k⟩ \land (m \in \{j\} \land k \in B))) \to m \in \{j\}$
171		elsni	$⊢ m \in \{j\} \to m = j$
172	170 171	syl	$⊢ ((φ \land j \in (x \cup \{y\})) \land (z = ⟨m, k⟩ \land (m \in \{j\} \land k \in B))) \to m = j$
173	172	opeq1d	$⊢ ((φ \land j \in (x \cup \{y\})) \land (z = ⟨m, k⟩ \land (m \in \{j\} \land k \in B))) \to ⟨m, k⟩ = ⟨j, k⟩$
174	169 173	eqtrd	$⊢ ((φ \land j \in (x \cup \{y\})) \land (z = ⟨m, k⟩ \land (m \in \{j\} \land k \in B))) \to z = ⟨j, k⟩$
175	174 1	syl	$⊢ ((φ \land j \in (x \cup \{y\})) \land (z = ⟨m, k⟩ \land (m \in \{j\} \land k \in B))) \to D = C$
176		simpll	$⊢ ((φ \land j \in (x \cup \{y\})) \land (z = ⟨m, k⟩ \land (m \in \{j\} \land k \in B))) \to φ$
177	119	adantr	$⊢ ((φ \land j \in (x \cup \{y\})) \land (z = ⟨m, k⟩ \land (m \in \{j\} \land k \in B))) \to j \in A$
178		simprrr	$⊢ ((φ \land j \in (x \cup \{y\})) \land (z = ⟨m, k⟩ \land (m \in \{j\} \land k \in B))) \to k \in B$
179	176 177 178 4	syl12anc	$⊢ ((φ \land j \in (x \cup \{y\})) \land (z = ⟨m, k⟩ \land (m \in \{j\} \land k \in B))) \to C \in ℂ$
180	175 179	eqeltrd	$⊢ ((φ \land j \in (x \cup \{y\})) \land (z = ⟨m, k⟩ \land (m \in \{j\} \land k \in B))) \to D \in ℂ$
181	180	ex	$⊢ (φ \land j \in (x \cup \{y\})) \to ((z = ⟨m, k⟩ \land (m \in \{j\} \land k \in B)) \to D \in ℂ)$
182	181	exlimdvv	$⊢ (φ \land j \in (x \cup \{y\})) \to (\exists m \exists k (z = ⟨m, k⟩ \land (m \in \{j\} \land k \in B)) \to D \in ℂ)$
183	168 182	biimtrid	$⊢ (φ \land j \in (x \cup \{y\})) \to (z \in (\{j\} \times B) \to D \in ℂ)$
184	183	rexlimdva	$⊢ φ \to (\exists j \in (x \cup \{y\}) z \in (\{j\} \times B) \to D \in ℂ)$
185	167 184	biimtrid	$⊢ φ \to (z \in ⋃_{j \in x \cup \{y\}} (\{j\} \times B) \to D \in ℂ)$
186	185	imp	$⊢ (φ \land z \in ⋃_{j \in x \cup \{y\}} (\{j\} \times B)) \to D \in ℂ$
187	145 159 166 186	fprodsplit	$⊢ φ \to \prod_{z \in ⋃_{j \in x \cup \{y\}} (\{j\} \times B)} D = \prod_{z \in ⋃_{j \in x} (\{j\} \times B)} D \prod_{z \in \{y\} \times ⦋ y / j ⦌ B} D$
188	187	adantr	$⊢ (φ \land ψ) \to \prod_{z \in ⋃_{j \in x \cup \{y\}} (\{j\} \times B)} D = \prod_{z \in ⋃_{j \in x} (\{j\} \times B)} D \prod_{z \in \{y\} \times ⦋ y / j ⦌ B} D$
189	114 124 188	3eqtr4d	$⊢ (φ \land ψ) \to \prod_{j \in x \cup \{y\}} \prod_{k \in B} C = \prod_{z \in ⋃_{j \in x \cup \{y\}} (\{j\} \times B)} D$

Metamath Proof Explorer

Theorem fprod2dlem

Proof