smueqlem

Description: Any element of a sequence multiplication only depends on the values of the argument sequences up to and including that point. (Contributed by Mario Carneiro, 20-Sep-2016)

	Ref	Expression
Hypotheses	smueq.a	$⊢ φ \to A \subseteq ℕ_{0}$
	smueq.b	$⊢ φ \to B \subseteq ℕ_{0}$
	smueq.n	$⊢ φ \to N \in ℕ_{0}$
	smueq.p	$⊢ P = seq 0 ((p \in 𝒫 ℕ_{0}, m \in ℕ_{0} ⟼ p sadd \{n \in ℕ_{0} \| (m \in A \land n - m \in B)\}), (n \in ℕ_{0} ⟼ if (n = 0, \emptyset, n - 1)))$
	smueq.q	$⊢ Q = seq 0 ((p \in 𝒫 ℕ_{0}, m \in ℕ_{0} ⟼ p sadd \{n \in ℕ_{0} \| (m \in A \land n - m \in (B \cap (0 ..^N)))\}), (n \in ℕ_{0} ⟼ if (n = 0, \emptyset, n - 1)))$
Assertion	smueqlem	$⊢ φ \to (A smul B) \cap (0 ..^N) = ((A \cap (0 ..^N)) smul (B \cap (0 ..^N))) \cap (0 ..^N)$

Proof

Step	Hyp	Ref	Expression
1		smueq.a	$⊢ φ \to A \subseteq ℕ_{0}$
2		smueq.b	$⊢ φ \to B \subseteq ℕ_{0}$
3		smueq.n	$⊢ φ \to N \in ℕ_{0}$
4		smueq.p	$⊢ P = seq 0 ((p \in 𝒫 ℕ_{0}, m \in ℕ_{0} ⟼ p sadd \{n \in ℕ_{0} \| (m \in A \land n - m \in B)\}), (n \in ℕ_{0} ⟼ if (n = 0, \emptyset, n - 1)))$
5		smueq.q	$⊢ Q = seq 0 ((p \in 𝒫 ℕ_{0}, m \in ℕ_{0} ⟼ p sadd \{n \in ℕ_{0} \| (m \in A \land n - m \in (B \cap (0 ..^N)))\}), (n \in ℕ_{0} ⟼ if (n = 0, \emptyset, n - 1)))$
6	1	adantr	$⊢ (φ \land k \in (0 ..^N)) \to A \subseteq ℕ_{0}$
7	2	adantr	$⊢ (φ \land k \in (0 ..^N)) \to B \subseteq ℕ_{0}$
8		elfzouz	$⊢ k \in (0 ..^N) \to k \in ℤ_{\geq 0}$
9	8	adantl	$⊢ (φ \land k \in (0 ..^N)) \to k \in ℤ_{\geq 0}$
10		nn0uz	$⊢ ℕ_{0} = ℤ_{\geq 0}$
11	9 10	eleqtrrdi	$⊢ (φ \land k \in (0 ..^N)) \to k \in ℕ_{0}$
12	11	nn0zd	$⊢ (φ \land k \in (0 ..^N)) \to k \in ℤ$
13	12	peano2zd	$⊢ (φ \land k \in (0 ..^N)) \to k + 1 \in ℤ$
14	3	adantr	$⊢ (φ \land k \in (0 ..^N)) \to N \in ℕ_{0}$
15	14	nn0zd	$⊢ (φ \land k \in (0 ..^N)) \to N \in ℤ$
16		elfzolt2	$⊢ k \in (0 ..^N) \to k < N$
17	16	adantl	$⊢ (φ \land k \in (0 ..^N)) \to k < N$
18		nn0ltp1le	$⊢ (k \in ℕ_{0} \land N \in ℕ_{0}) \to (k < N \leftrightarrow k + 1 \leq N)$
19	11 14 18	syl2anc	$⊢ (φ \land k \in (0 ..^N)) \to (k < N \leftrightarrow k + 1 \leq N)$
20	17 19	mpbid	$⊢ (φ \land k \in (0 ..^N)) \to k + 1 \leq N$
21		eluz2	$⊢ N \in ℤ_{\geq (k + 1)} \leftrightarrow (k + 1 \in ℤ \land N \in ℤ \land k + 1 \leq N)$
22	13 15 20 21	syl3anbrc	$⊢ (φ \land k \in (0 ..^N)) \to N \in ℤ_{\geq (k + 1)}$
23	6 7 4 11 22	smuval2	$⊢ (φ \land k \in (0 ..^N)) \to (k \in (A smul B) \leftrightarrow k \in P (N))$
24	3 10	eleqtrdi	$⊢ φ \to N \in ℤ_{\geq 0}$
25		eluzfz2b	$⊢ N \in ℤ_{\geq 0} \leftrightarrow N \in (0 \dots N)$
26	24 25	sylib	$⊢ φ \to N \in (0 \dots N)$
27		fveq2	$⊢ x = 0 \to P (x) = P (0)$
28	27	ineq1d	$⊢ x = 0 \to P (x) \cap (0 ..^N) = P (0) \cap (0 ..^N)$
29		fveq2	$⊢ x = 0 \to Q (x) = Q (0)$
30	29	ineq1d	$⊢ x = 0 \to Q (x) \cap (0 ..^N) = Q (0) \cap (0 ..^N)$
31	28 30	eqeq12d	$⊢ x = 0 \to (P (x) \cap (0 ..^N) = Q (x) \cap (0 ..^N) \leftrightarrow P (0) \cap (0 ..^N) = Q (0) \cap (0 ..^N))$
32	31	imbi2d	$⊢ x = 0 \to ((φ \to P (x) \cap (0 ..^N) = Q (x) \cap (0 ..^N)) \leftrightarrow (φ \to P (0) \cap (0 ..^N) = Q (0) \cap (0 ..^N)))$
33		fveq2	$⊢ x = i \to P (x) = P (i)$
34	33	ineq1d	$⊢ x = i \to P (x) \cap (0 ..^N) = P (i) \cap (0 ..^N)$
35		fveq2	$⊢ x = i \to Q (x) = Q (i)$
36	35	ineq1d	$⊢ x = i \to Q (x) \cap (0 ..^N) = Q (i) \cap (0 ..^N)$
37	34 36	eqeq12d	$⊢ x = i \to (P (x) \cap (0 ..^N) = Q (x) \cap (0 ..^N) \leftrightarrow P (i) \cap (0 ..^N) = Q (i) \cap (0 ..^N))$
38	37	imbi2d	$⊢ x = i \to ((φ \to P (x) \cap (0 ..^N) = Q (x) \cap (0 ..^N)) \leftrightarrow (φ \to P (i) \cap (0 ..^N) = Q (i) \cap (0 ..^N)))$
39		fveq2	$⊢ x = i + 1 \to P (x) = P (i + 1)$
40	39	ineq1d	$⊢ x = i + 1 \to P (x) \cap (0 ..^N) = P (i + 1) \cap (0 ..^N)$
41		fveq2	$⊢ x = i + 1 \to Q (x) = Q (i + 1)$
42	41	ineq1d	$⊢ x = i + 1 \to Q (x) \cap (0 ..^N) = Q (i + 1) \cap (0 ..^N)$
43	40 42	eqeq12d	$⊢ x = i + 1 \to (P (x) \cap (0 ..^N) = Q (x) \cap (0 ..^N) \leftrightarrow P (i + 1) \cap (0 ..^N) = Q (i + 1) \cap (0 ..^N))$
44	43	imbi2d	$⊢ x = i + 1 \to ((φ \to P (x) \cap (0 ..^N) = Q (x) \cap (0 ..^N)) \leftrightarrow (φ \to P (i + 1) \cap (0 ..^N) = Q (i + 1) \cap (0 ..^N)))$
45		fveq2	$⊢ x = N \to P (x) = P (N)$
46	45	ineq1d	$⊢ x = N \to P (x) \cap (0 ..^N) = P (N) \cap (0 ..^N)$
47		fveq2	$⊢ x = N \to Q (x) = Q (N)$
48	47	ineq1d	$⊢ x = N \to Q (x) \cap (0 ..^N) = Q (N) \cap (0 ..^N)$
49	46 48	eqeq12d	$⊢ x = N \to (P (x) \cap (0 ..^N) = Q (x) \cap (0 ..^N) \leftrightarrow P (N) \cap (0 ..^N) = Q (N) \cap (0 ..^N))$
50	49	imbi2d	$⊢ x = N \to ((φ \to P (x) \cap (0 ..^N) = Q (x) \cap (0 ..^N)) \leftrightarrow (φ \to P (N) \cap (0 ..^N) = Q (N) \cap (0 ..^N)))$
51	1 2 4	smup0	$⊢ φ \to P (0) = \emptyset$
52		inss1	$⊢ B \cap (0 ..^N) \subseteq B$
53	52 2	sstrid	$⊢ φ \to B \cap (0 ..^N) \subseteq ℕ_{0}$
54	1 53 5	smup0	$⊢ φ \to Q (0) = \emptyset$
55	51 54	eqtr4d	$⊢ φ \to P (0) = Q (0)$
56	55	ineq1d	$⊢ φ \to P (0) \cap (0 ..^N) = Q (0) \cap (0 ..^N)$
57	56	a1i	$⊢ N \in ℤ_{\geq 0} \to (φ \to P (0) \cap (0 ..^N) = Q (0) \cap (0 ..^N))$
58		oveq1	$⊢ P (i) \cap (0 ..^N) = Q (i) \cap (0 ..^N) \to (P (i) \cap (0 ..^N)) sadd (\{n \in ℕ_{0} \| (i \in A \land n - i \in B)\} \cap (0 ..^N)) = (Q (i) \cap (0 ..^N)) sadd (\{n \in ℕ_{0} \| (i \in A \land n - i \in B)\} \cap (0 ..^N))$
59	58	ineq1d	$⊢ P (i) \cap (0 ..^N) = Q (i) \cap (0 ..^N) \to ((P (i) \cap (0 ..^N)) sadd (\{n \in ℕ_{0} \| (i \in A \land n - i \in B)\} \cap (0 ..^N))) \cap (0 ..^N) = ((Q (i) \cap (0 ..^N)) sadd (\{n \in ℕ_{0} \| (i \in A \land n - i \in B)\} \cap (0 ..^N))) \cap (0 ..^N)$
60	1	adantr	$⊢ (φ \land i \in (0 ..^N)) \to A \subseteq ℕ_{0}$
61	2	adantr	$⊢ (φ \land i \in (0 ..^N)) \to B \subseteq ℕ_{0}$
62		elfzonn0	$⊢ i \in (0 ..^N) \to i \in ℕ_{0}$
63	62	adantl	$⊢ (φ \land i \in (0 ..^N)) \to i \in ℕ_{0}$
64	60 61 4 63	smupp1	$⊢ (φ \land i \in (0 ..^N)) \to P (i + 1) = P (i) sadd \{n \in ℕ_{0} \| (i \in A \land n - i \in B)\}$
65	64	ineq1d	$⊢ (φ \land i \in (0 ..^N)) \to P (i + 1) \cap (0 ..^N) = (P (i) sadd \{n \in ℕ_{0} \| (i \in A \land n - i \in B)\}) \cap (0 ..^N)$
66	1 2 4	smupf	$⊢ φ \to P : ℕ_{0} ⟶ 𝒫 ℕ_{0}$
67		ffvelrn	$⊢ (P : ℕ_{0} ⟶ 𝒫 ℕ_{0} \land i \in ℕ_{0}) \to P (i) \in 𝒫 ℕ_{0}$
68	66 62 67	syl2an	$⊢ (φ \land i \in (0 ..^N)) \to P (i) \in 𝒫 ℕ_{0}$
69	68	elpwid	$⊢ (φ \land i \in (0 ..^N)) \to P (i) \subseteq ℕ_{0}$
70		ssrab2	$⊢ \{n \in ℕ_{0} \| (i \in A \land n - i \in B)\} \subseteq ℕ_{0}$
71	70	a1i	$⊢ (φ \land i \in (0 ..^N)) \to \{n \in ℕ_{0} \| (i \in A \land n - i \in B)\} \subseteq ℕ_{0}$
72	3	adantr	$⊢ (φ \land i \in (0 ..^N)) \to N \in ℕ_{0}$
73	69 71 72	sadeq	$⊢ (φ \land i \in (0 ..^N)) \to (P (i) sadd \{n \in ℕ_{0} \| (i \in A \land n - i \in B)\}) \cap (0 ..^N) = ((P (i) \cap (0 ..^N)) sadd (\{n \in ℕ_{0} \| (i \in A \land n - i \in B)\} \cap (0 ..^N))) \cap (0 ..^N)$
74	65 73	eqtrd	$⊢ (φ \land i \in (0 ..^N)) \to P (i + 1) \cap (0 ..^N) = ((P (i) \cap (0 ..^N)) sadd (\{n \in ℕ_{0} \| (i \in A \land n - i \in B)\} \cap (0 ..^N))) \cap (0 ..^N)$
75	53	adantr	$⊢ (φ \land i \in (0 ..^N)) \to B \cap (0 ..^N) \subseteq ℕ_{0}$
76	60 75 5 63	smupp1	$⊢ (φ \land i \in (0 ..^N)) \to Q (i + 1) = Q (i) sadd \{n \in ℕ_{0} \| (i \in A \land n - i \in (B \cap (0 ..^N)))\}$
77	76	ineq1d	$⊢ (φ \land i \in (0 ..^N)) \to Q (i + 1) \cap (0 ..^N) = (Q (i) sadd \{n \in ℕ_{0} \| (i \in A \land n - i \in (B \cap (0 ..^N)))\}) \cap (0 ..^N)$
78	1 53 5	smupf	$⊢ φ \to Q : ℕ_{0} ⟶ 𝒫 ℕ_{0}$
79		ffvelrn	$⊢ (Q : ℕ_{0} ⟶ 𝒫 ℕ_{0} \land i \in ℕ_{0}) \to Q (i) \in 𝒫 ℕ_{0}$
80	78 62 79	syl2an	$⊢ (φ \land i \in (0 ..^N)) \to Q (i) \in 𝒫 ℕ_{0}$
81	80	elpwid	$⊢ (φ \land i \in (0 ..^N)) \to Q (i) \subseteq ℕ_{0}$
82		ssrab2	$⊢ \{n \in ℕ_{0} \| (i \in A \land n - i \in (B \cap (0 ..^N)))\} \subseteq ℕ_{0}$
83	82	a1i	$⊢ (φ \land i \in (0 ..^N)) \to \{n \in ℕ_{0} \| (i \in A \land n - i \in (B \cap (0 ..^N)))\} \subseteq ℕ_{0}$
84	81 83 72	sadeq	$⊢ (φ \land i \in (0 ..^N)) \to (Q (i) sadd \{n \in ℕ_{0} \| (i \in A \land n - i \in (B \cap (0 ..^N)))\}) \cap (0 ..^N) = ((Q (i) \cap (0 ..^N)) sadd (\{n \in ℕ_{0} \| (i \in A \land n - i \in (B \cap (0 ..^N)))\} \cap (0 ..^N))) \cap (0 ..^N)$
85		elinel2	$⊢ n \in (ℕ_{0} \cap (0 ..^N)) \to n \in (0 ..^N)$
86	61	adantr	$⊢ ((φ \land i \in (0 ..^N)) \land n \in (0 ..^N)) \to B \subseteq ℕ_{0}$
87	86	sseld	$⊢ ((φ \land i \in (0 ..^N)) \land n \in (0 ..^N)) \to (n - i \in B \to n - i \in ℕ_{0})$
88		elfzo0	$⊢ n \in (0 ..^N) \leftrightarrow (n \in ℕ_{0} \land N \in ℕ \land n < N)$
89	88	simp2bi	$⊢ n \in (0 ..^N) \to N \in ℕ$
90	89	adantl	$⊢ ((φ \land i \in (0 ..^N)) \land n \in (0 ..^N)) \to N \in ℕ$
91		elfzonn0	$⊢ n \in (0 ..^N) \to n \in ℕ_{0}$
92	91	adantl	$⊢ ((φ \land i \in (0 ..^N)) \land n \in (0 ..^N)) \to n \in ℕ_{0}$
93	92	nn0red	$⊢ ((φ \land i \in (0 ..^N)) \land n \in (0 ..^N)) \to n \in ℝ$
94	63	adantr	$⊢ ((φ \land i \in (0 ..^N)) \land n \in (0 ..^N)) \to i \in ℕ_{0}$
95	94	nn0red	$⊢ ((φ \land i \in (0 ..^N)) \land n \in (0 ..^N)) \to i \in ℝ$
96	93 95	resubcld	$⊢ ((φ \land i \in (0 ..^N)) \land n \in (0 ..^N)) \to n - i \in ℝ$
97	90	nnred	$⊢ ((φ \land i \in (0 ..^N)) \land n \in (0 ..^N)) \to N \in ℝ$
98	94	nn0ge0d	$⊢ ((φ \land i \in (0 ..^N)) \land n \in (0 ..^N)) \to 0 \leq i$
99	93 95	subge02d	$⊢ ((φ \land i \in (0 ..^N)) \land n \in (0 ..^N)) \to (0 \leq i \leftrightarrow n - i \leq n)$
100	98 99	mpbid	$⊢ ((φ \land i \in (0 ..^N)) \land n \in (0 ..^N)) \to n - i \leq n$
101		elfzolt2	$⊢ n \in (0 ..^N) \to n < N$
102	101	adantl	$⊢ ((φ \land i \in (0 ..^N)) \land n \in (0 ..^N)) \to n < N$
103	96 93 97 100 102	lelttrd	$⊢ ((φ \land i \in (0 ..^N)) \land n \in (0 ..^N)) \to n - i < N$
104	90 103	jca	$⊢ ((φ \land i \in (0 ..^N)) \land n \in (0 ..^N)) \to (N \in ℕ \land n - i < N)$
105		elfzo0	$⊢ n - i \in (0 ..^N) \leftrightarrow (n - i \in ℕ_{0} \land N \in ℕ \land n - i < N)$
106		3anass	$⊢ (n - i \in ℕ_{0} \land N \in ℕ \land n - i < N) \leftrightarrow (n - i \in ℕ_{0} \land (N \in ℕ \land n - i < N))$
107	105 106	bitri	$⊢ n - i \in (0 ..^N) \leftrightarrow (n - i \in ℕ_{0} \land (N \in ℕ \land n - i < N))$
108	107	baib	$⊢ n - i \in ℕ_{0} \to (n - i \in (0 ..^N) \leftrightarrow (N \in ℕ \land n - i < N))$
109	104 108	syl5ibrcom	$⊢ ((φ \land i \in (0 ..^N)) \land n \in (0 ..^N)) \to (n - i \in ℕ_{0} \to n - i \in (0 ..^N))$
110	87 109	syld	$⊢ ((φ \land i \in (0 ..^N)) \land n \in (0 ..^N)) \to (n - i \in B \to n - i \in (0 ..^N))$
111	110	pm4.71rd	$⊢ ((φ \land i \in (0 ..^N)) \land n \in (0 ..^N)) \to (n - i \in B \leftrightarrow (n - i \in (0 ..^N) \land n - i \in B))$
112		ancom	$⊢ (n - i \in (0 ..^N) \land n - i \in B) \leftrightarrow (n - i \in B \land n - i \in (0 ..^N))$
113		elin	$⊢ n - i \in (B \cap (0 ..^N)) \leftrightarrow (n - i \in B \land n - i \in (0 ..^N))$
114	112 113	bitr4i	$⊢ (n - i \in (0 ..^N) \land n - i \in B) \leftrightarrow n - i \in (B \cap (0 ..^N))$
115	111 114	bitr2di	$⊢ ((φ \land i \in (0 ..^N)) \land n \in (0 ..^N)) \to (n - i \in (B \cap (0 ..^N)) \leftrightarrow n - i \in B)$
116	115	anbi2d	$⊢ ((φ \land i \in (0 ..^N)) \land n \in (0 ..^N)) \to ((i \in A \land n - i \in (B \cap (0 ..^N))) \leftrightarrow (i \in A \land n - i \in B))$
117	85 116	sylan2	$⊢ ((φ \land i \in (0 ..^N)) \land n \in (ℕ_{0} \cap (0 ..^N))) \to ((i \in A \land n - i \in (B \cap (0 ..^N))) \leftrightarrow (i \in A \land n - i \in B))$
118	117	rabbidva	$⊢ (φ \land i \in (0 ..^N)) \to \{n \in (ℕ_{0} \cap (0 ..^N)) \| (i \in A \land n - i \in (B \cap (0 ..^N)))\} = \{n \in (ℕ_{0} \cap (0 ..^N)) \| (i \in A \land n - i \in B)\}$
119		inrab2	$⊢ \{n \in ℕ_{0} \| (i \in A \land n - i \in (B \cap (0 ..^N)))\} \cap (0 ..^N) = \{n \in (ℕ_{0} \cap (0 ..^N)) \| (i \in A \land n - i \in (B \cap (0 ..^N)))\}$
120		inrab2	$⊢ \{n \in ℕ_{0} \| (i \in A \land n - i \in B)\} \cap (0 ..^N) = \{n \in (ℕ_{0} \cap (0 ..^N)) \| (i \in A \land n - i \in B)\}$
121	118 119 120	3eqtr4g	$⊢ (φ \land i \in (0 ..^N)) \to \{n \in ℕ_{0} \| (i \in A \land n - i \in (B \cap (0 ..^N)))\} \cap (0 ..^N) = \{n \in ℕ_{0} \| (i \in A \land n - i \in B)\} \cap (0 ..^N)$
122	121	oveq2d	$⊢ (φ \land i \in (0 ..^N)) \to (Q (i) \cap (0 ..^N)) sadd (\{n \in ℕ_{0} \| (i \in A \land n - i \in (B \cap (0 ..^N)))\} \cap (0 ..^N)) = (Q (i) \cap (0 ..^N)) sadd (\{n \in ℕ_{0} \| (i \in A \land n - i \in B)\} \cap (0 ..^N))$
123	122	ineq1d	$⊢ (φ \land i \in (0 ..^N)) \to ((Q (i) \cap (0 ..^N)) sadd (\{n \in ℕ_{0} \| (i \in A \land n - i \in (B \cap (0 ..^N)))\} \cap (0 ..^N))) \cap (0 ..^N) = ((Q (i) \cap (0 ..^N)) sadd (\{n \in ℕ_{0} \| (i \in A \land n - i \in B)\} \cap (0 ..^N))) \cap (0 ..^N)$
124	77 84 123	3eqtrd	$⊢ (φ \land i \in (0 ..^N)) \to Q (i + 1) \cap (0 ..^N) = ((Q (i) \cap (0 ..^N)) sadd (\{n \in ℕ_{0} \| (i \in A \land n - i \in B)\} \cap (0 ..^N))) \cap (0 ..^N)$
125	74 124	eqeq12d	$⊢ (φ \land i \in (0 ..^N)) \to (P (i + 1) \cap (0 ..^N) = Q (i + 1) \cap (0 ..^N) \leftrightarrow ((P (i) \cap (0 ..^N)) sadd (\{n \in ℕ_{0} \| (i \in A \land n - i \in B)\} \cap (0 ..^N))) \cap (0 ..^N) = ((Q (i) \cap (0 ..^N)) sadd (\{n \in ℕ_{0} \| (i \in A \land n - i \in B)\} \cap (0 ..^N))) \cap (0 ..^N))$
126	59 125	syl5ibr	$⊢ (φ \land i \in (0 ..^N)) \to (P (i) \cap (0 ..^N) = Q (i) \cap (0 ..^N) \to P (i + 1) \cap (0 ..^N) = Q (i + 1) \cap (0 ..^N))$
127	126	expcom	$⊢ i \in (0 ..^N) \to (φ \to (P (i) \cap (0 ..^N) = Q (i) \cap (0 ..^N) \to P (i + 1) \cap (0 ..^N) = Q (i + 1) \cap (0 ..^N)))$
128	127	a2d	$⊢ i \in (0 ..^N) \to ((φ \to P (i) \cap (0 ..^N) = Q (i) \cap (0 ..^N)) \to (φ \to P (i + 1) \cap (0 ..^N) = Q (i + 1) \cap (0 ..^N)))$
129	32 38 44 50 57 128	fzind2	$⊢ N \in (0 \dots N) \to (φ \to P (N) \cap (0 ..^N) = Q (N) \cap (0 ..^N))$
130	26 129	mpcom	$⊢ φ \to P (N) \cap (0 ..^N) = Q (N) \cap (0 ..^N)$
131	130	adantr	$⊢ (φ \land k \in (0 ..^N)) \to P (N) \cap (0 ..^N) = Q (N) \cap (0 ..^N)$
132	131	eleq2d	$⊢ (φ \land k \in (0 ..^N)) \to (k \in (P (N) \cap (0 ..^N)) \leftrightarrow k \in (Q (N) \cap (0 ..^N)))$
133		elin	$⊢ k \in (P (N) \cap (0 ..^N)) \leftrightarrow (k \in P (N) \land k \in (0 ..^N))$
134	133	rbaib	$⊢ k \in (0 ..^N) \to (k \in (P (N) \cap (0 ..^N)) \leftrightarrow k \in P (N))$
135	134	adantl	$⊢ (φ \land k \in (0 ..^N)) \to (k \in (P (N) \cap (0 ..^N)) \leftrightarrow k \in P (N))$
136		elin	$⊢ k \in (Q (N) \cap (0 ..^N)) \leftrightarrow (k \in Q (N) \land k \in (0 ..^N))$
137	136	rbaib	$⊢ k \in (0 ..^N) \to (k \in (Q (N) \cap (0 ..^N)) \leftrightarrow k \in Q (N))$
138	137	adantl	$⊢ (φ \land k \in (0 ..^N)) \to (k \in (Q (N) \cap (0 ..^N)) \leftrightarrow k \in Q (N))$
139	132 135 138	3bitr3d	$⊢ (φ \land k \in (0 ..^N)) \to (k \in P (N) \leftrightarrow k \in Q (N))$
140	53	adantr	$⊢ (φ \land k \in (0 ..^N)) \to B \cap (0 ..^N) \subseteq ℕ_{0}$
141	6 140 5 14	smupval	$⊢ (φ \land k \in (0 ..^N)) \to Q (N) = (A \cap (0 ..^N)) smul (B \cap (0 ..^N))$
142	141	eleq2d	$⊢ (φ \land k \in (0 ..^N)) \to (k \in Q (N) \leftrightarrow k \in ((A \cap (0 ..^N)) smul (B \cap (0 ..^N))))$
143	23 139 142	3bitrd	$⊢ (φ \land k \in (0 ..^N)) \to (k \in (A smul B) \leftrightarrow k \in ((A \cap (0 ..^N)) smul (B \cap (0 ..^N))))$
144	143	ex	$⊢ φ \to (k \in (0 ..^N) \to (k \in (A smul B) \leftrightarrow k \in ((A \cap (0 ..^N)) smul (B \cap (0 ..^N)))))$
145	144	pm5.32rd	$⊢ φ \to ((k \in (A smul B) \land k \in (0 ..^N)) \leftrightarrow (k \in ((A \cap (0 ..^N)) smul (B \cap (0 ..^N))) \land k \in (0 ..^N)))$
146		elin	$⊢ k \in ((A smul B) \cap (0 ..^N)) \leftrightarrow (k \in (A smul B) \land k \in (0 ..^N))$
147		elin	$⊢ k \in (((A \cap (0 ..^N)) smul (B \cap (0 ..^N))) \cap (0 ..^N)) \leftrightarrow (k \in ((A \cap (0 ..^N)) smul (B \cap (0 ..^N))) \land k \in (0 ..^N))$
148	145 146 147	3bitr4g	$⊢ φ \to (k \in ((A smul B) \cap (0 ..^N)) \leftrightarrow k \in (((A \cap (0 ..^N)) smul (B \cap (0 ..^N))) \cap (0 ..^N)))$
149	148	eqrdv	$⊢ φ \to (A smul B) \cap (0 ..^N) = ((A \cap (0 ..^N)) smul (B \cap (0 ..^N))) \cap (0 ..^N)$

Metamath Proof Explorer

Theorem smueqlem

Proof