Theorem linply1

Description: A term of the form x - C is a (univariate) polynomial, also called "linear polynomial". (Part of ply1remlem ). (Contributed by AV, 3-Jul-2019)

	Ref	Expression
Hypotheses	linply1.p	$$⊢P={\mathrm{Poly}}_1\left(R\right)$$
	linply1.b	$$⊢B={\mathrm{Base}}_P$$
	linply1.k	$$⊢K={\mathrm{Base}}_R$$
	linply1.x	$$⊢X={\mathrm{var}}_1\left(R\right)$$
	linply1.m	$$⊢\underset{\dot{}}{-}={-}_P$$
	linply1.a	$$⊢A=\mathrm{algSc}\left(P\right)$$
	linply1.g	$$⊢G=X\underset{\dot{}}{-}A\left(C\right)$$
	linply1.c	$$⊢\phi \to C\in K$$
	linply1.r	$$⊢\phi \to R\in \mathrm{Ring}$$
Assertion	linply1	$$⊢\phi \to G\in B$$

Proof

Step	Hyp	Ref	Expression
1		linply1.p	$$⊢P={\mathrm{Poly}}_1\left(R\right)$$
2		linply1.b	$$⊢B={\mathrm{Base}}_P$$
3		linply1.k	$$⊢K={\mathrm{Base}}_R$$
4		linply1.x	$$⊢X={\mathrm{var}}_1\left(R\right)$$
5		linply1.m	$$⊢\underset{\dot{}}{-}={-}_P$$
6		linply1.a	$$⊢A=\mathrm{algSc}\left(P\right)$$
7		linply1.g	$$⊢G=X\underset{\dot{}}{-}A\left(C\right)$$
8		linply1.c	$$⊢\phi \to C\in K$$
9		linply1.r	$$⊢\phi \to R\in \mathrm{Ring}$$
10	1	ply1ring	$$⊢R\in \mathrm{Ring}\to P\in \mathrm{Ring}$$
11		ringgrp	$$⊢P\in \mathrm{Ring}\to P\in \mathrm{Grp}$$
12	9 10 11	3syl	$$⊢\phi \to P\in \mathrm{Grp}$$
13	4 1 2	vr1cl	$$⊢R\in \mathrm{Ring}\to X\in B$$
14	9 13	syl	$$⊢\phi \to X\in B$$
15	1 6 3 2	ply1sclf	$$⊢R\in \mathrm{Ring}\to A:K⟶B$$
16	9 15	syl	$$⊢\phi \to A:K⟶B$$
17	16 8	ffvelrnd	$$⊢\phi \to A\left(C\right)\in B$$
18	2 5	grpsubcl	$$⊢\left(P\in \mathrm{Grp}\wedge X\in B\wedge A\left(C\right)\in B\right)\to X\underset{\dot{}}{-}A\left(C\right)\in B$$
19	12 14 17 18	syl3anc	$$⊢\phi \to X\underset{\dot{}}{-}A\left(C\right)\in B$$
20	7 19	eqeltrid	$$⊢\phi \to G\in B$$