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

Metamath Proof Explorer

Theorem selvply1rhmlemb

Proof