pf1ind

Description: Prove a property of polynomials by "structural" induction, under a simplified model of structure which loses the sum of products structure. (Contributed by Mario Carneiro, 12-Jun-2015)

	Ref	Expression
Hypotheses	pf1ind.cb	$⊢ B = {Base}_{R}$
	pf1ind.cp	$⊢ \underset{˙}{+} = +_{R}$
	pf1ind.ct	$⊢ \underset{˙}{\cdot} = \cdot_{R}$
	pf1ind.cq	$⊢ Q = ran {eval}_{1} (R)$
	pf1ind.ad	$⊢ (φ \land ((f \in Q \land τ) \land (g \in Q \land η))) \to ζ$
	pf1ind.mu	$⊢ (φ \land ((f \in Q \land τ) \land (g \in Q \land η))) \to σ$
	pf1ind.wa	$⊢ x = B \times \{f\} \to (ψ \leftrightarrow χ)$
	pf1ind.wb	$⊢ x = {I ↾}_{B} \to (ψ \leftrightarrow θ)$
	pf1ind.wc	$⊢ x = f \to (ψ \leftrightarrow τ)$
	pf1ind.wd	$⊢ x = g \to (ψ \leftrightarrow η)$
	pf1ind.we	$⊢ x = f {\underset{˙}{+}}_{f} g \to (ψ \leftrightarrow ζ)$
	pf1ind.wf	$⊢ x = f {\underset{˙}{\cdot}}_{f} g \to (ψ \leftrightarrow σ)$
	pf1ind.wg	$⊢ x = A \to (ψ \leftrightarrow ρ)$
	pf1ind.co	$⊢ (φ \land f \in B) \to χ$
	pf1ind.pr	$⊢ φ \to θ$
	pf1ind.a	$⊢ φ \to A \in Q$
Assertion	pf1ind	$⊢ φ \to ρ$

Proof

Step	Hyp	Ref	Expression
1		pf1ind.cb	$⊢ B = {Base}_{R}$
2		pf1ind.cp	$⊢ \underset{˙}{+} = +_{R}$
3		pf1ind.ct	$⊢ \underset{˙}{\cdot} = \cdot_{R}$
4		pf1ind.cq	$⊢ Q = ran {eval}_{1} (R)$
5		pf1ind.ad	$⊢ (φ \land ((f \in Q \land τ) \land (g \in Q \land η))) \to ζ$
6		pf1ind.mu	$⊢ (φ \land ((f \in Q \land τ) \land (g \in Q \land η))) \to σ$
7		pf1ind.wa	$⊢ x = B \times \{f\} \to (ψ \leftrightarrow χ)$
8		pf1ind.wb	$⊢ x = {I ↾}_{B} \to (ψ \leftrightarrow θ)$
9		pf1ind.wc	$⊢ x = f \to (ψ \leftrightarrow τ)$
10		pf1ind.wd	$⊢ x = g \to (ψ \leftrightarrow η)$
11		pf1ind.we	$⊢ x = f {\underset{˙}{+}}_{f} g \to (ψ \leftrightarrow ζ)$
12		pf1ind.wf	$⊢ x = f {\underset{˙}{\cdot}}_{f} g \to (ψ \leftrightarrow σ)$
13		pf1ind.wg	$⊢ x = A \to (ψ \leftrightarrow ρ)$
14		pf1ind.co	$⊢ (φ \land f \in B) \to χ$
15		pf1ind.pr	$⊢ φ \to θ$
16		pf1ind.a	$⊢ φ \to A \in Q$
17		coass	$⊢ (A \circ (b \in (B^{1_{𝑜}}) ⟼ b (\emptyset))) \circ (w \in B ⟼ 1_{𝑜} \times \{w\}) = A \circ ((b \in (B^{1_{𝑜}}) ⟼ b (\emptyset)) \circ (w \in B ⟼ 1_{𝑜} \times \{w\}))$
18		df1o2	$⊢ 1_{𝑜} = \{\emptyset\}$
19	1	fvexi	$⊢ B \in V$
20		0ex	$⊢ \emptyset \in V$
21		eqid	$⊢ (b \in (B^{1_{𝑜}}) ⟼ b (\emptyset)) = (b \in (B^{1_{𝑜}}) ⟼ b (\emptyset))$
22	18 19 20 21	mapsncnv	$⊢ {(b \in (B^{1_{𝑜}}) ⟼ b (\emptyset))}^{-1} = (w \in B ⟼ 1_{𝑜} \times \{w\})$
23	22	coeq2i	$⊢ (b \in (B^{1_{𝑜}}) ⟼ b (\emptyset)) \circ {(b \in (B^{1_{𝑜}}) ⟼ b (\emptyset))}^{-1} = (b \in (B^{1_{𝑜}}) ⟼ b (\emptyset)) \circ (w \in B ⟼ 1_{𝑜} \times \{w\})$
24	18 19 20 21	mapsnf1o2	$⊢ (b \in (B^{1_{𝑜}}) ⟼ b (\emptyset)) : B^{1_{𝑜}} \underset{1-1 onto}{⟶} B$
25		f1ococnv2	$⊢ (b \in (B^{1_{𝑜}}) ⟼ b (\emptyset)) : B^{1_{𝑜}} \underset{1-1 onto}{⟶} B \to (b \in (B^{1_{𝑜}}) ⟼ b (\emptyset)) \circ {(b \in (B^{1_{𝑜}}) ⟼ b (\emptyset))}^{-1} = {I ↾}_{B}$
26	24 25	mp1i	$⊢ φ \to (b \in (B^{1_{𝑜}}) ⟼ b (\emptyset)) \circ {(b \in (B^{1_{𝑜}}) ⟼ b (\emptyset))}^{-1} = {I ↾}_{B}$
27	23 26	eqtr3id	$⊢ φ \to (b \in (B^{1_{𝑜}}) ⟼ b (\emptyset)) \circ (w \in B ⟼ 1_{𝑜} \times \{w\}) = {I ↾}_{B}$
28	27	coeq2d	$⊢ φ \to A \circ ((b \in (B^{1_{𝑜}}) ⟼ b (\emptyset)) \circ (w \in B ⟼ 1_{𝑜} \times \{w\})) = A \circ ({I ↾}_{B})$
29	17 28	eqtrid	$⊢ φ \to (A \circ (b \in (B^{1_{𝑜}}) ⟼ b (\emptyset))) \circ (w \in B ⟼ 1_{𝑜} \times \{w\}) = A \circ ({I ↾}_{B})$
30	4 1	pf1f	$⊢ A \in Q \to A : B ⟶ B$
31		fcoi1	$⊢ A : B ⟶ B \to A \circ ({I ↾}_{B}) = A$
32	16 30 31	3syl	$⊢ φ \to A \circ ({I ↾}_{B}) = A$
33	29 32	eqtrd	$⊢ φ \to (A \circ (b \in (B^{1_{𝑜}}) ⟼ b (\emptyset))) \circ (w \in B ⟼ 1_{𝑜} \times \{w\}) = A$
34		eqid	$⊢ 1_{𝑜} eval R = 1_{𝑜} eval R$
35	34 1	evlval	$⊢ 1_{𝑜} eval R = (1_{𝑜} evalSub R) (B)$
36	35	rneqi	$⊢ ran (1_{𝑜} eval R) = ran (1_{𝑜} evalSub R) (B)$
37		an4	$⊢ ((a \in ran (1_{𝑜} eval R) \land a \circ (w \in B ⟼ 1_{𝑜} \times \{w\}) \in \{x \| ψ\}) \land (b \in ran (1_{𝑜} eval R) \land b \circ (w \in B ⟼ 1_{𝑜} \times \{w\}) \in \{x \| ψ\})) \leftrightarrow ((a \in ran (1_{𝑜} eval R) \land b \in ran (1_{𝑜} eval R)) \land (a \circ (w \in B ⟼ 1_{𝑜} \times \{w\}) \in \{x \| ψ\} \land b \circ (w \in B ⟼ 1_{𝑜} \times \{w\}) \in \{x \| ψ\}))$
38		eqid	$⊢ ran (1_{𝑜} eval R) = ran (1_{𝑜} eval R)$
39	4 1 38	mpfpf1	$⊢ a \in ran (1_{𝑜} eval R) \to a \circ (w \in B ⟼ 1_{𝑜} \times \{w\}) \in Q$
40	4 1 38	mpfpf1	$⊢ b \in ran (1_{𝑜} eval R) \to b \circ (w \in B ⟼ 1_{𝑜} \times \{w\}) \in Q$
41		vex	$⊢ f \in V$
42	41 9	elab	$⊢ f \in \{x \| ψ\} \leftrightarrow τ$
43		eleq1	$⊢ f = a \circ (w \in B ⟼ 1_{𝑜} \times \{w\}) \to (f \in \{x \| ψ\} \leftrightarrow a \circ (w \in B ⟼ 1_{𝑜} \times \{w\}) \in \{x \| ψ\})$
44	42 43	bitr3id	$⊢ f = a \circ (w \in B ⟼ 1_{𝑜} \times \{w\}) \to (τ \leftrightarrow a \circ (w \in B ⟼ 1_{𝑜} \times \{w\}) \in \{x \| ψ\})$
45	44	anbi1d	$⊢ f = a \circ (w \in B ⟼ 1_{𝑜} \times \{w\}) \to ((τ \land η) \leftrightarrow (a \circ (w \in B ⟼ 1_{𝑜} \times \{w\}) \in \{x \| ψ\} \land η))$
46	45	anbi1d	$⊢ f = a \circ (w \in B ⟼ 1_{𝑜} \times \{w\}) \to (((τ \land η) \land φ) \leftrightarrow ((a \circ (w \in B ⟼ 1_{𝑜} \times \{w\}) \in \{x \| ψ\} \land η) \land φ))$
47		ovex	$⊢ f {\underset{˙}{+}}_{f} g \in V$
48	47 11	elab	$⊢ f {\underset{˙}{+}}_{f} g \in \{x \| ψ\} \leftrightarrow ζ$
49		oveq1	$⊢ f = a \circ (w \in B ⟼ 1_{𝑜} \times \{w\}) \to f {\underset{˙}{+}}_{f} g = (a \circ (w \in B ⟼ 1_{𝑜} \times \{w\})) {\underset{˙}{+}}_{f} g$
50	49	eleq1d	$⊢ f = a \circ (w \in B ⟼ 1_{𝑜} \times \{w\}) \to (f {\underset{˙}{+}}_{f} g \in \{x \| ψ\} \leftrightarrow (a \circ (w \in B ⟼ 1_{𝑜} \times \{w\})) {\underset{˙}{+}}_{f} g \in \{x \| ψ\})$
51	48 50	bitr3id	$⊢ f = a \circ (w \in B ⟼ 1_{𝑜} \times \{w\}) \to (ζ \leftrightarrow (a \circ (w \in B ⟼ 1_{𝑜} \times \{w\})) {\underset{˙}{+}}_{f} g \in \{x \| ψ\})$
52	46 51	imbi12d	$⊢ f = a \circ (w \in B ⟼ 1_{𝑜} \times \{w\}) \to ((((τ \land η) \land φ) \to ζ) \leftrightarrow (((a \circ (w \in B ⟼ 1_{𝑜} \times \{w\}) \in \{x \| ψ\} \land η) \land φ) \to (a \circ (w \in B ⟼ 1_{𝑜} \times \{w\})) {\underset{˙}{+}}_{f} g \in \{x \| ψ\}))$
53		vex	$⊢ g \in V$
54	53 10	elab	$⊢ g \in \{x \| ψ\} \leftrightarrow η$
55		eleq1	$⊢ g = b \circ (w \in B ⟼ 1_{𝑜} \times \{w\}) \to (g \in \{x \| ψ\} \leftrightarrow b \circ (w \in B ⟼ 1_{𝑜} \times \{w\}) \in \{x \| ψ\})$
56	54 55	bitr3id	$⊢ g = b \circ (w \in B ⟼ 1_{𝑜} \times \{w\}) \to (η \leftrightarrow b \circ (w \in B ⟼ 1_{𝑜} \times \{w\}) \in \{x \| ψ\})$
57	56	anbi2d	$⊢ g = b \circ (w \in B ⟼ 1_{𝑜} \times \{w\}) \to ((a \circ (w \in B ⟼ 1_{𝑜} \times \{w\}) \in \{x \| ψ\} \land η) \leftrightarrow (a \circ (w \in B ⟼ 1_{𝑜} \times \{w\}) \in \{x \| ψ\} \land b \circ (w \in B ⟼ 1_{𝑜} \times \{w\}) \in \{x \| ψ\}))$
58	57	anbi1d	$⊢ g = b \circ (w \in B ⟼ 1_{𝑜} \times \{w\}) \to (((a \circ (w \in B ⟼ 1_{𝑜} \times \{w\}) \in \{x \| ψ\} \land η) \land φ) \leftrightarrow ((a \circ (w \in B ⟼ 1_{𝑜} \times \{w\}) \in \{x \| ψ\} \land b \circ (w \in B ⟼ 1_{𝑜} \times \{w\}) \in \{x \| ψ\}) \land φ))$
59		oveq2	$⊢ g = b \circ (w \in B ⟼ 1_{𝑜} \times \{w\}) \to (a \circ (w \in B ⟼ 1_{𝑜} \times \{w\})) {\underset{˙}{+}}_{f} g = (a \circ (w \in B ⟼ 1_{𝑜} \times \{w\})) {\underset{˙}{+}}_{f} (b \circ (w \in B ⟼ 1_{𝑜} \times \{w\}))$
60	59	eleq1d	$⊢ g = b \circ (w \in B ⟼ 1_{𝑜} \times \{w\}) \to ((a \circ (w \in B ⟼ 1_{𝑜} \times \{w\})) {\underset{˙}{+}}_{f} g \in \{x \| ψ\} \leftrightarrow (a \circ (w \in B ⟼ 1_{𝑜} \times \{w\})) {\underset{˙}{+}}_{f} (b \circ (w \in B ⟼ 1_{𝑜} \times \{w\})) \in \{x \| ψ\})$
61	58 60	imbi12d	$⊢ g = b \circ (w \in B ⟼ 1_{𝑜} \times \{w\}) \to ((((a \circ (w \in B ⟼ 1_{𝑜} \times \{w\}) \in \{x \| ψ\} \land η) \land φ) \to (a \circ (w \in B ⟼ 1_{𝑜} \times \{w\})) {\underset{˙}{+}}_{f} g \in \{x \| ψ\}) \leftrightarrow (((a \circ (w \in B ⟼ 1_{𝑜} \times \{w\}) \in \{x \| ψ\} \land b \circ (w \in B ⟼ 1_{𝑜} \times \{w\}) \in \{x \| ψ\}) \land φ) \to (a \circ (w \in B ⟼ 1_{𝑜} \times \{w\})) {\underset{˙}{+}}_{f} (b \circ (w \in B ⟼ 1_{𝑜} \times \{w\})) \in \{x \| ψ\}))$
62	5	expcom	$⊢ ((f \in Q \land τ) \land (g \in Q \land η)) \to (φ \to ζ)$
63	62	an4s	$⊢ ((f \in Q \land g \in Q) \land (τ \land η)) \to (φ \to ζ)$
64	63	expimpd	$⊢ (f \in Q \land g \in Q) \to (((τ \land η) \land φ) \to ζ)$
65	52 61 64	vtocl2ga	$⊢ (a \circ (w \in B ⟼ 1_{𝑜} \times \{w\}) \in Q \land b \circ (w \in B ⟼ 1_{𝑜} \times \{w\}) \in Q) \to (((a \circ (w \in B ⟼ 1_{𝑜} \times \{w\}) \in \{x \| ψ\} \land b \circ (w \in B ⟼ 1_{𝑜} \times \{w\}) \in \{x \| ψ\}) \land φ) \to (a \circ (w \in B ⟼ 1_{𝑜} \times \{w\})) {\underset{˙}{+}}_{f} (b \circ (w \in B ⟼ 1_{𝑜} \times \{w\})) \in \{x \| ψ\})$
66	39 40 65	syl2an	$⊢ (a \in ran (1_{𝑜} eval R) \land b \in ran (1_{𝑜} eval R)) \to (((a \circ (w \in B ⟼ 1_{𝑜} \times \{w\}) \in \{x \| ψ\} \land b \circ (w \in B ⟼ 1_{𝑜} \times \{w\}) \in \{x \| ψ\}) \land φ) \to (a \circ (w \in B ⟼ 1_{𝑜} \times \{w\})) {\underset{˙}{+}}_{f} (b \circ (w \in B ⟼ 1_{𝑜} \times \{w\})) \in \{x \| ψ\})$
67	66	expcomd	$⊢ (a \in ran (1_{𝑜} eval R) \land b \in ran (1_{𝑜} eval R)) \to (φ \to ((a \circ (w \in B ⟼ 1_{𝑜} \times \{w\}) \in \{x \| ψ\} \land b \circ (w \in B ⟼ 1_{𝑜} \times \{w\}) \in \{x \| ψ\}) \to (a \circ (w \in B ⟼ 1_{𝑜} \times \{w\})) {\underset{˙}{+}}_{f} (b \circ (w \in B ⟼ 1_{𝑜} \times \{w\})) \in \{x \| ψ\}))$
68	67	impcom	$⊢ (φ \land (a \in ran (1_{𝑜} eval R) \land b \in ran (1_{𝑜} eval R))) \to ((a \circ (w \in B ⟼ 1_{𝑜} \times \{w\}) \in \{x \| ψ\} \land b \circ (w \in B ⟼ 1_{𝑜} \times \{w\}) \in \{x \| ψ\}) \to (a \circ (w \in B ⟼ 1_{𝑜} \times \{w\})) {\underset{˙}{+}}_{f} (b \circ (w \in B ⟼ 1_{𝑜} \times \{w\})) \in \{x \| ψ\})$
69	36 1	mpff	$⊢ a \in ran (1_{𝑜} eval R) \to a : B^{1_{𝑜}} ⟶ B$
70	69	ad2antrl	$⊢ (φ \land (a \in ran (1_{𝑜} eval R) \land b \in ran (1_{𝑜} eval R))) \to a : B^{1_{𝑜}} ⟶ B$
71	70	ffnd	$⊢ (φ \land (a \in ran (1_{𝑜} eval R) \land b \in ran (1_{𝑜} eval R))) \to a Fn (B^{1_{𝑜}})$
72	36 1	mpff	$⊢ b \in ran (1_{𝑜} eval R) \to b : B^{1_{𝑜}} ⟶ B$
73	72	ad2antll	$⊢ (φ \land (a \in ran (1_{𝑜} eval R) \land b \in ran (1_{𝑜} eval R))) \to b : B^{1_{𝑜}} ⟶ B$
74	73	ffnd	$⊢ (φ \land (a \in ran (1_{𝑜} eval R) \land b \in ran (1_{𝑜} eval R))) \to b Fn (B^{1_{𝑜}})$
75		eqid	$⊢ (w \in B ⟼ 1_{𝑜} \times \{w\}) = (w \in B ⟼ 1_{𝑜} \times \{w\})$
76	18 19 20 75	mapsnf1o3	$⊢ (w \in B ⟼ 1_{𝑜} \times \{w\}) : B \underset{1-1 onto}{⟶} B^{1_{𝑜}}$
77		f1of	$⊢ (w \in B ⟼ 1_{𝑜} \times \{w\}) : B \underset{1-1 onto}{⟶} B^{1_{𝑜}} \to (w \in B ⟼ 1_{𝑜} \times \{w\}) : B ⟶ B^{1_{𝑜}}$
78	76 77	mp1i	$⊢ (φ \land (a \in ran (1_{𝑜} eval R) \land b \in ran (1_{𝑜} eval R))) \to (w \in B ⟼ 1_{𝑜} \times \{w\}) : B ⟶ B^{1_{𝑜}}$
79		ovexd	$⊢ (φ \land (a \in ran (1_{𝑜} eval R) \land b \in ran (1_{𝑜} eval R))) \to B^{1_{𝑜}} \in V$
80	19	a1i	$⊢ (φ \land (a \in ran (1_{𝑜} eval R) \land b \in ran (1_{𝑜} eval R))) \to B \in V$
81		inidm	$⊢ (B^{1_{𝑜}}) \cap (B^{1_{𝑜}}) = B^{1_{𝑜}}$
82	71 74 78 79 79 80 81	ofco	$⊢ (φ \land (a \in ran (1_{𝑜} eval R) \land b \in ran (1_{𝑜} eval R))) \to (a {\underset{˙}{+}}_{f} b) \circ (w \in B ⟼ 1_{𝑜} \times \{w\}) = (a \circ (w \in B ⟼ 1_{𝑜} \times \{w\})) {\underset{˙}{+}}_{f} (b \circ (w \in B ⟼ 1_{𝑜} \times \{w\}))$
83	82	eleq1d	$⊢ (φ \land (a \in ran (1_{𝑜} eval R) \land b \in ran (1_{𝑜} eval R))) \to ((a {\underset{˙}{+}}_{f} b) \circ (w \in B ⟼ 1_{𝑜} \times \{w\}) \in \{x \| ψ\} \leftrightarrow (a \circ (w \in B ⟼ 1_{𝑜} \times \{w\})) {\underset{˙}{+}}_{f} (b \circ (w \in B ⟼ 1_{𝑜} \times \{w\})) \in \{x \| ψ\})$
84	68 83	sylibrd	$⊢ (φ \land (a \in ran (1_{𝑜} eval R) \land b \in ran (1_{𝑜} eval R))) \to ((a \circ (w \in B ⟼ 1_{𝑜} \times \{w\}) \in \{x \| ψ\} \land b \circ (w \in B ⟼ 1_{𝑜} \times \{w\}) \in \{x \| ψ\}) \to (a {\underset{˙}{+}}_{f} b) \circ (w \in B ⟼ 1_{𝑜} \times \{w\}) \in \{x \| ψ\})$
85	84	expimpd	$⊢ φ \to (((a \in ran (1_{𝑜} eval R) \land b \in ran (1_{𝑜} eval R)) \land (a \circ (w \in B ⟼ 1_{𝑜} \times \{w\}) \in \{x \| ψ\} \land b \circ (w \in B ⟼ 1_{𝑜} \times \{w\}) \in \{x \| ψ\})) \to (a {\underset{˙}{+}}_{f} b) \circ (w \in B ⟼ 1_{𝑜} \times \{w\}) \in \{x \| ψ\})$
86	37 85	biimtrid	$⊢ φ \to (((a \in ran (1_{𝑜} eval R) \land a \circ (w \in B ⟼ 1_{𝑜} \times \{w\}) \in \{x \| ψ\}) \land (b \in ran (1_{𝑜} eval R) \land b \circ (w \in B ⟼ 1_{𝑜} \times \{w\}) \in \{x \| ψ\})) \to (a {\underset{˙}{+}}_{f} b) \circ (w \in B ⟼ 1_{𝑜} \times \{w\}) \in \{x \| ψ\})$
87	86	imp	$⊢ (φ \land ((a \in ran (1_{𝑜} eval R) \land a \circ (w \in B ⟼ 1_{𝑜} \times \{w\}) \in \{x \| ψ\}) \land (b \in ran (1_{𝑜} eval R) \land b \circ (w \in B ⟼ 1_{𝑜} \times \{w\}) \in \{x \| ψ\}))) \to (a {\underset{˙}{+}}_{f} b) \circ (w \in B ⟼ 1_{𝑜} \times \{w\}) \in \{x \| ψ\}$
88		ovex	$⊢ f {\underset{˙}{\cdot}}_{f} g \in V$
89	88 12	elab	$⊢ f {\underset{˙}{\cdot}}_{f} g \in \{x \| ψ\} \leftrightarrow σ$
90		oveq1	$⊢ f = a \circ (w \in B ⟼ 1_{𝑜} \times \{w\}) \to f {\underset{˙}{\cdot}}_{f} g = (a \circ (w \in B ⟼ 1_{𝑜} \times \{w\})) {\underset{˙}{\cdot}}_{f} g$
91	90	eleq1d	$⊢ f = a \circ (w \in B ⟼ 1_{𝑜} \times \{w\}) \to (f {\underset{˙}{\cdot}}_{f} g \in \{x \| ψ\} \leftrightarrow (a \circ (w \in B ⟼ 1_{𝑜} \times \{w\})) {\underset{˙}{\cdot}}_{f} g \in \{x \| ψ\})$
92	89 91	bitr3id	$⊢ f = a \circ (w \in B ⟼ 1_{𝑜} \times \{w\}) \to (σ \leftrightarrow (a \circ (w \in B ⟼ 1_{𝑜} \times \{w\})) {\underset{˙}{\cdot}}_{f} g \in \{x \| ψ\})$
93	46 92	imbi12d	$⊢ f = a \circ (w \in B ⟼ 1_{𝑜} \times \{w\}) \to ((((τ \land η) \land φ) \to σ) \leftrightarrow (((a \circ (w \in B ⟼ 1_{𝑜} \times \{w\}) \in \{x \| ψ\} \land η) \land φ) \to (a \circ (w \in B ⟼ 1_{𝑜} \times \{w\})) {\underset{˙}{\cdot}}_{f} g \in \{x \| ψ\}))$
94		oveq2	$⊢ g = b \circ (w \in B ⟼ 1_{𝑜} \times \{w\}) \to (a \circ (w \in B ⟼ 1_{𝑜} \times \{w\})) {\underset{˙}{\cdot}}_{f} g = (a \circ (w \in B ⟼ 1_{𝑜} \times \{w\})) {\underset{˙}{\cdot}}_{f} (b \circ (w \in B ⟼ 1_{𝑜} \times \{w\}))$
95	94	eleq1d	$⊢ g = b \circ (w \in B ⟼ 1_{𝑜} \times \{w\}) \to ((a \circ (w \in B ⟼ 1_{𝑜} \times \{w\})) {\underset{˙}{\cdot}}_{f} g \in \{x \| ψ\} \leftrightarrow (a \circ (w \in B ⟼ 1_{𝑜} \times \{w\})) {\underset{˙}{\cdot}}_{f} (b \circ (w \in B ⟼ 1_{𝑜} \times \{w\})) \in \{x \| ψ\})$
96	58 95	imbi12d	$⊢ g = b \circ (w \in B ⟼ 1_{𝑜} \times \{w\}) \to ((((a \circ (w \in B ⟼ 1_{𝑜} \times \{w\}) \in \{x \| ψ\} \land η) \land φ) \to (a \circ (w \in B ⟼ 1_{𝑜} \times \{w\})) {\underset{˙}{\cdot}}_{f} g \in \{x \| ψ\}) \leftrightarrow (((a \circ (w \in B ⟼ 1_{𝑜} \times \{w\}) \in \{x \| ψ\} \land b \circ (w \in B ⟼ 1_{𝑜} \times \{w\}) \in \{x \| ψ\}) \land φ) \to (a \circ (w \in B ⟼ 1_{𝑜} \times \{w\})) {\underset{˙}{\cdot}}_{f} (b \circ (w \in B ⟼ 1_{𝑜} \times \{w\})) \in \{x \| ψ\}))$
97	6	expcom	$⊢ ((f \in Q \land τ) \land (g \in Q \land η)) \to (φ \to σ)$
98	97	an4s	$⊢ ((f \in Q \land g \in Q) \land (τ \land η)) \to (φ \to σ)$
99	98	expimpd	$⊢ (f \in Q \land g \in Q) \to (((τ \land η) \land φ) \to σ)$
100	93 96 99	vtocl2ga	$⊢ (a \circ (w \in B ⟼ 1_{𝑜} \times \{w\}) \in Q \land b \circ (w \in B ⟼ 1_{𝑜} \times \{w\}) \in Q) \to (((a \circ (w \in B ⟼ 1_{𝑜} \times \{w\}) \in \{x \| ψ\} \land b \circ (w \in B ⟼ 1_{𝑜} \times \{w\}) \in \{x \| ψ\}) \land φ) \to (a \circ (w \in B ⟼ 1_{𝑜} \times \{w\})) {\underset{˙}{\cdot}}_{f} (b \circ (w \in B ⟼ 1_{𝑜} \times \{w\})) \in \{x \| ψ\})$
101	39 40 100	syl2an	$⊢ (a \in ran (1_{𝑜} eval R) \land b \in ran (1_{𝑜} eval R)) \to (((a \circ (w \in B ⟼ 1_{𝑜} \times \{w\}) \in \{x \| ψ\} \land b \circ (w \in B ⟼ 1_{𝑜} \times \{w\}) \in \{x \| ψ\}) \land φ) \to (a \circ (w \in B ⟼ 1_{𝑜} \times \{w\})) {\underset{˙}{\cdot}}_{f} (b \circ (w \in B ⟼ 1_{𝑜} \times \{w\})) \in \{x \| ψ\})$
102	101	expcomd	$⊢ (a \in ran (1_{𝑜} eval R) \land b \in ran (1_{𝑜} eval R)) \to (φ \to ((a \circ (w \in B ⟼ 1_{𝑜} \times \{w\}) \in \{x \| ψ\} \land b \circ (w \in B ⟼ 1_{𝑜} \times \{w\}) \in \{x \| ψ\}) \to (a \circ (w \in B ⟼ 1_{𝑜} \times \{w\})) {\underset{˙}{\cdot}}_{f} (b \circ (w \in B ⟼ 1_{𝑜} \times \{w\})) \in \{x \| ψ\}))$
103	102	impcom	$⊢ (φ \land (a \in ran (1_{𝑜} eval R) \land b \in ran (1_{𝑜} eval R))) \to ((a \circ (w \in B ⟼ 1_{𝑜} \times \{w\}) \in \{x \| ψ\} \land b \circ (w \in B ⟼ 1_{𝑜} \times \{w\}) \in \{x \| ψ\}) \to (a \circ (w \in B ⟼ 1_{𝑜} \times \{w\})) {\underset{˙}{\cdot}}_{f} (b \circ (w \in B ⟼ 1_{𝑜} \times \{w\})) \in \{x \| ψ\})$
104	71 74 78 79 79 80 81	ofco	$⊢ (φ \land (a \in ran (1_{𝑜} eval R) \land b \in ran (1_{𝑜} eval R))) \to (a {\underset{˙}{\cdot}}_{f} b) \circ (w \in B ⟼ 1_{𝑜} \times \{w\}) = (a \circ (w \in B ⟼ 1_{𝑜} \times \{w\})) {\underset{˙}{\cdot}}_{f} (b \circ (w \in B ⟼ 1_{𝑜} \times \{w\}))$
105	104	eleq1d	$⊢ (φ \land (a \in ran (1_{𝑜} eval R) \land b \in ran (1_{𝑜} eval R))) \to ((a {\underset{˙}{\cdot}}_{f} b) \circ (w \in B ⟼ 1_{𝑜} \times \{w\}) \in \{x \| ψ\} \leftrightarrow (a \circ (w \in B ⟼ 1_{𝑜} \times \{w\})) {\underset{˙}{\cdot}}_{f} (b \circ (w \in B ⟼ 1_{𝑜} \times \{w\})) \in \{x \| ψ\})$
106	103 105	sylibrd	$⊢ (φ \land (a \in ran (1_{𝑜} eval R) \land b \in ran (1_{𝑜} eval R))) \to ((a \circ (w \in B ⟼ 1_{𝑜} \times \{w\}) \in \{x \| ψ\} \land b \circ (w \in B ⟼ 1_{𝑜} \times \{w\}) \in \{x \| ψ\}) \to (a {\underset{˙}{\cdot}}_{f} b) \circ (w \in B ⟼ 1_{𝑜} \times \{w\}) \in \{x \| ψ\})$
107	106	expimpd	$⊢ φ \to (((a \in ran (1_{𝑜} eval R) \land b \in ran (1_{𝑜} eval R)) \land (a \circ (w \in B ⟼ 1_{𝑜} \times \{w\}) \in \{x \| ψ\} \land b \circ (w \in B ⟼ 1_{𝑜} \times \{w\}) \in \{x \| ψ\})) \to (a {\underset{˙}{\cdot}}_{f} b) \circ (w \in B ⟼ 1_{𝑜} \times \{w\}) \in \{x \| ψ\})$
108	37 107	biimtrid	$⊢ φ \to (((a \in ran (1_{𝑜} eval R) \land a \circ (w \in B ⟼ 1_{𝑜} \times \{w\}) \in \{x \| ψ\}) \land (b \in ran (1_{𝑜} eval R) \land b \circ (w \in B ⟼ 1_{𝑜} \times \{w\}) \in \{x \| ψ\})) \to (a {\underset{˙}{\cdot}}_{f} b) \circ (w \in B ⟼ 1_{𝑜} \times \{w\}) \in \{x \| ψ\})$
109	108	imp	$⊢ (φ \land ((a \in ran (1_{𝑜} eval R) \land a \circ (w \in B ⟼ 1_{𝑜} \times \{w\}) \in \{x \| ψ\}) \land (b \in ran (1_{𝑜} eval R) \land b \circ (w \in B ⟼ 1_{𝑜} \times \{w\}) \in \{x \| ψ\}))) \to (a {\underset{˙}{\cdot}}_{f} b) \circ (w \in B ⟼ 1_{𝑜} \times \{w\}) \in \{x \| ψ\}$
110		coeq1	$⊢ y = (B^{1_{𝑜}}) \times \{a\} \to y \circ (w \in B ⟼ 1_{𝑜} \times \{w\}) = ((B^{1_{𝑜}}) \times \{a\}) \circ (w \in B ⟼ 1_{𝑜} \times \{w\})$
111	110	eleq1d	$⊢ y = (B^{1_{𝑜}}) \times \{a\} \to (y \circ (w \in B ⟼ 1_{𝑜} \times \{w\}) \in \{x \| ψ\} \leftrightarrow ((B^{1_{𝑜}}) \times \{a\}) \circ (w \in B ⟼ 1_{𝑜} \times \{w\}) \in \{x \| ψ\})$
112		coeq1	$⊢ y = (b \in (B^{1_{𝑜}}) ⟼ b (a)) \to y \circ (w \in B ⟼ 1_{𝑜} \times \{w\}) = (b \in (B^{1_{𝑜}}) ⟼ b (a)) \circ (w \in B ⟼ 1_{𝑜} \times \{w\})$
113	112	eleq1d	$⊢ y = (b \in (B^{1_{𝑜}}) ⟼ b (a)) \to (y \circ (w \in B ⟼ 1_{𝑜} \times \{w\}) \in \{x \| ψ\} \leftrightarrow (b \in (B^{1_{𝑜}}) ⟼ b (a)) \circ (w \in B ⟼ 1_{𝑜} \times \{w\}) \in \{x \| ψ\})$
114		coeq1	$⊢ y = a \to y \circ (w \in B ⟼ 1_{𝑜} \times \{w\}) = a \circ (w \in B ⟼ 1_{𝑜} \times \{w\})$
115	114	eleq1d	$⊢ y = a \to (y \circ (w \in B ⟼ 1_{𝑜} \times \{w\}) \in \{x \| ψ\} \leftrightarrow a \circ (w \in B ⟼ 1_{𝑜} \times \{w\}) \in \{x \| ψ\})$
116		coeq1	$⊢ y = b \to y \circ (w \in B ⟼ 1_{𝑜} \times \{w\}) = b \circ (w \in B ⟼ 1_{𝑜} \times \{w\})$
117	116	eleq1d	$⊢ y = b \to (y \circ (w \in B ⟼ 1_{𝑜} \times \{w\}) \in \{x \| ψ\} \leftrightarrow b \circ (w \in B ⟼ 1_{𝑜} \times \{w\}) \in \{x \| ψ\})$
118		coeq1	$⊢ y = a {\underset{˙}{+}}_{f} b \to y \circ (w \in B ⟼ 1_{𝑜} \times \{w\}) = (a {\underset{˙}{+}}_{f} b) \circ (w \in B ⟼ 1_{𝑜} \times \{w\})$
119	118	eleq1d	$⊢ y = a {\underset{˙}{+}}_{f} b \to (y \circ (w \in B ⟼ 1_{𝑜} \times \{w\}) \in \{x \| ψ\} \leftrightarrow (a {\underset{˙}{+}}_{f} b) \circ (w \in B ⟼ 1_{𝑜} \times \{w\}) \in \{x \| ψ\})$
120		coeq1	$⊢ y = a {\underset{˙}{\cdot}}_{f} b \to y \circ (w \in B ⟼ 1_{𝑜} \times \{w\}) = (a {\underset{˙}{\cdot}}_{f} b) \circ (w \in B ⟼ 1_{𝑜} \times \{w\})$
121	120	eleq1d	$⊢ y = a {\underset{˙}{\cdot}}_{f} b \to (y \circ (w \in B ⟼ 1_{𝑜} \times \{w\}) \in \{x \| ψ\} \leftrightarrow (a {\underset{˙}{\cdot}}_{f} b) \circ (w \in B ⟼ 1_{𝑜} \times \{w\}) \in \{x \| ψ\})$
122		coeq1	$⊢ y = A \circ (b \in (B^{1_{𝑜}}) ⟼ b (\emptyset)) \to y \circ (w \in B ⟼ 1_{𝑜} \times \{w\}) = (A \circ (b \in (B^{1_{𝑜}}) ⟼ b (\emptyset))) \circ (w \in B ⟼ 1_{𝑜} \times \{w\})$
123	122	eleq1d	$⊢ y = A \circ (b \in (B^{1_{𝑜}}) ⟼ b (\emptyset)) \to (y \circ (w \in B ⟼ 1_{𝑜} \times \{w\}) \in \{x \| ψ\} \leftrightarrow (A \circ (b \in (B^{1_{𝑜}}) ⟼ b (\emptyset))) \circ (w \in B ⟼ 1_{𝑜} \times \{w\}) \in \{x \| ψ\})$
124	4	pf1rcl	$⊢ A \in Q \to R \in CRing$
125	16 124	syl	$⊢ φ \to R \in CRing$
126	125	adantr	$⊢ (φ \land a \in B) \to R \in CRing$
127		1on	$⊢ 1_{𝑜} \in On$
128		eqid	$⊢ 1_{𝑜} mPoly R = 1_{𝑜} mPoly R$
129	128	mplassa	$⊢ (1_{𝑜} \in On \land R \in CRing) \to 1_{𝑜} mPoly R \in AssAlg$
130	127 125 129	sylancr	$⊢ φ \to 1_{𝑜} mPoly R \in AssAlg$
131		eqid	$⊢ {Poly}_{1} (R) = {Poly}_{1} (R)$
132		eqid	$⊢ algSc ({Poly}_{1} (R)) = algSc ({Poly}_{1} (R))$
133	131 132	ply1ascl	$⊢ algSc ({Poly}_{1} (R)) = algSc (1_{𝑜} mPoly R)$
134		eqid	$⊢ Scalar (1_{𝑜} mPoly R) = Scalar (1_{𝑜} mPoly R)$
135	133 134	asclrhm	$⊢ 1_{𝑜} mPoly R \in AssAlg \to algSc ({Poly}_{1} (R)) \in (Scalar (1_{𝑜} mPoly R) RingHom (1_{𝑜} mPoly R))$
136	130 135	syl	$⊢ φ \to algSc ({Poly}_{1} (R)) \in (Scalar (1_{𝑜} mPoly R) RingHom (1_{𝑜} mPoly R))$
137	127	a1i	$⊢ φ \to 1_{𝑜} \in On$
138	128 137 125	mplsca	$⊢ φ \to R = Scalar (1_{𝑜} mPoly R)$
139	138	oveq1d	$⊢ φ \to R RingHom (1_{𝑜} mPoly R) = Scalar (1_{𝑜} mPoly R) RingHom (1_{𝑜} mPoly R)$
140	136 139	eleqtrrd	$⊢ φ \to algSc ({Poly}_{1} (R)) \in (R RingHom (1_{𝑜} mPoly R))$
141		eqid	$⊢ {Base}_{(1_{𝑜} mPoly R)} = {Base}_{(1_{𝑜} mPoly R)}$
142	1 141	rhmf	$⊢ algSc ({Poly}_{1} (R)) \in (R RingHom (1_{𝑜} mPoly R)) \to algSc ({Poly}_{1} (R)) : B ⟶ {Base}_{(1_{𝑜} mPoly R)}$
143	140 142	syl	$⊢ φ \to algSc ({Poly}_{1} (R)) : B ⟶ {Base}_{(1_{𝑜} mPoly R)}$
144	143	ffvelcdmda	$⊢ (φ \land a \in B) \to algSc ({Poly}_{1} (R)) (a) \in {Base}_{(1_{𝑜} mPoly R)}$
145		eqid	$⊢ {eval}_{1} (R) = {eval}_{1} (R)$
146	145 34 1 128 141	evl1val	$⊢ (R \in CRing \land algSc ({Poly}_{1} (R)) (a) \in {Base}_{(1_{𝑜} mPoly R)}) \to {eval}_{1} (R) (algSc ({Poly}_{1} (R)) (a)) = (1_{𝑜} eval R) (algSc ({Poly}_{1} (R)) (a)) \circ (w \in B ⟼ 1_{𝑜} \times \{w\})$
147	126 144 146	syl2anc	$⊢ (φ \land a \in B) \to {eval}_{1} (R) (algSc ({Poly}_{1} (R)) (a)) = (1_{𝑜} eval R) (algSc ({Poly}_{1} (R)) (a)) \circ (w \in B ⟼ 1_{𝑜} \times \{w\})$
148	145 131 1 132	evl1sca	$⊢ (R \in CRing \land a \in B) \to {eval}_{1} (R) (algSc ({Poly}_{1} (R)) (a)) = B \times \{a\}$
149	125 148	sylan	$⊢ (φ \land a \in B) \to {eval}_{1} (R) (algSc ({Poly}_{1} (R)) (a)) = B \times \{a\}$
150	1	ressid	$⊢ R \in CRing \to R ↾_{𝑠} B = R$
151	126 150	syl	$⊢ (φ \land a \in B) \to R ↾_{𝑠} B = R$
152	151	oveq2d	$⊢ (φ \land a \in B) \to 1_{𝑜} mPoly (R ↾_{𝑠} B) = 1_{𝑜} mPoly R$
153	152	fveq2d	$⊢ (φ \land a \in B) \to algSc (1_{𝑜} mPoly (R ↾_{𝑠} B)) = algSc (1_{𝑜} mPoly R)$
154	153 133	eqtr4di	$⊢ (φ \land a \in B) \to algSc (1_{𝑜} mPoly (R ↾_{𝑠} B)) = algSc ({Poly}_{1} (R))$
155	154	fveq1d	$⊢ (φ \land a \in B) \to algSc (1_{𝑜} mPoly (R ↾_{𝑠} B)) (a) = algSc ({Poly}_{1} (R)) (a)$
156	155	fveq2d	$⊢ (φ \land a \in B) \to (1_{𝑜} eval R) (algSc (1_{𝑜} mPoly (R ↾_{𝑠} B)) (a)) = (1_{𝑜} eval R) (algSc ({Poly}_{1} (R)) (a))$
157		eqid	$⊢ 1_{𝑜} mPoly (R ↾_{𝑠} B) = 1_{𝑜} mPoly (R ↾_{𝑠} B)$
158		eqid	$⊢ R ↾_{𝑠} B = R ↾_{𝑠} B$
159		eqid	$⊢ algSc (1_{𝑜} mPoly (R ↾_{𝑠} B)) = algSc (1_{𝑜} mPoly (R ↾_{𝑠} B))$
160	127	a1i	$⊢ (φ \land a \in B) \to 1_{𝑜} \in On$
161		crngring	$⊢ R \in CRing \to R \in Ring$
162	1	subrgid	$⊢ R \in Ring \to B \in SubRing (R)$
163	125 161 162	3syl	$⊢ φ \to B \in SubRing (R)$
164	163	adantr	$⊢ (φ \land a \in B) \to B \in SubRing (R)$
165		simpr	$⊢ (φ \land a \in B) \to a \in B$
166	35 157 158 1 159 160 126 164 165	evlssca	$⊢ (φ \land a \in B) \to (1_{𝑜} eval R) (algSc (1_{𝑜} mPoly (R ↾_{𝑠} B)) (a)) = (B^{1_{𝑜}}) \times \{a\}$
167	156 166	eqtr3d	$⊢ (φ \land a \in B) \to (1_{𝑜} eval R) (algSc ({Poly}_{1} (R)) (a)) = (B^{1_{𝑜}}) \times \{a\}$
168	167	coeq1d	$⊢ (φ \land a \in B) \to (1_{𝑜} eval R) (algSc ({Poly}_{1} (R)) (a)) \circ (w \in B ⟼ 1_{𝑜} \times \{w\}) = ((B^{1_{𝑜}}) \times \{a\}) \circ (w \in B ⟼ 1_{𝑜} \times \{w\})$
169	147 149 168	3eqtr3d	$⊢ (φ \land a \in B) \to B \times \{a\} = ((B^{1_{𝑜}}) \times \{a\}) \circ (w \in B ⟼ 1_{𝑜} \times \{w\})$
170		vsnex	$⊢ \{f\} \in V$
171	19 170	xpex	$⊢ B \times \{f\} \in V$
172	171 7	elab	$⊢ B \times \{f\} \in \{x \| ψ\} \leftrightarrow χ$
173	14 172	sylibr	$⊢ (φ \land f \in B) \to B \times \{f\} \in \{x \| ψ\}$
174	173	ralrimiva	$⊢ φ \to \forall f \in B B \times \{f\} \in \{x \| ψ\}$
175		sneq	$⊢ f = a \to \{f\} = \{a\}$
176	175	xpeq2d	$⊢ f = a \to B \times \{f\} = B \times \{a\}$
177	176	eleq1d	$⊢ f = a \to (B \times \{f\} \in \{x \| ψ\} \leftrightarrow B \times \{a\} \in \{x \| ψ\})$
178	177	rspccva	$⊢ (\forall f \in B B \times \{f\} \in \{x \| ψ\} \land a \in B) \to B \times \{a\} \in \{x \| ψ\}$
179	174 178	sylan	$⊢ (φ \land a \in B) \to B \times \{a\} \in \{x \| ψ\}$
180	169 179	eqeltrrd	$⊢ (φ \land a \in B) \to ((B^{1_{𝑜}}) \times \{a\}) \circ (w \in B ⟼ 1_{𝑜} \times \{w\}) \in \{x \| ψ\}$
181		resiexg	$⊢ B \in V \to {I ↾}_{B} \in V$
182	19 181	ax-mp	$⊢ {I ↾}_{B} \in V$
183	182 8	elab	$⊢ {I ↾}_{B} \in \{x \| ψ\} \leftrightarrow θ$
184	15 183	sylibr	$⊢ φ \to {I ↾}_{B} \in \{x \| ψ\}$
185	27 184	eqeltrd	$⊢ φ \to (b \in (B^{1_{𝑜}}) ⟼ b (\emptyset)) \circ (w \in B ⟼ 1_{𝑜} \times \{w\}) \in \{x \| ψ\}$
186		el1o	$⊢ a \in 1_{𝑜} \leftrightarrow a = \emptyset$
187		fveq2	$⊢ a = \emptyset \to b (a) = b (\emptyset)$
188	186 187	sylbi	$⊢ a \in 1_{𝑜} \to b (a) = b (\emptyset)$
189	188	mpteq2dv	$⊢ a \in 1_{𝑜} \to (b \in (B^{1_{𝑜}}) ⟼ b (a)) = (b \in (B^{1_{𝑜}}) ⟼ b (\emptyset))$
190	189	coeq1d	$⊢ a \in 1_{𝑜} \to (b \in (B^{1_{𝑜}}) ⟼ b (a)) \circ (w \in B ⟼ 1_{𝑜} \times \{w\}) = (b \in (B^{1_{𝑜}}) ⟼ b (\emptyset)) \circ (w \in B ⟼ 1_{𝑜} \times \{w\})$
191	190	eleq1d	$⊢ a \in 1_{𝑜} \to ((b \in (B^{1_{𝑜}}) ⟼ b (a)) \circ (w \in B ⟼ 1_{𝑜} \times \{w\}) \in \{x \| ψ\} \leftrightarrow (b \in (B^{1_{𝑜}}) ⟼ b (\emptyset)) \circ (w \in B ⟼ 1_{𝑜} \times \{w\}) \in \{x \| ψ\})$
192	185 191	syl5ibrcom	$⊢ φ \to (a \in 1_{𝑜} \to (b \in (B^{1_{𝑜}}) ⟼ b (a)) \circ (w \in B ⟼ 1_{𝑜} \times \{w\}) \in \{x \| ψ\})$
193	192	imp	$⊢ (φ \land a \in 1_{𝑜}) \to (b \in (B^{1_{𝑜}}) ⟼ b (a)) \circ (w \in B ⟼ 1_{𝑜} \times \{w\}) \in \{x \| ψ\}$
194	4 1 38	pf1mpf	$⊢ A \in Q \to A \circ (b \in (B^{1_{𝑜}}) ⟼ b (\emptyset)) \in ran (1_{𝑜} eval R)$
195	16 194	syl	$⊢ φ \to A \circ (b \in (B^{1_{𝑜}}) ⟼ b (\emptyset)) \in ran (1_{𝑜} eval R)$
196	1 2 3 36 87 109 111 113 115 117 119 121 123 180 193 195	mpfind	$⊢ φ \to (A \circ (b \in (B^{1_{𝑜}}) ⟼ b (\emptyset))) \circ (w \in B ⟼ 1_{𝑜} \times \{w\}) \in \{x \| ψ\}$
197	33 196	eqeltrrd	$⊢ φ \to A \in \{x \| ψ\}$
198	13	elabg	$⊢ A \in Q \to (A \in \{x \| ψ\} \leftrightarrow ρ)$
199	16 198	syl	$⊢ φ \to (A \in \{x \| ψ\} \leftrightarrow ρ)$
200	197 199	mpbid	$⊢ φ \to ρ$

Metamath Proof Explorer

Theorem pf1ind

Proof