selvply1rhmlemb

	Ref	Expression
Hypotheses	selvply1rhmlema.1	$⊢ B = {Base}_{P}$
	selvply1rhmlema.2	$⊢ P = \{X\} mPoly R$
	selvply1rhmlema.3	$⊢ \underset{˙}{\cdot} = \cdot_{P}$
	selvply1rhmlema.4	$⊢ \underset{˙}{\times} = \cdot_{Q}$
	selvply1rhmlema.5	$⊢ Q = {Poly}_{1} (R)$
	selvply1rhmlema.6	$⊢ M = (f \in B ⟼ (n \in ({ℕ_{0}}^{1_{𝑜}}) ⟼ f (\{⟨X, n (\emptyset)⟩\})))$
	selvply1rhmlema.7	$⊢ φ \to X \in V$
	selvply1rhmlema.8	$⊢ φ \to R \in Ring$
	selvply1rhmlema.9	$⊢ φ \to F \in B$
	selvply1rhmlemb.10	$⊢ φ \to G \in B$
Assertion	selvply1rhmlemb	$⊢ φ \to M (F \underset{˙}{\cdot} G) = M (F) \underset{˙}{\times} M (G)$

Proof

Step	Hyp	Ref	Expression
1		selvply1rhmlema.1	$⊢ B = {Base}_{P}$
2		selvply1rhmlema.2	$⊢ P = \{X\} mPoly R$
3		selvply1rhmlema.3	$⊢ \underset{˙}{\cdot} = \cdot_{P}$
4		selvply1rhmlema.4	$⊢ \underset{˙}{\times} = \cdot_{Q}$
5		selvply1rhmlema.5	$⊢ Q = {Poly}_{1} (R)$
6		selvply1rhmlema.6	$⊢ M = (f \in B ⟼ (n \in ({ℕ_{0}}^{1_{𝑜}}) ⟼ f (\{⟨X, n (\emptyset)⟩\})))$
7		selvply1rhmlema.7	$⊢ φ \to X \in V$
8		selvply1rhmlema.8	$⊢ φ \to R \in Ring$
9		selvply1rhmlema.9	$⊢ φ \to F \in B$
10		selvply1rhmlemb.10	$⊢ φ \to G \in B$
11		fveq1	$⊢ f = F \underset{˙}{\cdot} G \to f (\{⟨X, n (\emptyset)⟩\}) = (F \underset{˙}{\cdot} G) (\{⟨X, n (\emptyset)⟩\})$
12	11	mpteq2dv	$⊢ f = F \underset{˙}{\cdot} G \to (n \in ({ℕ_{0}}^{1_{𝑜}}) ⟼ f (\{⟨X, n (\emptyset)⟩\})) = (n \in ({ℕ_{0}}^{1_{𝑜}}) ⟼ (F \underset{˙}{\cdot} G) (\{⟨X, n (\emptyset)⟩\}))$
13		eqid	$⊢ \cdot_{R} = \cdot_{R}$
14		eqid	$⊢ \{g \in ({ℕ_{0}}^{\{X\}}) \| {finSupp}_{0} (g)\} = \{g \in ({ℕ_{0}}^{\{X\}}) \| {finSupp}_{0} (g)\}$
15	14	psrbasfsupp	$⊢ \{g \in ({ℕ_{0}}^{\{X\}}) \| {finSupp}_{0} (g)\} = \{g \in ({ℕ_{0}}^{\{X\}}) \| g^{-1} [ℕ] \in Fin\}$
16	2 1 13 3 15 9 10	mplmul	$⊢ φ \to F \underset{˙}{\cdot} G = (m \in \{g \in ({ℕ_{0}}^{\{X\}}) \| {finSupp}_{0} (g)\} ⟼ \underset{j \in \{l \in \{g \in ({ℕ_{0}}^{\{X\}}) \| {finSupp}_{0} (g)\} \| l \leq_{f} m\}}{\sum_{R}} (F (j) \cdot_{R} G (m -_{f} j)))$
17	16	adantr	$⊢ (φ \land n \in ({ℕ_{0}}^{1_{𝑜}})) \to F \underset{˙}{\cdot} G = (m \in \{g \in ({ℕ_{0}}^{\{X\}}) \| {finSupp}_{0} (g)\} ⟼ \underset{j \in \{l \in \{g \in ({ℕ_{0}}^{\{X\}}) \| {finSupp}_{0} (g)\} \| l \leq_{f} m\}}{\sum_{R}} (F (j) \cdot_{R} G (m -_{f} j)))$
18		breq2	$⊢ m = \{⟨X, n (\emptyset)⟩\} \to (l \leq_{f} m \leftrightarrow l \leq_{f} \{⟨X, n (\emptyset)⟩\})$
19	18	rabbidv	$⊢ m = \{⟨X, n (\emptyset)⟩\} \to \{l \in \{g \in ({ℕ_{0}}^{\{X\}}) \| {finSupp}_{0} (g)\} \| l \leq_{f} m\} = \{l \in \{g \in ({ℕ_{0}}^{\{X\}}) \| {finSupp}_{0} (g)\} \| l \leq_{f} \{⟨X, n (\emptyset)⟩\}\}$
20		fvoveq1	$⊢ m = \{⟨X, n (\emptyset)⟩\} \to G (m -_{f} j) = G (\{⟨X, n (\emptyset)⟩\} -_{f} j)$
21	20	oveq2d	$⊢ m = \{⟨X, n (\emptyset)⟩\} \to F (j) \cdot_{R} G (m -_{f} j) = F (j) \cdot_{R} G (\{⟨X, n (\emptyset)⟩\} -_{f} j)$
22	19 21	mpteq12dv	$⊢ m = \{⟨X, n (\emptyset)⟩\} \to (j \in \{l \in \{g \in ({ℕ_{0}}^{\{X\}}) \| {finSupp}_{0} (g)\} \| l \leq_{f} m\} ⟼ F (j) \cdot_{R} G (m -_{f} j)) = (j \in \{l \in \{g \in ({ℕ_{0}}^{\{X\}}) \| {finSupp}_{0} (g)\} \| l \leq_{f} \{⟨X, n (\emptyset)⟩\}\} ⟼ F (j) \cdot_{R} G (\{⟨X, n (\emptyset)⟩\} -_{f} j))$
23	22	oveq2d	$⊢ m = \{⟨X, n (\emptyset)⟩\} \to \underset{j \in \{l \in \{g \in ({ℕ_{0}}^{\{X\}}) \| {finSupp}_{0} (g)\} \| l \leq_{f} m\}}{\sum_{R}} (F (j) \cdot_{R} G (m -_{f} j)) = \underset{j \in \{l \in \{g \in ({ℕ_{0}}^{\{X\}}) \| {finSupp}_{0} (g)\} \| l \leq_{f} \{⟨X, n (\emptyset)⟩\}\}}{\sum_{R}} (F (j) \cdot_{R} G (\{⟨X, n (\emptyset)⟩\} -_{f} j))$
24		nfcv	$⊢ \underline{Ⅎ} j (F (\{⟨X, i (\emptyset)⟩\}) \cdot_{R} G (\{⟨X, n (\emptyset)⟩\} -_{f} \{⟨X, i (\emptyset)⟩\}))$
25		eqid	$⊢ {Base}_{R} = {Base}_{R}$
26		eqid	$⊢ 0_{R} = 0_{R}$
27		fveq2	$⊢ j = \{⟨X, i (\emptyset)⟩\} \to F (j) = F (\{⟨X, i (\emptyset)⟩\})$
28		oveq2	$⊢ j = \{⟨X, i (\emptyset)⟩\} \to \{⟨X, n (\emptyset)⟩\} -_{f} j = \{⟨X, n (\emptyset)⟩\} -_{f} \{⟨X, i (\emptyset)⟩\}$
29	28	fveq2d	$⊢ j = \{⟨X, i (\emptyset)⟩\} \to G (\{⟨X, n (\emptyset)⟩\} -_{f} j) = G (\{⟨X, n (\emptyset)⟩\} -_{f} \{⟨X, i (\emptyset)⟩\})$
30	27 29	oveq12d	$⊢ j = \{⟨X, i (\emptyset)⟩\} \to F (j) \cdot_{R} G (\{⟨X, n (\emptyset)⟩\} -_{f} j) = F (\{⟨X, i (\emptyset)⟩\}) \cdot_{R} G (\{⟨X, n (\emptyset)⟩\} -_{f} \{⟨X, i (\emptyset)⟩\})$
31	8	ringcmnd	$⊢ φ \to R \in CMnd$
32	31	adantr	$⊢ (φ \land n \in ({ℕ_{0}}^{1_{𝑜}})) \to R \in CMnd$
33		eqid	$⊢ \{l \in \{g \in ({ℕ_{0}}^{\{X\}}) \| {finSupp}_{0} (g)\} \| l \leq_{f} \{⟨X, n (\emptyset)⟩\}\} = \{l \in \{g \in ({ℕ_{0}}^{\{X\}}) \| {finSupp}_{0} (g)\} \| l \leq_{f} \{⟨X, n (\emptyset)⟩\}\}$
34		ovexd	$⊢ φ \to {ℕ_{0}}^{\{X\}} \in V$
35	14 34	rabexd	$⊢ φ \to \{g \in ({ℕ_{0}}^{\{X\}}) \| {finSupp}_{0} (g)\} \in V$
36	33 35	rabexd	$⊢ φ \to \{l \in \{g \in ({ℕ_{0}}^{\{X\}}) \| {finSupp}_{0} (g)\} \| l \leq_{f} \{⟨X, n (\emptyset)⟩\}\} \in V$
37	36	adantr	$⊢ (φ \land n \in ({ℕ_{0}}^{1_{𝑜}})) \to \{l \in \{g \in ({ℕ_{0}}^{\{X\}}) \| {finSupp}_{0} (g)\} \| l \leq_{f} \{⟨X, n (\emptyset)⟩\}\} \in V$
38		fvexd	$⊢ (φ \land n \in ({ℕ_{0}}^{1_{𝑜}})) \to 0_{R} \in V$
39	35	adantr	$⊢ (φ \land n \in ({ℕ_{0}}^{1_{𝑜}})) \to \{g \in ({ℕ_{0}}^{\{X\}}) \| {finSupp}_{0} (g)\} \in V$
40		ssrab2	$⊢ \{l \in \{g \in ({ℕ_{0}}^{\{X\}}) \| {finSupp}_{0} (g)\} \| l \leq_{f} \{⟨X, n (\emptyset)⟩\}\} \subseteq \{g \in ({ℕ_{0}}^{\{X\}}) \| {finSupp}_{0} (g)\}$
41	40	a1i	$⊢ (φ \land n \in ({ℕ_{0}}^{1_{𝑜}})) \to \{l \in \{g \in ({ℕ_{0}}^{\{X\}}) \| {finSupp}_{0} (g)\} \| l \leq_{f} \{⟨X, n (\emptyset)⟩\}\} \subseteq \{g \in ({ℕ_{0}}^{\{X\}}) \| {finSupp}_{0} (g)\}$
42	2 25 1 15 10	mplelf	$⊢ φ \to G : \{g \in ({ℕ_{0}}^{\{X\}}) \| {finSupp}_{0} (g)\} ⟶ {Base}_{R}$
43	42	ad2antrr	$⊢ ((φ \land n \in ({ℕ_{0}}^{1_{𝑜}})) \land j \in \{l \in \{g \in ({ℕ_{0}}^{\{X\}}) \| {finSupp}_{0} (g)\} \| l \leq_{f} \{⟨X, n (\emptyset)⟩\}\}) \to G : \{g \in ({ℕ_{0}}^{\{X\}}) \| {finSupp}_{0} (g)\} ⟶ {Base}_{R}$
44		breq1	$⊢ g = \{⟨X, n (\emptyset)⟩\} \to ({finSupp}_{0} (g) \leftrightarrow {finSupp}_{0} (\{⟨X, n (\emptyset)⟩\}))$
45		nn0ex	$⊢ ℕ_{0} \in V$
46	45	a1i	$⊢ (φ \land n \in ({ℕ_{0}}^{1_{𝑜}})) \to ℕ_{0} \in V$
47		snex	$⊢ \{X\} \in V$
48	47	a1i	$⊢ (φ \land n \in ({ℕ_{0}}^{1_{𝑜}})) \to \{X\} \in V$
49	7	adantr	$⊢ (φ \land n \in ({ℕ_{0}}^{1_{𝑜}})) \to X \in V$
50		1oex	$⊢ 1_{𝑜} \in V$
51	50	a1i	$⊢ (φ \land n \in ({ℕ_{0}}^{1_{𝑜}})) \to 1_{𝑜} \in V$
52		simpr	$⊢ (φ \land n \in ({ℕ_{0}}^{1_{𝑜}})) \to n \in ({ℕ_{0}}^{1_{𝑜}})$
53	51 46 52	elmaprd	$⊢ (φ \land n \in ({ℕ_{0}}^{1_{𝑜}})) \to n : 1_{𝑜} ⟶ ℕ_{0}$
54		0lt1o	$⊢ \emptyset \in 1_{𝑜}$
55	54	a1i	$⊢ (φ \land n \in ({ℕ_{0}}^{1_{𝑜}})) \to \emptyset \in 1_{𝑜}$
56	53 55	ffvelcdmd	$⊢ (φ \land n \in ({ℕ_{0}}^{1_{𝑜}})) \to n (\emptyset) \in ℕ_{0}$
57	49 56	fsnd	$⊢ (φ \land n \in ({ℕ_{0}}^{1_{𝑜}})) \to \{⟨X, n (\emptyset)⟩\} : \{X\} ⟶ ℕ_{0}$
58	46 48 57	elmapdd	$⊢ (φ \land n \in ({ℕ_{0}}^{1_{𝑜}})) \to \{⟨X, n (\emptyset)⟩\} \in ({ℕ_{0}}^{\{X\}})$
59		snfi	$⊢ \{X\} \in Fin$
60	59	a1i	$⊢ (φ \land n \in ({ℕ_{0}}^{1_{𝑜}})) \to \{X\} \in Fin$
61		c0ex	$⊢ 0 \in V$
62	61	a1i	$⊢ (φ \land n \in ({ℕ_{0}}^{1_{𝑜}})) \to 0 \in V$
63	57 60 62	fdmfifsupp	$⊢ (φ \land n \in ({ℕ_{0}}^{1_{𝑜}})) \to {finSupp}_{0} (\{⟨X, n (\emptyset)⟩\})$
64	44 58 63	elrabd	$⊢ (φ \land n \in ({ℕ_{0}}^{1_{𝑜}})) \to \{⟨X, n (\emptyset)⟩\} \in \{g \in ({ℕ_{0}}^{\{X\}}) \| {finSupp}_{0} (g)\}$
65	64	adantr	$⊢ ((φ \land n \in ({ℕ_{0}}^{1_{𝑜}})) \land j \in \{l \in \{g \in ({ℕ_{0}}^{\{X\}}) \| {finSupp}_{0} (g)\} \| l \leq_{f} \{⟨X, n (\emptyset)⟩\}\}) \to \{⟨X, n (\emptyset)⟩\} \in \{g \in ({ℕ_{0}}^{\{X\}}) \| {finSupp}_{0} (g)\}$
66	47	a1i	$⊢ ((φ \land n \in ({ℕ_{0}}^{1_{𝑜}})) \land j \in \{l \in \{g \in ({ℕ_{0}}^{\{X\}}) \| {finSupp}_{0} (g)\} \| l \leq_{f} \{⟨X, n (\emptyset)⟩\}\}) \to \{X\} \in V$
67	45	a1i	$⊢ ((φ \land n \in ({ℕ_{0}}^{1_{𝑜}})) \land j \in \{l \in \{g \in ({ℕ_{0}}^{\{X\}}) \| {finSupp}_{0} (g)\} \| l \leq_{f} \{⟨X, n (\emptyset)⟩\}\}) \to ℕ_{0} \in V$
68		ssrab2	$⊢ \{g \in ({ℕ_{0}}^{\{X\}}) \| {finSupp}_{0} (g)\} \subseteq {ℕ_{0}}^{\{X\}}$
69	40 68	sstri	$⊢ \{l \in \{g \in ({ℕ_{0}}^{\{X\}}) \| {finSupp}_{0} (g)\} \| l \leq_{f} \{⟨X, n (\emptyset)⟩\}\} \subseteq {ℕ_{0}}^{\{X\}}$
70	69	a1i	$⊢ (φ \land n \in ({ℕ_{0}}^{1_{𝑜}})) \to \{l \in \{g \in ({ℕ_{0}}^{\{X\}}) \| {finSupp}_{0} (g)\} \| l \leq_{f} \{⟨X, n (\emptyset)⟩\}\} \subseteq {ℕ_{0}}^{\{X\}}$
71	70	sselda	$⊢ ((φ \land n \in ({ℕ_{0}}^{1_{𝑜}})) \land j \in \{l \in \{g \in ({ℕ_{0}}^{\{X\}}) \| {finSupp}_{0} (g)\} \| l \leq_{f} \{⟨X, n (\emptyset)⟩\}\}) \to j \in ({ℕ_{0}}^{\{X\}})$
72	66 67 71	elmaprd	$⊢ ((φ \land n \in ({ℕ_{0}}^{1_{𝑜}})) \land j \in \{l \in \{g \in ({ℕ_{0}}^{\{X\}}) \| {finSupp}_{0} (g)\} \| l \leq_{f} \{⟨X, n (\emptyset)⟩\}\}) \to j : \{X\} ⟶ ℕ_{0}$
73		breq1	$⊢ l = j \to (l \leq_{f} \{⟨X, n (\emptyset)⟩\} \leftrightarrow j \leq_{f} \{⟨X, n (\emptyset)⟩\})$
74		simpr	$⊢ ((φ \land n \in ({ℕ_{0}}^{1_{𝑜}})) \land j \in \{l \in \{g \in ({ℕ_{0}}^{\{X\}}) \| {finSupp}_{0} (g)\} \| l \leq_{f} \{⟨X, n (\emptyset)⟩\}\}) \to j \in \{l \in \{g \in ({ℕ_{0}}^{\{X\}}) \| {finSupp}_{0} (g)\} \| l \leq_{f} \{⟨X, n (\emptyset)⟩\}\}$
75	73 74	elrabrd	$⊢ ((φ \land n \in ({ℕ_{0}}^{1_{𝑜}})) \land j \in \{l \in \{g \in ({ℕ_{0}}^{\{X\}}) \| {finSupp}_{0} (g)\} \| l \leq_{f} \{⟨X, n (\emptyset)⟩\}\}) \to j \leq_{f} \{⟨X, n (\emptyset)⟩\}$
76	15	psrbagcon	$⊢ (\{⟨X, n (\emptyset)⟩\} \in \{g \in ({ℕ_{0}}^{\{X\}}) \| {finSupp}_{0} (g)\} \land j : \{X\} ⟶ ℕ_{0} \land j \leq_{f} \{⟨X, n (\emptyset)⟩\}) \to (\{⟨X, n (\emptyset)⟩\} -_{f} j \in \{g \in ({ℕ_{0}}^{\{X\}}) \| {finSupp}_{0} (g)\} \land (\{⟨X, n (\emptyset)⟩\} -_{f} j) \leq_{f} \{⟨X, n (\emptyset)⟩\})$
77	65 72 75 76	syl3anc	$⊢ ((φ \land n \in ({ℕ_{0}}^{1_{𝑜}})) \land j \in \{l \in \{g \in ({ℕ_{0}}^{\{X\}}) \| {finSupp}_{0} (g)\} \| l \leq_{f} \{⟨X, n (\emptyset)⟩\}\}) \to (\{⟨X, n (\emptyset)⟩\} -_{f} j \in \{g \in ({ℕ_{0}}^{\{X\}}) \| {finSupp}_{0} (g)\} \land (\{⟨X, n (\emptyset)⟩\} -_{f} j) \leq_{f} \{⟨X, n (\emptyset)⟩\})$
78	77	simpld	$⊢ ((φ \land n \in ({ℕ_{0}}^{1_{𝑜}})) \land j \in \{l \in \{g \in ({ℕ_{0}}^{\{X\}}) \| {finSupp}_{0} (g)\} \| l \leq_{f} \{⟨X, n (\emptyset)⟩\}\}) \to \{⟨X, n (\emptyset)⟩\} -_{f} j \in \{g \in ({ℕ_{0}}^{\{X\}}) \| {finSupp}_{0} (g)\}$
79	43 78	ffvelcdmd	$⊢ ((φ \land n \in ({ℕ_{0}}^{1_{𝑜}})) \land j \in \{l \in \{g \in ({ℕ_{0}}^{\{X\}}) \| {finSupp}_{0} (g)\} \| l \leq_{f} \{⟨X, n (\emptyset)⟩\}\}) \to G (\{⟨X, n (\emptyset)⟩\} -_{f} j) \in {Base}_{R}$
80	2 25 1 15 9	mplelf	$⊢ φ \to F : \{g \in ({ℕ_{0}}^{\{X\}}) \| {finSupp}_{0} (g)\} ⟶ {Base}_{R}$
81	80	adantr	$⊢ (φ \land n \in ({ℕ_{0}}^{1_{𝑜}})) \to F : \{g \in ({ℕ_{0}}^{\{X\}}) \| {finSupp}_{0} (g)\} ⟶ {Base}_{R}$
82	2 1 26 9	mplelsfi	$⊢ φ \to {finSupp}_{0_{R}} (F)$
83	82	adantr	$⊢ (φ \land n \in ({ℕ_{0}}^{1_{𝑜}})) \to {finSupp}_{0_{R}} (F)$
84	8	ad2antrr	$⊢ ((φ \land n \in ({ℕ_{0}}^{1_{𝑜}})) \land x \in {Base}_{R}) \to R \in Ring$
85		simpr	$⊢ ((φ \land n \in ({ℕ_{0}}^{1_{𝑜}})) \land x \in {Base}_{R}) \to x \in {Base}_{R}$
86	25 13 26 84 85	ringlzd	$⊢ ((φ \land n \in ({ℕ_{0}}^{1_{𝑜}})) \land x \in {Base}_{R}) \to 0_{R} \cdot_{R} x = 0_{R}$
87	38 38 39 41 79 81 83 86	fisuppov1	$⊢ (φ \land n \in ({ℕ_{0}}^{1_{𝑜}})) \to {finSupp}_{0_{R}} ((j \in \{l \in \{g \in ({ℕ_{0}}^{\{X\}}) \| {finSupp}_{0} (g)\} \| l \leq_{f} \{⟨X, n (\emptyset)⟩\}\} ⟼ F (j) \cdot_{R} G (\{⟨X, n (\emptyset)⟩\} -_{f} j)))$
88		ssidd	$⊢ (φ \land n \in ({ℕ_{0}}^{1_{𝑜}})) \to {Base}_{R} \subseteq {Base}_{R}$
89	8	ad2antrr	$⊢ ((φ \land n \in ({ℕ_{0}}^{1_{𝑜}})) \land j \in \{l \in \{g \in ({ℕ_{0}}^{\{X\}}) \| {finSupp}_{0} (g)\} \| l \leq_{f} \{⟨X, n (\emptyset)⟩\}\}) \to R \in Ring$
90	80	ad2antrr	$⊢ ((φ \land n \in ({ℕ_{0}}^{1_{𝑜}})) \land j \in \{l \in \{g \in ({ℕ_{0}}^{\{X\}}) \| {finSupp}_{0} (g)\} \| l \leq_{f} \{⟨X, n (\emptyset)⟩\}\}) \to F : \{g \in ({ℕ_{0}}^{\{X\}}) \| {finSupp}_{0} (g)\} ⟶ {Base}_{R}$
91	41	sselda	$⊢ ((φ \land n \in ({ℕ_{0}}^{1_{𝑜}})) \land j \in \{l \in \{g \in ({ℕ_{0}}^{\{X\}}) \| {finSupp}_{0} (g)\} \| l \leq_{f} \{⟨X, n (\emptyset)⟩\}\}) \to j \in \{g \in ({ℕ_{0}}^{\{X\}}) \| {finSupp}_{0} (g)\}$
92	90 91	ffvelcdmd	$⊢ ((φ \land n \in ({ℕ_{0}}^{1_{𝑜}})) \land j \in \{l \in \{g \in ({ℕ_{0}}^{\{X\}}) \| {finSupp}_{0} (g)\} \| l \leq_{f} \{⟨X, n (\emptyset)⟩\}\}) \to F (j) \in {Base}_{R}$
93	25 13 89 92 79	ringcld	$⊢ ((φ \land n \in ({ℕ_{0}}^{1_{𝑜}})) \land j \in \{l \in \{g \in ({ℕ_{0}}^{\{X\}}) \| {finSupp}_{0} (g)\} \| l \leq_{f} \{⟨X, n (\emptyset)⟩\}\}) \to F (j) \cdot_{R} G (\{⟨X, n (\emptyset)⟩\} -_{f} j) \in {Base}_{R}$
94		breq1	$⊢ l = \{⟨X, i (\emptyset)⟩\} \to (l \leq_{f} \{⟨X, n (\emptyset)⟩\} \leftrightarrow \{⟨X, i (\emptyset)⟩\} \leq_{f} \{⟨X, n (\emptyset)⟩\})$
95		breq1	$⊢ g = \{⟨X, i (\emptyset)⟩\} \to ({finSupp}_{0} (g) \leftrightarrow {finSupp}_{0} (\{⟨X, i (\emptyset)⟩\}))$
96	45	a1i	$⊢ ((φ \land n \in ({ℕ_{0}}^{1_{𝑜}})) \land i \in \{k \in ({ℕ_{0}}^{1_{𝑜}}) \| k \leq_{f} n\}) \to ℕ_{0} \in V$
97	47	a1i	$⊢ ((φ \land n \in ({ℕ_{0}}^{1_{𝑜}})) \land i \in \{k \in ({ℕ_{0}}^{1_{𝑜}}) \| k \leq_{f} n\}) \to \{X\} \in V$
98	49	adantr	$⊢ ((φ \land n \in ({ℕ_{0}}^{1_{𝑜}})) \land i \in \{k \in ({ℕ_{0}}^{1_{𝑜}}) \| k \leq_{f} n\}) \to X \in V$
99	50	a1i	$⊢ ((φ \land n \in ({ℕ_{0}}^{1_{𝑜}})) \land i \in \{k \in ({ℕ_{0}}^{1_{𝑜}}) \| k \leq_{f} n\}) \to 1_{𝑜} \in V$
100		ssrab2	$⊢ \{k \in ({ℕ_{0}}^{1_{𝑜}}) \| k \leq_{f} n\} \subseteq {ℕ_{0}}^{1_{𝑜}}$
101	100	a1i	$⊢ (φ \land n \in ({ℕ_{0}}^{1_{𝑜}})) \to \{k \in ({ℕ_{0}}^{1_{𝑜}}) \| k \leq_{f} n\} \subseteq {ℕ_{0}}^{1_{𝑜}}$
102	101	sselda	$⊢ ((φ \land n \in ({ℕ_{0}}^{1_{𝑜}})) \land i \in \{k \in ({ℕ_{0}}^{1_{𝑜}}) \| k \leq_{f} n\}) \to i \in ({ℕ_{0}}^{1_{𝑜}})$
103	99 96 102	elmaprd	$⊢ ((φ \land n \in ({ℕ_{0}}^{1_{𝑜}})) \land i \in \{k \in ({ℕ_{0}}^{1_{𝑜}}) \| k \leq_{f} n\}) \to i : 1_{𝑜} ⟶ ℕ_{0}$
104	54	a1i	$⊢ ((φ \land n \in ({ℕ_{0}}^{1_{𝑜}})) \land i \in \{k \in ({ℕ_{0}}^{1_{𝑜}}) \| k \leq_{f} n\}) \to \emptyset \in 1_{𝑜}$
105	103 104	ffvelcdmd	$⊢ ((φ \land n \in ({ℕ_{0}}^{1_{𝑜}})) \land i \in \{k \in ({ℕ_{0}}^{1_{𝑜}}) \| k \leq_{f} n\}) \to i (\emptyset) \in ℕ_{0}$
106	98 105	fsnd	$⊢ ((φ \land n \in ({ℕ_{0}}^{1_{𝑜}})) \land i \in \{k \in ({ℕ_{0}}^{1_{𝑜}}) \| k \leq_{f} n\}) \to \{⟨X, i (\emptyset)⟩\} : \{X\} ⟶ ℕ_{0}$
107	96 97 106	elmapdd	$⊢ ((φ \land n \in ({ℕ_{0}}^{1_{𝑜}})) \land i \in \{k \in ({ℕ_{0}}^{1_{𝑜}}) \| k \leq_{f} n\}) \to \{⟨X, i (\emptyset)⟩\} \in ({ℕ_{0}}^{\{X\}})$
108	59	a1i	$⊢ ((φ \land n \in ({ℕ_{0}}^{1_{𝑜}})) \land i \in \{k \in ({ℕ_{0}}^{1_{𝑜}}) \| k \leq_{f} n\}) \to \{X\} \in Fin$
109	61	a1i	$⊢ ((φ \land n \in ({ℕ_{0}}^{1_{𝑜}})) \land i \in \{k \in ({ℕ_{0}}^{1_{𝑜}}) \| k \leq_{f} n\}) \to 0 \in V$
110	106 108 109	fdmfifsupp	$⊢ ((φ \land n \in ({ℕ_{0}}^{1_{𝑜}})) \land i \in \{k \in ({ℕ_{0}}^{1_{𝑜}}) \| k \leq_{f} n\}) \to {finSupp}_{0} (\{⟨X, i (\emptyset)⟩\})$
111	95 107 110	elrabd	$⊢ ((φ \land n \in ({ℕ_{0}}^{1_{𝑜}})) \land i \in \{k \in ({ℕ_{0}}^{1_{𝑜}}) \| k \leq_{f} n\}) \to \{⟨X, i (\emptyset)⟩\} \in \{g \in ({ℕ_{0}}^{\{X\}}) \| {finSupp}_{0} (g)\}$
112		simplr	$⊢ ((φ \land n \in ({ℕ_{0}}^{1_{𝑜}})) \land i \in \{k \in ({ℕ_{0}}^{1_{𝑜}}) \| k \leq_{f} n\}) \to n \in ({ℕ_{0}}^{1_{𝑜}})$
113		breq1	$⊢ k = i \to (k \leq_{f} n \leftrightarrow i \leq_{f} n)$
114		simpr	$⊢ ((φ \land n \in ({ℕ_{0}}^{1_{𝑜}})) \land i \in \{k \in ({ℕ_{0}}^{1_{𝑜}}) \| k \leq_{f} n\}) \to i \in \{k \in ({ℕ_{0}}^{1_{𝑜}}) \| k \leq_{f} n\}$
115	113 114	elrabrd	$⊢ ((φ \land n \in ({ℕ_{0}}^{1_{𝑜}})) \land i \in \{k \in ({ℕ_{0}}^{1_{𝑜}}) \| k \leq_{f} n\}) \to i \leq_{f} n$
116		elmapfn	$⊢ i \in ({ℕ_{0}}^{1_{𝑜}}) \to i Fn 1_{𝑜}$
117	116	adantl	$⊢ (n \in ({ℕ_{0}}^{1_{𝑜}}) \land i \in ({ℕ_{0}}^{1_{𝑜}})) \to i Fn 1_{𝑜}$
118		elmapfn	$⊢ n \in ({ℕ_{0}}^{1_{𝑜}}) \to n Fn 1_{𝑜}$
119	118	adantr	$⊢ (n \in ({ℕ_{0}}^{1_{𝑜}}) \land i \in ({ℕ_{0}}^{1_{𝑜}})) \to n Fn 1_{𝑜}$
120	50	a1i	$⊢ (n \in ({ℕ_{0}}^{1_{𝑜}}) \land i \in ({ℕ_{0}}^{1_{𝑜}})) \to 1_{𝑜} \in V$
121		inidm	$⊢ 1_{𝑜} \cap 1_{𝑜} = 1_{𝑜}$
122		eqidd	$⊢ ((n \in ({ℕ_{0}}^{1_{𝑜}}) \land i \in ({ℕ_{0}}^{1_{𝑜}})) \land \emptyset \in 1_{𝑜}) \to i (\emptyset) = i (\emptyset)$
123		eqidd	$⊢ ((n \in ({ℕ_{0}}^{1_{𝑜}}) \land i \in ({ℕ_{0}}^{1_{𝑜}})) \land \emptyset \in 1_{𝑜}) \to n (\emptyset) = n (\emptyset)$
124	117 119 120 120 121 122 123	ofrval	$⊢ ((n \in ({ℕ_{0}}^{1_{𝑜}}) \land i \in ({ℕ_{0}}^{1_{𝑜}})) \land i \leq_{f} n \land \emptyset \in 1_{𝑜}) \to i (\emptyset) \leq n (\emptyset)$
125	112 102 115 104 124	syl211anc	$⊢ ((φ \land n \in ({ℕ_{0}}^{1_{𝑜}})) \land i \in \{k \in ({ℕ_{0}}^{1_{𝑜}}) \| k \leq_{f} n\}) \to i (\emptyset) \leq n (\emptyset)$
126	125	ralrimivw	$⊢ ((φ \land n \in ({ℕ_{0}}^{1_{𝑜}})) \land i \in \{k \in ({ℕ_{0}}^{1_{𝑜}}) \| k \leq_{f} n\}) \to \forall x \in \{X\} i (\emptyset) \leq n (\emptyset)$
127	106	ffnd	$⊢ ((φ \land n \in ({ℕ_{0}}^{1_{𝑜}})) \land i \in \{k \in ({ℕ_{0}}^{1_{𝑜}}) \| k \leq_{f} n\}) \to \{⟨X, i (\emptyset)⟩\} Fn \{X\}$
128	57	adantr	$⊢ ((φ \land n \in ({ℕ_{0}}^{1_{𝑜}})) \land i \in \{k \in ({ℕ_{0}}^{1_{𝑜}}) \| k \leq_{f} n\}) \to \{⟨X, n (\emptyset)⟩\} : \{X\} ⟶ ℕ_{0}$
129	128	ffnd	$⊢ ((φ \land n \in ({ℕ_{0}}^{1_{𝑜}})) \land i \in \{k \in ({ℕ_{0}}^{1_{𝑜}}) \| k \leq_{f} n\}) \to \{⟨X, n (\emptyset)⟩\} Fn \{X\}$
130		inidm	$⊢ \{X\} \cap \{X\} = \{X\}$
131		simpr	$⊢ (((φ \land n \in ({ℕ_{0}}^{1_{𝑜}})) \land i \in \{k \in ({ℕ_{0}}^{1_{𝑜}}) \| k \leq_{f} n\}) \land x \in \{X\}) \to x \in \{X\}$
132	131	elsnd	$⊢ (((φ \land n \in ({ℕ_{0}}^{1_{𝑜}})) \land i \in \{k \in ({ℕ_{0}}^{1_{𝑜}}) \| k \leq_{f} n\}) \land x \in \{X\}) \to x = X$
133	132	fveq2d	$⊢ (((φ \land n \in ({ℕ_{0}}^{1_{𝑜}})) \land i \in \{k \in ({ℕ_{0}}^{1_{𝑜}}) \| k \leq_{f} n\}) \land x \in \{X\}) \to \{⟨X, i (\emptyset)⟩\} (x) = \{⟨X, i (\emptyset)⟩\} (X)$
134		fvsng	$⊢ (X \in V \land i (\emptyset) \in ℕ_{0}) \to \{⟨X, i (\emptyset)⟩\} (X) = i (\emptyset)$
135	98 105 134	syl2anc	$⊢ ((φ \land n \in ({ℕ_{0}}^{1_{𝑜}})) \land i \in \{k \in ({ℕ_{0}}^{1_{𝑜}}) \| k \leq_{f} n\}) \to \{⟨X, i (\emptyset)⟩\} (X) = i (\emptyset)$
136	135	adantr	$⊢ (((φ \land n \in ({ℕ_{0}}^{1_{𝑜}})) \land i \in \{k \in ({ℕ_{0}}^{1_{𝑜}}) \| k \leq_{f} n\}) \land x \in \{X\}) \to \{⟨X, i (\emptyset)⟩\} (X) = i (\emptyset)$
137	133 136	eqtrd	$⊢ (((φ \land n \in ({ℕ_{0}}^{1_{𝑜}})) \land i \in \{k \in ({ℕ_{0}}^{1_{𝑜}}) \| k \leq_{f} n\}) \land x \in \{X\}) \to \{⟨X, i (\emptyset)⟩\} (x) = i (\emptyset)$
138	132	fveq2d	$⊢ (((φ \land n \in ({ℕ_{0}}^{1_{𝑜}})) \land i \in \{k \in ({ℕ_{0}}^{1_{𝑜}}) \| k \leq_{f} n\}) \land x \in \{X\}) \to \{⟨X, n (\emptyset)⟩\} (x) = \{⟨X, n (\emptyset)⟩\} (X)$
139	56	adantr	$⊢ ((φ \land n \in ({ℕ_{0}}^{1_{𝑜}})) \land i \in \{k \in ({ℕ_{0}}^{1_{𝑜}}) \| k \leq_{f} n\}) \to n (\emptyset) \in ℕ_{0}$
140		fvsng	$⊢ (X \in V \land n (\emptyset) \in ℕ_{0}) \to \{⟨X, n (\emptyset)⟩\} (X) = n (\emptyset)$
141	98 139 140	syl2anc	$⊢ ((φ \land n \in ({ℕ_{0}}^{1_{𝑜}})) \land i \in \{k \in ({ℕ_{0}}^{1_{𝑜}}) \| k \leq_{f} n\}) \to \{⟨X, n (\emptyset)⟩\} (X) = n (\emptyset)$
142	141	adantr	$⊢ (((φ \land n \in ({ℕ_{0}}^{1_{𝑜}})) \land i \in \{k \in ({ℕ_{0}}^{1_{𝑜}}) \| k \leq_{f} n\}) \land x \in \{X\}) \to \{⟨X, n (\emptyset)⟩\} (X) = n (\emptyset)$
143	138 142	eqtrd	$⊢ (((φ \land n \in ({ℕ_{0}}^{1_{𝑜}})) \land i \in \{k \in ({ℕ_{0}}^{1_{𝑜}}) \| k \leq_{f} n\}) \land x \in \{X\}) \to \{⟨X, n (\emptyset)⟩\} (x) = n (\emptyset)$
144	127 129 97 97 130 137 143	ofrfval	$⊢ ((φ \land n \in ({ℕ_{0}}^{1_{𝑜}})) \land i \in \{k \in ({ℕ_{0}}^{1_{𝑜}}) \| k \leq_{f} n\}) \to (\{⟨X, i (\emptyset)⟩\} \leq_{f} \{⟨X, n (\emptyset)⟩\} \leftrightarrow \forall x \in \{X\} i (\emptyset) \leq n (\emptyset))$
145	126 144	mpbird	$⊢ ((φ \land n \in ({ℕ_{0}}^{1_{𝑜}})) \land i \in \{k \in ({ℕ_{0}}^{1_{𝑜}}) \| k \leq_{f} n\}) \to \{⟨X, i (\emptyset)⟩\} \leq_{f} \{⟨X, n (\emptyset)⟩\}$
146	94 111 145	elrabd	$⊢ ((φ \land n \in ({ℕ_{0}}^{1_{𝑜}})) \land i \in \{k \in ({ℕ_{0}}^{1_{𝑜}}) \| k \leq_{f} n\}) \to \{⟨X, i (\emptyset)⟩\} \in \{l \in \{g \in ({ℕ_{0}}^{\{X\}}) \| {finSupp}_{0} (g)\} \| l \leq_{f} \{⟨X, n (\emptyset)⟩\}\}$
147		breq1	$⊢ k = \{⟨\emptyset, j (X)⟩\} \to (k \leq_{f} n \leftrightarrow \{⟨\emptyset, j (X)⟩\} \leq_{f} n)$
148	50	a1i	$⊢ ((φ \land n \in ({ℕ_{0}}^{1_{𝑜}})) \land j \in \{l \in \{g \in ({ℕ_{0}}^{\{X\}}) \| {finSupp}_{0} (g)\} \| l \leq_{f} \{⟨X, n (\emptyset)⟩\}\}) \to 1_{𝑜} \in V$
149		df1o2	$⊢ 1_{𝑜} = \{\emptyset\}$
150	149	eqcomi	$⊢ \{\emptyset\} = 1_{𝑜}$
151	150	a1i	$⊢ ((φ \land n \in ({ℕ_{0}}^{1_{𝑜}})) \land j \in \{l \in \{g \in ({ℕ_{0}}^{\{X\}}) \| {finSupp}_{0} (g)\} \| l \leq_{f} \{⟨X, n (\emptyset)⟩\}\}) \to \{\emptyset\} = 1_{𝑜}$
152		0ex	$⊢ \emptyset \in V$
153	152	a1i	$⊢ ((φ \land n \in ({ℕ_{0}}^{1_{𝑜}})) \land j \in \{l \in \{g \in ({ℕ_{0}}^{\{X\}}) \| {finSupp}_{0} (g)\} \| l \leq_{f} \{⟨X, n (\emptyset)⟩\}\}) \to \emptyset \in V$
154		snidg	$⊢ X \in V \to X \in \{X\}$
155	7 154	syl	$⊢ φ \to X \in \{X\}$
156	155	ad2antrr	$⊢ ((φ \land n \in ({ℕ_{0}}^{1_{𝑜}})) \land j \in \{l \in \{g \in ({ℕ_{0}}^{\{X\}}) \| {finSupp}_{0} (g)\} \| l \leq_{f} \{⟨X, n (\emptyset)⟩\}\}) \to X \in \{X\}$
157	72 156	ffvelcdmd	$⊢ ((φ \land n \in ({ℕ_{0}}^{1_{𝑜}})) \land j \in \{l \in \{g \in ({ℕ_{0}}^{\{X\}}) \| {finSupp}_{0} (g)\} \| l \leq_{f} \{⟨X, n (\emptyset)⟩\}\}) \to j (X) \in ℕ_{0}$
158	153 157	fsnd	$⊢ ((φ \land n \in ({ℕ_{0}}^{1_{𝑜}})) \land j \in \{l \in \{g \in ({ℕ_{0}}^{\{X\}}) \| {finSupp}_{0} (g)\} \| l \leq_{f} \{⟨X, n (\emptyset)⟩\}\}) \to \{⟨\emptyset, j (X)⟩\} : \{\emptyset\} ⟶ ℕ_{0}$
159	151 158	feq2dd	$⊢ ((φ \land n \in ({ℕ_{0}}^{1_{𝑜}})) \land j \in \{l \in \{g \in ({ℕ_{0}}^{\{X\}}) \| {finSupp}_{0} (g)\} \| l \leq_{f} \{⟨X, n (\emptyset)⟩\}\}) \to \{⟨\emptyset, j (X)⟩\} : 1_{𝑜} ⟶ ℕ_{0}$
160	67 148 159	elmapdd	$⊢ ((φ \land n \in ({ℕ_{0}}^{1_{𝑜}})) \land j \in \{l \in \{g \in ({ℕ_{0}}^{\{X\}}) \| {finSupp}_{0} (g)\} \| l \leq_{f} \{⟨X, n (\emptyset)⟩\}\}) \to \{⟨\emptyset, j (X)⟩\} \in ({ℕ_{0}}^{1_{𝑜}})$
161		simplr	$⊢ ((φ \land n \in ({ℕ_{0}}^{1_{𝑜}})) \land j \in \{l \in \{g \in ({ℕ_{0}}^{\{X\}}) \| {finSupp}_{0} (g)\} \| l \leq_{f} \{⟨X, n (\emptyset)⟩\}\}) \to n \in ({ℕ_{0}}^{1_{𝑜}})$
162	49	adantr	$⊢ ((φ \land n \in ({ℕ_{0}}^{1_{𝑜}})) \land j \in \{l \in \{g \in ({ℕ_{0}}^{\{X\}}) \| {finSupp}_{0} (g)\} \| l \leq_{f} \{⟨X, n (\emptyset)⟩\}\}) \to X \in V$
163	161 162	jca	$⊢ ((φ \land n \in ({ℕ_{0}}^{1_{𝑜}})) \land j \in \{l \in \{g \in ({ℕ_{0}}^{\{X\}}) \| {finSupp}_{0} (g)\} \| l \leq_{f} \{⟨X, n (\emptyset)⟩\}\}) \to (n \in ({ℕ_{0}}^{1_{𝑜}}) \land X \in V)$
164		elmapfn	$⊢ j \in ({ℕ_{0}}^{\{X\}}) \to j Fn \{X\}$
165	164	adantr	$⊢ (j \in ({ℕ_{0}}^{\{X\}}) \land (n \in ({ℕ_{0}}^{1_{𝑜}}) \land X \in V)) \to j Fn \{X\}$
166		simpr	$⊢ (n \in ({ℕ_{0}}^{1_{𝑜}}) \land X \in V) \to X \in V$
167		elmapi	$⊢ n \in ({ℕ_{0}}^{1_{𝑜}}) \to n : 1_{𝑜} ⟶ ℕ_{0}$
168	54	a1i	$⊢ n \in ({ℕ_{0}}^{1_{𝑜}}) \to \emptyset \in 1_{𝑜}$
169	167 168	ffvelcdmd	$⊢ n \in ({ℕ_{0}}^{1_{𝑜}}) \to n (\emptyset) \in ℕ_{0}$
170	169	adantr	$⊢ (n \in ({ℕ_{0}}^{1_{𝑜}}) \land X \in V) \to n (\emptyset) \in ℕ_{0}$
171	166 170	fsnd	$⊢ (n \in ({ℕ_{0}}^{1_{𝑜}}) \land X \in V) \to \{⟨X, n (\emptyset)⟩\} : \{X\} ⟶ ℕ_{0}$
172	171	ffnd	$⊢ (n \in ({ℕ_{0}}^{1_{𝑜}}) \land X \in V) \to \{⟨X, n (\emptyset)⟩\} Fn \{X\}$
173	172	adantl	$⊢ (j \in ({ℕ_{0}}^{\{X\}}) \land (n \in ({ℕ_{0}}^{1_{𝑜}}) \land X \in V)) \to \{⟨X, n (\emptyset)⟩\} Fn \{X\}$
174	47	a1i	$⊢ (j \in ({ℕ_{0}}^{\{X\}}) \land (n \in ({ℕ_{0}}^{1_{𝑜}}) \land X \in V)) \to \{X\} \in V$
175		eqidd	$⊢ ((j \in ({ℕ_{0}}^{\{X\}}) \land (n \in ({ℕ_{0}}^{1_{𝑜}}) \land X \in V)) \land X \in \{X\}) \to j (X) = j (X)$
176	166 170 140	syl2anc	$⊢ (n \in ({ℕ_{0}}^{1_{𝑜}}) \land X \in V) \to \{⟨X, n (\emptyset)⟩\} (X) = n (\emptyset)$
177	176	ad2antlr	$⊢ ((j \in ({ℕ_{0}}^{\{X\}}) \land (n \in ({ℕ_{0}}^{1_{𝑜}}) \land X \in V)) \land X \in \{X\}) \to \{⟨X, n (\emptyset)⟩\} (X) = n (\emptyset)$
178	165 173 174 174 130 175 177	ofrval	$⊢ ((j \in ({ℕ_{0}}^{\{X\}}) \land (n \in ({ℕ_{0}}^{1_{𝑜}}) \land X \in V)) \land j \leq_{f} \{⟨X, n (\emptyset)⟩\} \land X \in \{X\}) \to j (X) \leq n (\emptyset)$
179	71 163 75 156 178	syl211anc	$⊢ ((φ \land n \in ({ℕ_{0}}^{1_{𝑜}})) \land j \in \{l \in \{g \in ({ℕ_{0}}^{\{X\}}) \| {finSupp}_{0} (g)\} \| l \leq_{f} \{⟨X, n (\emptyset)⟩\}\}) \to j (X) \leq n (\emptyset)$
180		fveq2	$⊢ o = \emptyset \to n (o) = n (\emptyset)$
181	180	breq2d	$⊢ o = \emptyset \to (j (X) \leq n (o) \leftrightarrow j (X) \leq n (\emptyset))$
182	152 181	ralsn	$⊢ \forall o \in \{\emptyset\} j (X) \leq n (o) \leftrightarrow j (X) \leq n (\emptyset)$
183	179 182	sylibr	$⊢ ((φ \land n \in ({ℕ_{0}}^{1_{𝑜}})) \land j \in \{l \in \{g \in ({ℕ_{0}}^{\{X\}}) \| {finSupp}_{0} (g)\} \| l \leq_{f} \{⟨X, n (\emptyset)⟩\}\}) \to \forall o \in \{\emptyset\} j (X) \leq n (o)$
184	149	a1i	$⊢ ((φ \land n \in ({ℕ_{0}}^{1_{𝑜}})) \land j \in \{l \in \{g \in ({ℕ_{0}}^{\{X\}}) \| {finSupp}_{0} (g)\} \| l \leq_{f} \{⟨X, n (\emptyset)⟩\}\}) \to 1_{𝑜} = \{\emptyset\}$
185	183 184	raleqtrrdv	$⊢ ((φ \land n \in ({ℕ_{0}}^{1_{𝑜}})) \land j \in \{l \in \{g \in ({ℕ_{0}}^{\{X\}}) \| {finSupp}_{0} (g)\} \| l \leq_{f} \{⟨X, n (\emptyset)⟩\}\}) \to \forall o \in 1_{𝑜} j (X) \leq n (o)$
186	159	ffnd	$⊢ ((φ \land n \in ({ℕ_{0}}^{1_{𝑜}})) \land j \in \{l \in \{g \in ({ℕ_{0}}^{\{X\}}) \| {finSupp}_{0} (g)\} \| l \leq_{f} \{⟨X, n (\emptyset)⟩\}\}) \to \{⟨\emptyset, j (X)⟩\} Fn 1_{𝑜}$
187	118	ad2antlr	$⊢ ((φ \land n \in ({ℕ_{0}}^{1_{𝑜}})) \land j \in \{l \in \{g \in ({ℕ_{0}}^{\{X\}}) \| {finSupp}_{0} (g)\} \| l \leq_{f} \{⟨X, n (\emptyset)⟩\}\}) \to n Fn 1_{𝑜}$
188		elsni	$⊢ o \in \{\emptyset\} \to o = \emptyset$
189	188 149	eleq2s	$⊢ o \in 1_{𝑜} \to o = \emptyset$
190	189	adantl	$⊢ (((φ \land n \in ({ℕ_{0}}^{1_{𝑜}})) \land j \in \{l \in \{g \in ({ℕ_{0}}^{\{X\}}) \| {finSupp}_{0} (g)\} \| l \leq_{f} \{⟨X, n (\emptyset)⟩\}\}) \land o \in 1_{𝑜}) \to o = \emptyset$
191	190	fveq2d	$⊢ (((φ \land n \in ({ℕ_{0}}^{1_{𝑜}})) \land j \in \{l \in \{g \in ({ℕ_{0}}^{\{X\}}) \| {finSupp}_{0} (g)\} \| l \leq_{f} \{⟨X, n (\emptyset)⟩\}\}) \land o \in 1_{𝑜}) \to \{⟨\emptyset, j (X)⟩\} (o) = \{⟨\emptyset, j (X)⟩\} (\emptyset)$
192	157	adantr	$⊢ (((φ \land n \in ({ℕ_{0}}^{1_{𝑜}})) \land j \in \{l \in \{g \in ({ℕ_{0}}^{\{X\}}) \| {finSupp}_{0} (g)\} \| l \leq_{f} \{⟨X, n (\emptyset)⟩\}\}) \land o \in 1_{𝑜}) \to j (X) \in ℕ_{0}$
193		fvsng	$⊢ (\emptyset \in V \land j (X) \in ℕ_{0}) \to \{⟨\emptyset, j (X)⟩\} (\emptyset) = j (X)$
194	152 192 193	sylancr	$⊢ (((φ \land n \in ({ℕ_{0}}^{1_{𝑜}})) \land j \in \{l \in \{g \in ({ℕ_{0}}^{\{X\}}) \| {finSupp}_{0} (g)\} \| l \leq_{f} \{⟨X, n (\emptyset)⟩\}\}) \land o \in 1_{𝑜}) \to \{⟨\emptyset, j (X)⟩\} (\emptyset) = j (X)$
195	191 194	eqtrd	$⊢ (((φ \land n \in ({ℕ_{0}}^{1_{𝑜}})) \land j \in \{l \in \{g \in ({ℕ_{0}}^{\{X\}}) \| {finSupp}_{0} (g)\} \| l \leq_{f} \{⟨X, n (\emptyset)⟩\}\}) \land o \in 1_{𝑜}) \to \{⟨\emptyset, j (X)⟩\} (o) = j (X)$
196		eqidd	$⊢ (((φ \land n \in ({ℕ_{0}}^{1_{𝑜}})) \land j \in \{l \in \{g \in ({ℕ_{0}}^{\{X\}}) \| {finSupp}_{0} (g)\} \| l \leq_{f} \{⟨X, n (\emptyset)⟩\}\}) \land o \in 1_{𝑜}) \to n (o) = n (o)$
197	186 187 148 148 121 195 196	ofrfval	$⊢ ((φ \land n \in ({ℕ_{0}}^{1_{𝑜}})) \land j \in \{l \in \{g \in ({ℕ_{0}}^{\{X\}}) \| {finSupp}_{0} (g)\} \| l \leq_{f} \{⟨X, n (\emptyset)⟩\}\}) \to (\{⟨\emptyset, j (X)⟩\} \leq_{f} n \leftrightarrow \forall o \in 1_{𝑜} j (X) \leq n (o))$
198	185 197	mpbird	$⊢ ((φ \land n \in ({ℕ_{0}}^{1_{𝑜}})) \land j \in \{l \in \{g \in ({ℕ_{0}}^{\{X\}}) \| {finSupp}_{0} (g)\} \| l \leq_{f} \{⟨X, n (\emptyset)⟩\}\}) \to \{⟨\emptyset, j (X)⟩\} \leq_{f} n$
199	147 160 198	elrabd	$⊢ ((φ \land n \in ({ℕ_{0}}^{1_{𝑜}})) \land j \in \{l \in \{g \in ({ℕ_{0}}^{\{X\}}) \| {finSupp}_{0} (g)\} \| l \leq_{f} \{⟨X, n (\emptyset)⟩\}\}) \to \{⟨\emptyset, j (X)⟩\} \in \{k \in ({ℕ_{0}}^{1_{𝑜}}) \| k \leq_{f} n\}$
200		eqcom	$⊢ j (X) = i (\emptyset) \leftrightarrow i (\emptyset) = j (X)$
201	200	a1i	$⊢ (((φ \land n \in ({ℕ_{0}}^{1_{𝑜}})) \land j \in \{l \in \{g \in ({ℕ_{0}}^{\{X\}}) \| {finSupp}_{0} (g)\} \| l \leq_{f} \{⟨X, n (\emptyset)⟩\}\}) \land i \in \{k \in ({ℕ_{0}}^{1_{𝑜}}) \| k \leq_{f} n\}) \to (j (X) = i (\emptyset) \leftrightarrow i (\emptyset) = j (X))$
202	135	adantlr	$⊢ (((φ \land n \in ({ℕ_{0}}^{1_{𝑜}})) \land j \in \{l \in \{g \in ({ℕ_{0}}^{\{X\}}) \| {finSupp}_{0} (g)\} \| l \leq_{f} \{⟨X, n (\emptyset)⟩\}\}) \land i \in \{k \in ({ℕ_{0}}^{1_{𝑜}}) \| k \leq_{f} n\}) \to \{⟨X, i (\emptyset)⟩\} (X) = i (\emptyset)$
203	202	eqeq2d	$⊢ (((φ \land n \in ({ℕ_{0}}^{1_{𝑜}})) \land j \in \{l \in \{g \in ({ℕ_{0}}^{\{X\}}) \| {finSupp}_{0} (g)\} \| l \leq_{f} \{⟨X, n (\emptyset)⟩\}\}) \land i \in \{k \in ({ℕ_{0}}^{1_{𝑜}}) \| k \leq_{f} n\}) \to (j (X) = \{⟨X, i (\emptyset)⟩\} (X) \leftrightarrow j (X) = i (\emptyset))$
204	157	adantr	$⊢ (((φ \land n \in ({ℕ_{0}}^{1_{𝑜}})) \land j \in \{l \in \{g \in ({ℕ_{0}}^{\{X\}}) \| {finSupp}_{0} (g)\} \| l \leq_{f} \{⟨X, n (\emptyset)⟩\}\}) \land i \in \{k \in ({ℕ_{0}}^{1_{𝑜}}) \| k \leq_{f} n\}) \to j (X) \in ℕ_{0}$
205	152 204 193	sylancr	$⊢ (((φ \land n \in ({ℕ_{0}}^{1_{𝑜}})) \land j \in \{l \in \{g \in ({ℕ_{0}}^{\{X\}}) \| {finSupp}_{0} (g)\} \| l \leq_{f} \{⟨X, n (\emptyset)⟩\}\}) \land i \in \{k \in ({ℕ_{0}}^{1_{𝑜}}) \| k \leq_{f} n\}) \to \{⟨\emptyset, j (X)⟩\} (\emptyset) = j (X)$
206	205	eqeq2d	$⊢ (((φ \land n \in ({ℕ_{0}}^{1_{𝑜}})) \land j \in \{l \in \{g \in ({ℕ_{0}}^{\{X\}}) \| {finSupp}_{0} (g)\} \| l \leq_{f} \{⟨X, n (\emptyset)⟩\}\}) \land i \in \{k \in ({ℕ_{0}}^{1_{𝑜}}) \| k \leq_{f} n\}) \to (i (\emptyset) = \{⟨\emptyset, j (X)⟩\} (\emptyset) \leftrightarrow i (\emptyset) = j (X))$
207	201 203 206	3bitr4d	$⊢ (((φ \land n \in ({ℕ_{0}}^{1_{𝑜}})) \land j \in \{l \in \{g \in ({ℕ_{0}}^{\{X\}}) \| {finSupp}_{0} (g)\} \| l \leq_{f} \{⟨X, n (\emptyset)⟩\}\}) \land i \in \{k \in ({ℕ_{0}}^{1_{𝑜}}) \| k \leq_{f} n\}) \to (j (X) = \{⟨X, i (\emptyset)⟩\} (X) \leftrightarrow i (\emptyset) = \{⟨\emptyset, j (X)⟩\} (\emptyset))$
208	162	adantr	$⊢ (((φ \land n \in ({ℕ_{0}}^{1_{𝑜}})) \land j \in \{l \in \{g \in ({ℕ_{0}}^{\{X\}}) \| {finSupp}_{0} (g)\} \| l \leq_{f} \{⟨X, n (\emptyset)⟩\}\}) \land i \in \{k \in ({ℕ_{0}}^{1_{𝑜}}) \| k \leq_{f} n\}) \to X \in V$
209		eqid	$⊢ \{X\} = \{X\}$
210	72	adantr	$⊢ (((φ \land n \in ({ℕ_{0}}^{1_{𝑜}})) \land j \in \{l \in \{g \in ({ℕ_{0}}^{\{X\}}) \| {finSupp}_{0} (g)\} \| l \leq_{f} \{⟨X, n (\emptyset)⟩\}\}) \land i \in \{k \in ({ℕ_{0}}^{1_{𝑜}}) \| k \leq_{f} n\}) \to j : \{X\} ⟶ ℕ_{0}$
211	210	ffnd	$⊢ (((φ \land n \in ({ℕ_{0}}^{1_{𝑜}})) \land j \in \{l \in \{g \in ({ℕ_{0}}^{\{X\}}) \| {finSupp}_{0} (g)\} \| l \leq_{f} \{⟨X, n (\emptyset)⟩\}\}) \land i \in \{k \in ({ℕ_{0}}^{1_{𝑜}}) \| k \leq_{f} n\}) \to j Fn \{X\}$
212	127	adantlr	$⊢ (((φ \land n \in ({ℕ_{0}}^{1_{𝑜}})) \land j \in \{l \in \{g \in ({ℕ_{0}}^{\{X\}}) \| {finSupp}_{0} (g)\} \| l \leq_{f} \{⟨X, n (\emptyset)⟩\}\}) \land i \in \{k \in ({ℕ_{0}}^{1_{𝑜}}) \| k \leq_{f} n\}) \to \{⟨X, i (\emptyset)⟩\} Fn \{X\}$
213	208 209 211 212	fsneq	$⊢ (((φ \land n \in ({ℕ_{0}}^{1_{𝑜}})) \land j \in \{l \in \{g \in ({ℕ_{0}}^{\{X\}}) \| {finSupp}_{0} (g)\} \| l \leq_{f} \{⟨X, n (\emptyset)⟩\}\}) \land i \in \{k \in ({ℕ_{0}}^{1_{𝑜}}) \| k \leq_{f} n\}) \to (j = \{⟨X, i (\emptyset)⟩\} \leftrightarrow j (X) = \{⟨X, i (\emptyset)⟩\} (X))$
214	152	a1i	$⊢ (((φ \land n \in ({ℕ_{0}}^{1_{𝑜}})) \land j \in \{l \in \{g \in ({ℕ_{0}}^{\{X\}}) \| {finSupp}_{0} (g)\} \| l \leq_{f} \{⟨X, n (\emptyset)⟩\}\}) \land i \in \{k \in ({ℕ_{0}}^{1_{𝑜}}) \| k \leq_{f} n\}) \to \emptyset \in V$
215	103	adantlr	$⊢ (((φ \land n \in ({ℕ_{0}}^{1_{𝑜}})) \land j \in \{l \in \{g \in ({ℕ_{0}}^{\{X\}}) \| {finSupp}_{0} (g)\} \| l \leq_{f} \{⟨X, n (\emptyset)⟩\}\}) \land i \in \{k \in ({ℕ_{0}}^{1_{𝑜}}) \| k \leq_{f} n\}) \to i : 1_{𝑜} ⟶ ℕ_{0}$
216	215	ffnd	$⊢ (((φ \land n \in ({ℕ_{0}}^{1_{𝑜}})) \land j \in \{l \in \{g \in ({ℕ_{0}}^{\{X\}}) \| {finSupp}_{0} (g)\} \| l \leq_{f} \{⟨X, n (\emptyset)⟩\}\}) \land i \in \{k \in ({ℕ_{0}}^{1_{𝑜}}) \| k \leq_{f} n\}) \to i Fn 1_{𝑜}$
217	186	adantr	$⊢ (((φ \land n \in ({ℕ_{0}}^{1_{𝑜}})) \land j \in \{l \in \{g \in ({ℕ_{0}}^{\{X\}}) \| {finSupp}_{0} (g)\} \| l \leq_{f} \{⟨X, n (\emptyset)⟩\}\}) \land i \in \{k \in ({ℕ_{0}}^{1_{𝑜}}) \| k \leq_{f} n\}) \to \{⟨\emptyset, j (X)⟩\} Fn 1_{𝑜}$
218	214 149 216 217	fsneq	$⊢ (((φ \land n \in ({ℕ_{0}}^{1_{𝑜}})) \land j \in \{l \in \{g \in ({ℕ_{0}}^{\{X\}}) \| {finSupp}_{0} (g)\} \| l \leq_{f} \{⟨X, n (\emptyset)⟩\}\}) \land i \in \{k \in ({ℕ_{0}}^{1_{𝑜}}) \| k \leq_{f} n\}) \to (i = \{⟨\emptyset, j (X)⟩\} \leftrightarrow i (\emptyset) = \{⟨\emptyset, j (X)⟩\} (\emptyset))$
219	207 213 218	3bitr4d	$⊢ (((φ \land n \in ({ℕ_{0}}^{1_{𝑜}})) \land j \in \{l \in \{g \in ({ℕ_{0}}^{\{X\}}) \| {finSupp}_{0} (g)\} \| l \leq_{f} \{⟨X, n (\emptyset)⟩\}\}) \land i \in \{k \in ({ℕ_{0}}^{1_{𝑜}}) \| k \leq_{f} n\}) \to (j = \{⟨X, i (\emptyset)⟩\} \leftrightarrow i = \{⟨\emptyset, j (X)⟩\})$
220	199 219	reu6dv	$⊢ ((φ \land n \in ({ℕ_{0}}^{1_{𝑜}})) \land j \in \{l \in \{g \in ({ℕ_{0}}^{\{X\}}) \| {finSupp}_{0} (g)\} \| l \leq_{f} \{⟨X, n (\emptyset)⟩\}\}) \to \exists! i \in \{k \in ({ℕ_{0}}^{1_{𝑜}}) \| k \leq_{f} n\} j = \{⟨X, i (\emptyset)⟩\}$
221	24 25 26 30 32 37 87 88 93 146 220	gsummptfsf1o	$⊢ (φ \land n \in ({ℕ_{0}}^{1_{𝑜}})) \to \underset{j \in \{l \in \{g \in ({ℕ_{0}}^{\{X\}}) \| {finSupp}_{0} (g)\} \| l \leq_{f} \{⟨X, n (\emptyset)⟩\}\}}{\sum_{R}} (F (j) \cdot_{R} G (\{⟨X, n (\emptyset)⟩\} -_{f} j)) = \underset{i \in \{k \in ({ℕ_{0}}^{1_{𝑜}}) \| k \leq_{f} n\}}{\sum_{R}} (F (\{⟨X, i (\emptyset)⟩\}) \cdot_{R} G (\{⟨X, n (\emptyset)⟩\} -_{f} \{⟨X, i (\emptyset)⟩\}))$
222	100	a1i	$⊢ φ \to \{k \in ({ℕ_{0}}^{1_{𝑜}}) \| k \leq_{f} n\} \subseteq {ℕ_{0}}^{1_{𝑜}}$
223	222	sselda	$⊢ (φ \land i \in \{k \in ({ℕ_{0}}^{1_{𝑜}}) \| k \leq_{f} n\}) \to i \in ({ℕ_{0}}^{1_{𝑜}})$
224		fveq1	$⊢ n = i \to n (\emptyset) = i (\emptyset)$
225	224	opeq2d	$⊢ n = i \to ⟨X, n (\emptyset)⟩ = ⟨X, i (\emptyset)⟩$
226	225	sneqd	$⊢ n = i \to \{⟨X, n (\emptyset)⟩\} = \{⟨X, i (\emptyset)⟩\}$
227	226	fveq2d	$⊢ n = i \to F (\{⟨X, n (\emptyset)⟩\}) = F (\{⟨X, i (\emptyset)⟩\})$
228		fveq1	$⊢ f = F \to f (\{⟨X, n (\emptyset)⟩\}) = F (\{⟨X, n (\emptyset)⟩\})$
229	228	mpteq2dv	$⊢ f = F \to (n \in ({ℕ_{0}}^{1_{𝑜}}) ⟼ f (\{⟨X, n (\emptyset)⟩\})) = (n \in ({ℕ_{0}}^{1_{𝑜}}) ⟼ F (\{⟨X, n (\emptyset)⟩\}))$
230		ovexd	$⊢ φ \to {ℕ_{0}}^{1_{𝑜}} \in V$
231	230	mptexd	$⊢ φ \to (n \in ({ℕ_{0}}^{1_{𝑜}}) ⟼ F (\{⟨X, n (\emptyset)⟩\})) \in V$
232	6 229 9 231	fvmptd3	$⊢ φ \to M (F) = (n \in ({ℕ_{0}}^{1_{𝑜}}) ⟼ F (\{⟨X, n (\emptyset)⟩\}))$
233	232	adantr	$⊢ (φ \land i \in ({ℕ_{0}}^{1_{𝑜}})) \to M (F) = (n \in ({ℕ_{0}}^{1_{𝑜}}) ⟼ F (\{⟨X, n (\emptyset)⟩\}))$
234		simpr	$⊢ (φ \land i \in ({ℕ_{0}}^{1_{𝑜}})) \to i \in ({ℕ_{0}}^{1_{𝑜}})$
235		fvexd	$⊢ (φ \land i \in ({ℕ_{0}}^{1_{𝑜}})) \to F (\{⟨X, i (\emptyset)⟩\}) \in V$
236	227 233 234 235	fvmptd4	$⊢ (φ \land i \in ({ℕ_{0}}^{1_{𝑜}})) \to M (F) (i) = F (\{⟨X, i (\emptyset)⟩\})$
237	223 236	syldan	$⊢ (φ \land i \in \{k \in ({ℕ_{0}}^{1_{𝑜}}) \| k \leq_{f} n\}) \to M (F) (i) = F (\{⟨X, i (\emptyset)⟩\})$
238	237	adantlr	$⊢ ((φ \land n \in ({ℕ_{0}}^{1_{𝑜}})) \land i \in \{k \in ({ℕ_{0}}^{1_{𝑜}}) \| k \leq_{f} n\}) \to M (F) (i) = F (\{⟨X, i (\emptyset)⟩\})$
239		fveq1	$⊢ f = G \to f (\{⟨X, n (\emptyset)⟩\}) = G (\{⟨X, n (\emptyset)⟩\})$
240	239	mpteq2dv	$⊢ f = G \to (n \in ({ℕ_{0}}^{1_{𝑜}}) ⟼ f (\{⟨X, n (\emptyset)⟩\})) = (n \in ({ℕ_{0}}^{1_{𝑜}}) ⟼ G (\{⟨X, n (\emptyset)⟩\}))$
241	230	mptexd	$⊢ φ \to (n \in ({ℕ_{0}}^{1_{𝑜}}) ⟼ G (\{⟨X, n (\emptyset)⟩\})) \in V$
242	6 240 10 241	fvmptd3	$⊢ φ \to M (G) = (n \in ({ℕ_{0}}^{1_{𝑜}}) ⟼ G (\{⟨X, n (\emptyset)⟩\}))$
243		fveq1	$⊢ n = m \to n (\emptyset) = m (\emptyset)$
244	243	opeq2d	$⊢ n = m \to ⟨X, n (\emptyset)⟩ = ⟨X, m (\emptyset)⟩$
245	244	sneqd	$⊢ n = m \to \{⟨X, n (\emptyset)⟩\} = \{⟨X, m (\emptyset)⟩\}$
246	245	fveq2d	$⊢ n = m \to G (\{⟨X, n (\emptyset)⟩\}) = G (\{⟨X, m (\emptyset)⟩\})$
247	246	cbvmptv	$⊢ (n \in ({ℕ_{0}}^{1_{𝑜}}) ⟼ G (\{⟨X, n (\emptyset)⟩\})) = (m \in ({ℕ_{0}}^{1_{𝑜}}) ⟼ G (\{⟨X, m (\emptyset)⟩\}))$
248	242 247	eqtrdi	$⊢ φ \to M (G) = (m \in ({ℕ_{0}}^{1_{𝑜}}) ⟼ G (\{⟨X, m (\emptyset)⟩\}))$
249	248	ad2antrr	$⊢ ((φ \land n \in ({ℕ_{0}}^{1_{𝑜}})) \land i \in \{k \in ({ℕ_{0}}^{1_{𝑜}}) \| k \leq_{f} n\}) \to M (G) = (m \in ({ℕ_{0}}^{1_{𝑜}}) ⟼ G (\{⟨X, m (\emptyset)⟩\}))$
250		simpr	$⊢ (((φ \land n \in ({ℕ_{0}}^{1_{𝑜}})) \land i \in \{k \in ({ℕ_{0}}^{1_{𝑜}}) \| k \leq_{f} n\}) \land m = n -_{f} i) \to m = n -_{f} i$
251	250	fveq1d	$⊢ (((φ \land n \in ({ℕ_{0}}^{1_{𝑜}})) \land i \in \{k \in ({ℕ_{0}}^{1_{𝑜}}) \| k \leq_{f} n\}) \land m = n -_{f} i) \to m (\emptyset) = (n -_{f} i) (\emptyset)$
252	54	a1i	$⊢ (((φ \land n \in ({ℕ_{0}}^{1_{𝑜}})) \land i \in \{k \in ({ℕ_{0}}^{1_{𝑜}}) \| k \leq_{f} n\}) \land m = n -_{f} i) \to \emptyset \in 1_{𝑜}$
253	118	adantl	$⊢ (φ \land n \in ({ℕ_{0}}^{1_{𝑜}})) \to n Fn 1_{𝑜}$
254	253	ad2antrr	$⊢ (((φ \land n \in ({ℕ_{0}}^{1_{𝑜}})) \land i \in \{k \in ({ℕ_{0}}^{1_{𝑜}}) \| k \leq_{f} n\}) \land m = n -_{f} i) \to n Fn 1_{𝑜}$
255	102 116	syl	$⊢ ((φ \land n \in ({ℕ_{0}}^{1_{𝑜}})) \land i \in \{k \in ({ℕ_{0}}^{1_{𝑜}}) \| k \leq_{f} n\}) \to i Fn 1_{𝑜}$
256	255	adantr	$⊢ (((φ \land n \in ({ℕ_{0}}^{1_{𝑜}})) \land i \in \{k \in ({ℕ_{0}}^{1_{𝑜}}) \| k \leq_{f} n\}) \land m = n -_{f} i) \to i Fn 1_{𝑜}$
257	50	a1i	$⊢ (((φ \land n \in ({ℕ_{0}}^{1_{𝑜}})) \land i \in \{k \in ({ℕ_{0}}^{1_{𝑜}}) \| k \leq_{f} n\}) \land m = n -_{f} i) \to 1_{𝑜} \in V$
258		eqidd	$⊢ ((((φ \land n \in ({ℕ_{0}}^{1_{𝑜}})) \land i \in \{k \in ({ℕ_{0}}^{1_{𝑜}}) \| k \leq_{f} n\}) \land m = n -_{f} i) \land \emptyset \in 1_{𝑜}) \to n (\emptyset) = n (\emptyset)$
259		eqidd	$⊢ ((((φ \land n \in ({ℕ_{0}}^{1_{𝑜}})) \land i \in \{k \in ({ℕ_{0}}^{1_{𝑜}}) \| k \leq_{f} n\}) \land m = n -_{f} i) \land \emptyset \in 1_{𝑜}) \to i (\emptyset) = i (\emptyset)$
260	254 256 257 257 121 258 259	ofval	$⊢ ((((φ \land n \in ({ℕ_{0}}^{1_{𝑜}})) \land i \in \{k \in ({ℕ_{0}}^{1_{𝑜}}) \| k \leq_{f} n\}) \land m = n -_{f} i) \land \emptyset \in 1_{𝑜}) \to (n -_{f} i) (\emptyset) = n (\emptyset) - i (\emptyset)$
261	252 260	mpdan	$⊢ (((φ \land n \in ({ℕ_{0}}^{1_{𝑜}})) \land i \in \{k \in ({ℕ_{0}}^{1_{𝑜}}) \| k \leq_{f} n\}) \land m = n -_{f} i) \to (n -_{f} i) (\emptyset) = n (\emptyset) - i (\emptyset)$
262	251 261	eqtrd	$⊢ (((φ \land n \in ({ℕ_{0}}^{1_{𝑜}})) \land i \in \{k \in ({ℕ_{0}}^{1_{𝑜}}) \| k \leq_{f} n\}) \land m = n -_{f} i) \to m (\emptyset) = n (\emptyset) - i (\emptyset)$
263	98	adantr	$⊢ (((φ \land n \in ({ℕ_{0}}^{1_{𝑜}})) \land i \in \{k \in ({ℕ_{0}}^{1_{𝑜}}) \| k \leq_{f} n\}) \land m = n -_{f} i) \to X \in V$
264		fvexd	$⊢ (((φ \land n \in ({ℕ_{0}}^{1_{𝑜}})) \land i \in \{k \in ({ℕ_{0}}^{1_{𝑜}}) \| k \leq_{f} n\}) \land m = n -_{f} i) \to m (\emptyset) \in V$
265		fvsng	$⊢ (X \in V \land m (\emptyset) \in V) \to \{⟨X, m (\emptyset)⟩\} (X) = m (\emptyset)$
266	263 264 265	syl2anc	$⊢ (((φ \land n \in ({ℕ_{0}}^{1_{𝑜}})) \land i \in \{k \in ({ℕ_{0}}^{1_{𝑜}}) \| k \leq_{f} n\}) \land m = n -_{f} i) \to \{⟨X, m (\emptyset)⟩\} (X) = m (\emptyset)$
267	263 154	syl	$⊢ (((φ \land n \in ({ℕ_{0}}^{1_{𝑜}})) \land i \in \{k \in ({ℕ_{0}}^{1_{𝑜}}) \| k \leq_{f} n\}) \land m = n -_{f} i) \to X \in \{X\}$
268	129	adantr	$⊢ (((φ \land n \in ({ℕ_{0}}^{1_{𝑜}})) \land i \in \{k \in ({ℕ_{0}}^{1_{𝑜}}) \| k \leq_{f} n\}) \land m = n -_{f} i) \to \{⟨X, n (\emptyset)⟩\} Fn \{X\}$
269	127	adantr	$⊢ (((φ \land n \in ({ℕ_{0}}^{1_{𝑜}})) \land i \in \{k \in ({ℕ_{0}}^{1_{𝑜}}) \| k \leq_{f} n\}) \land m = n -_{f} i) \to \{⟨X, i (\emptyset)⟩\} Fn \{X\}$
270	47	a1i	$⊢ (((φ \land n \in ({ℕ_{0}}^{1_{𝑜}})) \land i \in \{k \in ({ℕ_{0}}^{1_{𝑜}}) \| k \leq_{f} n\}) \land m = n -_{f} i) \to \{X\} \in V$
271	141	ad2antrr	$⊢ ((((φ \land n \in ({ℕ_{0}}^{1_{𝑜}})) \land i \in \{k \in ({ℕ_{0}}^{1_{𝑜}}) \| k \leq_{f} n\}) \land m = n -_{f} i) \land X \in \{X\}) \to \{⟨X, n (\emptyset)⟩\} (X) = n (\emptyset)$
272	135	ad2antrr	$⊢ ((((φ \land n \in ({ℕ_{0}}^{1_{𝑜}})) \land i \in \{k \in ({ℕ_{0}}^{1_{𝑜}}) \| k \leq_{f} n\}) \land m = n -_{f} i) \land X \in \{X\}) \to \{⟨X, i (\emptyset)⟩\} (X) = i (\emptyset)$
273	268 269 270 270 130 271 272	ofval	$⊢ ((((φ \land n \in ({ℕ_{0}}^{1_{𝑜}})) \land i \in \{k \in ({ℕ_{0}}^{1_{𝑜}}) \| k \leq_{f} n\}) \land m = n -_{f} i) \land X \in \{X\}) \to (\{⟨X, n (\emptyset)⟩\} -_{f} \{⟨X, i (\emptyset)⟩\}) (X) = n (\emptyset) - i (\emptyset)$
274	267 273	mpdan	$⊢ (((φ \land n \in ({ℕ_{0}}^{1_{𝑜}})) \land i \in \{k \in ({ℕ_{0}}^{1_{𝑜}}) \| k \leq_{f} n\}) \land m = n -_{f} i) \to (\{⟨X, n (\emptyset)⟩\} -_{f} \{⟨X, i (\emptyset)⟩\}) (X) = n (\emptyset) - i (\emptyset)$
275	262 266 274	3eqtr4d	$⊢ (((φ \land n \in ({ℕ_{0}}^{1_{𝑜}})) \land i \in \{k \in ({ℕ_{0}}^{1_{𝑜}}) \| k \leq_{f} n\}) \land m = n -_{f} i) \to \{⟨X, m (\emptyset)⟩\} (X) = (\{⟨X, n (\emptyset)⟩\} -_{f} \{⟨X, i (\emptyset)⟩\}) (X)$
276		elsni	$⊢ x \in \{n (\emptyset)\} \to x = n (\emptyset)$
277	276	adantr	$⊢ (x \in \{n (\emptyset)\} \land y \in (0 \dots n (\emptyset))) \to x = n (\emptyset)$
278	277	oveq1d	$⊢ (x \in \{n (\emptyset)\} \land y \in (0 \dots n (\emptyset))) \to x - y = n (\emptyset) - y$
279		fznn0sub2	$⊢ y \in (0 \dots n (\emptyset)) \to n (\emptyset) - y \in (0 \dots n (\emptyset))$
280	279	adantl	$⊢ (x \in \{n (\emptyset)\} \land y \in (0 \dots n (\emptyset))) \to n (\emptyset) - y \in (0 \dots n (\emptyset))$
281	278 280	eqeltrd	$⊢ (x \in \{n (\emptyset)\} \land y \in (0 \dots n (\emptyset))) \to x - y \in (0 \dots n (\emptyset))$
282	281	adantl	$⊢ (((φ \land n \in ({ℕ_{0}}^{1_{𝑜}})) \land i \in \{k \in ({ℕ_{0}}^{1_{𝑜}}) \| k \leq_{f} n\}) \land (x \in \{n (\emptyset)\} \land y \in (0 \dots n (\emptyset)))) \to x - y \in (0 \dots n (\emptyset))$
283		fvex	$⊢ n (\emptyset) \in V$
284	152 283	f1osn	$⊢ \{⟨\emptyset, n (\emptyset)⟩\} : \{\emptyset\} \underset{1-1 onto}{⟶} \{n (\emptyset)\}$
285		f1of	$⊢ \{⟨\emptyset, n (\emptyset)⟩\} : \{\emptyset\} \underset{1-1 onto}{⟶} \{n (\emptyset)\} \to \{⟨\emptyset, n (\emptyset)⟩\} : \{\emptyset\} ⟶ \{n (\emptyset)\}$
286	284 285	mp1i	$⊢ (φ \land n \in ({ℕ_{0}}^{1_{𝑜}})) \to \{⟨\emptyset, n (\emptyset)⟩\} : \{\emptyset\} ⟶ \{n (\emptyset)\}$
287		fvsng	$⊢ (\emptyset \in V \land n (\emptyset) \in ℕ_{0}) \to \{⟨\emptyset, n (\emptyset)⟩\} (\emptyset) = n (\emptyset)$
288	152 56 287	sylancr	$⊢ (φ \land n \in ({ℕ_{0}}^{1_{𝑜}})) \to \{⟨\emptyset, n (\emptyset)⟩\} (\emptyset) = n (\emptyset)$
289	288	eqcomd	$⊢ (φ \land n \in ({ℕ_{0}}^{1_{𝑜}})) \to n (\emptyset) = \{⟨\emptyset, n (\emptyset)⟩\} (\emptyset)$
290	152	a1i	$⊢ (φ \land n \in ({ℕ_{0}}^{1_{𝑜}})) \to \emptyset \in V$
291	150	a1i	$⊢ (φ \land n \in ({ℕ_{0}}^{1_{𝑜}})) \to \{\emptyset\} = 1_{𝑜}$
292	55 56	fsnd	$⊢ (φ \land n \in ({ℕ_{0}}^{1_{𝑜}})) \to \{⟨\emptyset, n (\emptyset)⟩\} : \{\emptyset\} ⟶ ℕ_{0}$
293	291 292	feq2dd	$⊢ (φ \land n \in ({ℕ_{0}}^{1_{𝑜}})) \to \{⟨\emptyset, n (\emptyset)⟩\} : 1_{𝑜} ⟶ ℕ_{0}$
294	293	ffnd	$⊢ (φ \land n \in ({ℕ_{0}}^{1_{𝑜}})) \to \{⟨\emptyset, n (\emptyset)⟩\} Fn 1_{𝑜}$
295	290 149 253 294	fsneq	$⊢ (φ \land n \in ({ℕ_{0}}^{1_{𝑜}})) \to (n = \{⟨\emptyset, n (\emptyset)⟩\} \leftrightarrow n (\emptyset) = \{⟨\emptyset, n (\emptyset)⟩\} (\emptyset))$
296	289 295	mpbird	$⊢ (φ \land n \in ({ℕ_{0}}^{1_{𝑜}})) \to n = \{⟨\emptyset, n (\emptyset)⟩\}$
297	149	a1i	$⊢ (φ \land n \in ({ℕ_{0}}^{1_{𝑜}})) \to 1_{𝑜} = \{\emptyset\}$
298	296 297	feq12d	$⊢ (φ \land n \in ({ℕ_{0}}^{1_{𝑜}})) \to (n : 1_{𝑜} ⟶ \{n (\emptyset)\} \leftrightarrow \{⟨\emptyset, n (\emptyset)⟩\} : \{\emptyset\} ⟶ \{n (\emptyset)\})$
299	286 298	mpbird	$⊢ (φ \land n \in ({ℕ_{0}}^{1_{𝑜}})) \to n : 1_{𝑜} ⟶ \{n (\emptyset)\}$
300	299	adantr	$⊢ ((φ \land n \in ({ℕ_{0}}^{1_{𝑜}})) \land i \in \{k \in ({ℕ_{0}}^{1_{𝑜}}) \| k \leq_{f} n\}) \to n : 1_{𝑜} ⟶ \{n (\emptyset)\}$
301	149	fneq2i	$⊢ i Fn 1_{𝑜} \leftrightarrow i Fn \{\emptyset\}$
302	255 301	sylib	$⊢ ((φ \land n \in ({ℕ_{0}}^{1_{𝑜}})) \land i \in \{k \in ({ℕ_{0}}^{1_{𝑜}}) \| k \leq_{f} n\}) \to i Fn \{\emptyset\}$
303		0zd	$⊢ ((φ \land n \in ({ℕ_{0}}^{1_{𝑜}})) \land i \in \{k \in ({ℕ_{0}}^{1_{𝑜}}) \| k \leq_{f} n\}) \to 0 \in ℤ$
304	139	nn0zd	$⊢ ((φ \land n \in ({ℕ_{0}}^{1_{𝑜}})) \land i \in \{k \in ({ℕ_{0}}^{1_{𝑜}}) \| k \leq_{f} n\}) \to n (\emptyset) \in ℤ$
305	105	nn0zd	$⊢ ((φ \land n \in ({ℕ_{0}}^{1_{𝑜}})) \land i \in \{k \in ({ℕ_{0}}^{1_{𝑜}}) \| k \leq_{f} n\}) \to i (\emptyset) \in ℤ$
306	105	nn0ge0d	$⊢ ((φ \land n \in ({ℕ_{0}}^{1_{𝑜}})) \land i \in \{k \in ({ℕ_{0}}^{1_{𝑜}}) \| k \leq_{f} n\}) \to 0 \leq i (\emptyset)$
307	303 304 305 306 125	elfzd	$⊢ ((φ \land n \in ({ℕ_{0}}^{1_{𝑜}})) \land i \in \{k \in ({ℕ_{0}}^{1_{𝑜}}) \| k \leq_{f} n\}) \to i (\emptyset) \in (0 \dots n (\emptyset))$
308		fveq2	$⊢ o = \emptyset \to i (o) = i (\emptyset)$
309	308	eleq1d	$⊢ o = \emptyset \to (i (o) \in (0 \dots n (\emptyset)) \leftrightarrow i (\emptyset) \in (0 \dots n (\emptyset)))$
310	152 309	ralsn	$⊢ \forall o \in \{\emptyset\} i (o) \in (0 \dots n (\emptyset)) \leftrightarrow i (\emptyset) \in (0 \dots n (\emptyset))$
311	307 310	sylibr	$⊢ ((φ \land n \in ({ℕ_{0}}^{1_{𝑜}})) \land i \in \{k \in ({ℕ_{0}}^{1_{𝑜}}) \| k \leq_{f} n\}) \to \forall o \in \{\emptyset\} i (o) \in (0 \dots n (\emptyset))$
312		ffnfv	$⊢ i : \{\emptyset\} ⟶ (0 \dots n (\emptyset)) \leftrightarrow (i Fn \{\emptyset\} \land \forall o \in \{\emptyset\} i (o) \in (0 \dots n (\emptyset)))$
313	302 311 312	sylanbrc	$⊢ ((φ \land n \in ({ℕ_{0}}^{1_{𝑜}})) \land i \in \{k \in ({ℕ_{0}}^{1_{𝑜}}) \| k \leq_{f} n\}) \to i : \{\emptyset\} ⟶ (0 \dots n (\emptyset))$
314	149 99	eqeltrrid	$⊢ ((φ \land n \in ({ℕ_{0}}^{1_{𝑜}})) \land i \in \{k \in ({ℕ_{0}}^{1_{𝑜}}) \| k \leq_{f} n\}) \to \{\emptyset\} \in V$
315	149	ineq2i	$⊢ 1_{𝑜} \cap 1_{𝑜} = 1_{𝑜} \cap \{\emptyset\}$
316	315 121	eqtr3i	$⊢ 1_{𝑜} \cap \{\emptyset\} = 1_{𝑜}$
317	282 300 313 99 314 316	off	$⊢ ((φ \land n \in ({ℕ_{0}}^{1_{𝑜}})) \land i \in \{k \in ({ℕ_{0}}^{1_{𝑜}}) \| k \leq_{f} n\}) \to (n -_{f} i) : 1_{𝑜} ⟶ (0 \dots n (\emptyset))$
318		fz0ssnn0	$⊢ (0 \dots n (\emptyset)) \subseteq ℕ_{0}$
319	318	a1i	$⊢ ((φ \land n \in ({ℕ_{0}}^{1_{𝑜}})) \land i \in \{k \in ({ℕ_{0}}^{1_{𝑜}}) \| k \leq_{f} n\}) \to (0 \dots n (\emptyset)) \subseteq ℕ_{0}$
320	317 319	fssd	$⊢ ((φ \land n \in ({ℕ_{0}}^{1_{𝑜}})) \land i \in \{k \in ({ℕ_{0}}^{1_{𝑜}}) \| k \leq_{f} n\}) \to (n -_{f} i) : 1_{𝑜} ⟶ ℕ_{0}$
321	320	adantr	$⊢ (((φ \land n \in ({ℕ_{0}}^{1_{𝑜}})) \land i \in \{k \in ({ℕ_{0}}^{1_{𝑜}}) \| k \leq_{f} n\}) \land m = n -_{f} i) \to (n -_{f} i) : 1_{𝑜} ⟶ ℕ_{0}$
322	321 252	ffvelcdmd	$⊢ (((φ \land n \in ({ℕ_{0}}^{1_{𝑜}})) \land i \in \{k \in ({ℕ_{0}}^{1_{𝑜}}) \| k \leq_{f} n\}) \land m = n -_{f} i) \to (n -_{f} i) (\emptyset) \in ℕ_{0}$
323	251 322	eqeltrd	$⊢ (((φ \land n \in ({ℕ_{0}}^{1_{𝑜}})) \land i \in \{k \in ({ℕ_{0}}^{1_{𝑜}}) \| k \leq_{f} n\}) \land m = n -_{f} i) \to m (\emptyset) \in ℕ_{0}$
324	263 323	fsnd	$⊢ (((φ \land n \in ({ℕ_{0}}^{1_{𝑜}})) \land i \in \{k \in ({ℕ_{0}}^{1_{𝑜}}) \| k \leq_{f} n\}) \land m = n -_{f} i) \to \{⟨X, m (\emptyset)⟩\} : \{X\} ⟶ ℕ_{0}$
325	324	ffnd	$⊢ (((φ \land n \in ({ℕ_{0}}^{1_{𝑜}})) \land i \in \{k \in ({ℕ_{0}}^{1_{𝑜}}) \| k \leq_{f} n\}) \land m = n -_{f} i) \to \{⟨X, m (\emptyset)⟩\} Fn \{X\}$
326	268 269 270 270 130	offn	$⊢ (((φ \land n \in ({ℕ_{0}}^{1_{𝑜}})) \land i \in \{k \in ({ℕ_{0}}^{1_{𝑜}}) \| k \leq_{f} n\}) \land m = n -_{f} i) \to (\{⟨X, n (\emptyset)⟩\} -_{f} \{⟨X, i (\emptyset)⟩\}) Fn \{X\}$
327	263 209 325 326	fsneq	$⊢ (((φ \land n \in ({ℕ_{0}}^{1_{𝑜}})) \land i \in \{k \in ({ℕ_{0}}^{1_{𝑜}}) \| k \leq_{f} n\}) \land m = n -_{f} i) \to (\{⟨X, m (\emptyset)⟩\} = \{⟨X, n (\emptyset)⟩\} -_{f} \{⟨X, i (\emptyset)⟩\} \leftrightarrow \{⟨X, m (\emptyset)⟩\} (X) = (\{⟨X, n (\emptyset)⟩\} -_{f} \{⟨X, i (\emptyset)⟩\}) (X))$
328	275 327	mpbird	$⊢ (((φ \land n \in ({ℕ_{0}}^{1_{𝑜}})) \land i \in \{k \in ({ℕ_{0}}^{1_{𝑜}}) \| k \leq_{f} n\}) \land m = n -_{f} i) \to \{⟨X, m (\emptyset)⟩\} = \{⟨X, n (\emptyset)⟩\} -_{f} \{⟨X, i (\emptyset)⟩\}$
329	328	fveq2d	$⊢ (((φ \land n \in ({ℕ_{0}}^{1_{𝑜}})) \land i \in \{k \in ({ℕ_{0}}^{1_{𝑜}}) \| k \leq_{f} n\}) \land m = n -_{f} i) \to G (\{⟨X, m (\emptyset)⟩\}) = G (\{⟨X, n (\emptyset)⟩\} -_{f} \{⟨X, i (\emptyset)⟩\})$
330	96 99 320	elmapdd	$⊢ ((φ \land n \in ({ℕ_{0}}^{1_{𝑜}})) \land i \in \{k \in ({ℕ_{0}}^{1_{𝑜}}) \| k \leq_{f} n\}) \to n -_{f} i \in ({ℕ_{0}}^{1_{𝑜}})$
331		fvexd	$⊢ ((φ \land n \in ({ℕ_{0}}^{1_{𝑜}})) \land i \in \{k \in ({ℕ_{0}}^{1_{𝑜}}) \| k \leq_{f} n\}) \to G (\{⟨X, n (\emptyset)⟩\} -_{f} \{⟨X, i (\emptyset)⟩\}) \in V$
332	249 329 330 331	fvmptd	$⊢ ((φ \land n \in ({ℕ_{0}}^{1_{𝑜}})) \land i \in \{k \in ({ℕ_{0}}^{1_{𝑜}}) \| k \leq_{f} n\}) \to M (G) (n -_{f} i) = G (\{⟨X, n (\emptyset)⟩\} -_{f} \{⟨X, i (\emptyset)⟩\})$
333	238 332	oveq12d	$⊢ ((φ \land n \in ({ℕ_{0}}^{1_{𝑜}})) \land i \in \{k \in ({ℕ_{0}}^{1_{𝑜}}) \| k \leq_{f} n\}) \to M (F) (i) \cdot_{R} M (G) (n -_{f} i) = F (\{⟨X, i (\emptyset)⟩\}) \cdot_{R} G (\{⟨X, n (\emptyset)⟩\} -_{f} \{⟨X, i (\emptyset)⟩\})$
334	333	mpteq2dva	$⊢ (φ \land n \in ({ℕ_{0}}^{1_{𝑜}})) \to (i \in \{k \in ({ℕ_{0}}^{1_{𝑜}}) \| k \leq_{f} n\} ⟼ M (F) (i) \cdot_{R} M (G) (n -_{f} i)) = (i \in \{k \in ({ℕ_{0}}^{1_{𝑜}}) \| k \leq_{f} n\} ⟼ F (\{⟨X, i (\emptyset)⟩\}) \cdot_{R} G (\{⟨X, n (\emptyset)⟩\} -_{f} \{⟨X, i (\emptyset)⟩\}))$
335	334	oveq2d	$⊢ (φ \land n \in ({ℕ_{0}}^{1_{𝑜}})) \to \underset{i \in \{k \in ({ℕ_{0}}^{1_{𝑜}}) \| k \leq_{f} n\}}{\sum_{R}} (M (F) (i) \cdot_{R} M (G) (n -_{f} i)) = \underset{i \in \{k \in ({ℕ_{0}}^{1_{𝑜}}) \| k \leq_{f} n\}}{\sum_{R}} (F (\{⟨X, i (\emptyset)⟩\}) \cdot_{R} G (\{⟨X, n (\emptyset)⟩\} -_{f} \{⟨X, i (\emptyset)⟩\}))$
336	221 335	eqtr4d	$⊢ (φ \land n \in ({ℕ_{0}}^{1_{𝑜}})) \to \underset{j \in \{l \in \{g \in ({ℕ_{0}}^{\{X\}}) \| {finSupp}_{0} (g)\} \| l \leq_{f} \{⟨X, n (\emptyset)⟩\}\}}{\sum_{R}} (F (j) \cdot_{R} G (\{⟨X, n (\emptyset)⟩\} -_{f} j)) = \underset{i \in \{k \in ({ℕ_{0}}^{1_{𝑜}}) \| k \leq_{f} n\}}{\sum_{R}} (M (F) (i) \cdot_{R} M (G) (n -_{f} i))$
337	23 336	sylan9eqr	$⊢ ((φ \land n \in ({ℕ_{0}}^{1_{𝑜}})) \land m = \{⟨X, n (\emptyset)⟩\}) \to \underset{j \in \{l \in \{g \in ({ℕ_{0}}^{\{X\}}) \| {finSupp}_{0} (g)\} \| l \leq_{f} m\}}{\sum_{R}} (F (j) \cdot_{R} G (m -_{f} j)) = \underset{i \in \{k \in ({ℕ_{0}}^{1_{𝑜}}) \| k \leq_{f} n\}}{\sum_{R}} (M (F) (i) \cdot_{R} M (G) (n -_{f} i))$
338		ovexd	$⊢ (φ \land n \in ({ℕ_{0}}^{1_{𝑜}})) \to \underset{i \in \{k \in ({ℕ_{0}}^{1_{𝑜}}) \| k \leq_{f} n\}}{\sum_{R}} (M (F) (i) \cdot_{R} M (G) (n -_{f} i)) \in V$
339	17 337 64 338	fvmptd	$⊢ (φ \land n \in ({ℕ_{0}}^{1_{𝑜}})) \to (F \underset{˙}{\cdot} G) (\{⟨X, n (\emptyset)⟩\}) = \underset{i \in \{k \in ({ℕ_{0}}^{1_{𝑜}}) \| k \leq_{f} n\}}{\sum_{R}} (M (F) (i) \cdot_{R} M (G) (n -_{f} i))$
340	339	mpteq2dva	$⊢ φ \to (n \in ({ℕ_{0}}^{1_{𝑜}}) ⟼ (F \underset{˙}{\cdot} G) (\{⟨X, n (\emptyset)⟩\})) = (n \in ({ℕ_{0}}^{1_{𝑜}}) ⟼ \underset{i \in \{k \in ({ℕ_{0}}^{1_{𝑜}}) \| k \leq_{f} n\}}{\sum_{R}} (M (F) (i) \cdot_{R} M (G) (n -_{f} i)))$
341		eqid	$⊢ 1_{𝑜} mPoly R = 1_{𝑜} mPoly R$
342		eqid	$⊢ {Base}_{Q} = {Base}_{Q}$
343	5 342	ply1bas	$⊢ {Base}_{Q} = {Base}_{(1_{𝑜} mPoly R)}$
344	5 341 4	ply1mulr	$⊢ \underset{˙}{\times} = \cdot_{(1_{𝑜} mPoly R)}$
345		psr1baslem	$⊢ {ℕ_{0}}^{1_{𝑜}} = \{h \in ({ℕ_{0}}^{1_{𝑜}}) \| h^{-1} [ℕ] \in Fin\}$
346	1 2 3 4 5 6 7 8 9	selvply1rhmlema	$⊢ φ \to M (F) \in {Base}_{Q}$
347	1 2 3 4 5 6 7 8 10	selvply1rhmlema	$⊢ φ \to M (G) \in {Base}_{Q}$
348	341 343 13 344 345 346 347	mplmul	$⊢ φ \to M (F) \underset{˙}{\times} M (G) = (n \in ({ℕ_{0}}^{1_{𝑜}}) ⟼ \underset{i \in \{k \in ({ℕ_{0}}^{1_{𝑜}}) \| k \leq_{f} n\}}{\sum_{R}} (M (F) (i) \cdot_{R} M (G) (n -_{f} i)))$
349	340 348	eqtr4d	$⊢ φ \to (n \in ({ℕ_{0}}^{1_{𝑜}}) ⟼ (F \underset{˙}{\cdot} G) (\{⟨X, n (\emptyset)⟩\})) = M (F) \underset{˙}{\times} M (G)$
350	12 349	sylan9eqr	$⊢ (φ \land f = F \underset{˙}{\cdot} G) \to (n \in ({ℕ_{0}}^{1_{𝑜}}) ⟼ f (\{⟨X, n (\emptyset)⟩\})) = M (F) \underset{˙}{\times} M (G)$
351	47	a1i	$⊢ φ \to \{X\} \in V$
352	2 351 8	mplringd	$⊢ φ \to P \in Ring$
353	1 3 352 9 10	ringcld	$⊢ φ \to F \underset{˙}{\cdot} G \in B$
354		ovexd	$⊢ φ \to M (F) \underset{˙}{\times} M (G) \in V$
355	6 350 353 354	fvmptd2	$⊢ φ \to M (F \underset{˙}{\cdot} G) = M (F) \underset{˙}{\times} M (G)$

Metamath Proof Explorer

Theorem selvply1rhmlemb

Proof