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 = ( Poly1 ` R )
	linply1.b	|- B = ( Base ` P )
	linply1.k	|- K = ( Base ` R )
	linply1.x	|- X = ( var1 ` R )
	linply1.m	|- .- = ( -g ` P )
	linply1.a	|- A = ( algSc ` P )
	linply1.g	|- G = ( X .- ( A ` C ) )
	linply1.c	|- ( ph -> C e. K )
	linply1.r	|- ( ph -> R e. Ring )
Assertion	linply1	|- ( ph -> G e. B )

Proof

Step	Hyp	Ref	Expression
1		linply1.p	|- P = ( Poly1 ` R )
2		linply1.b	|- B = ( Base ` P )
3		linply1.k	|- K = ( Base ` R )
4		linply1.x	|- X = ( var1 ` R )
5		linply1.m	|- .- = ( -g ` P )
6		linply1.a	|- A = ( algSc ` P )
7		linply1.g	|- G = ( X .- ( A ` C ) )
8		linply1.c	|- ( ph -> C e. K )
9		linply1.r	|- ( ph -> R e. Ring )
10	1	ply1ring	|- ( R e. Ring -> P e. Ring )
11		ringgrp	|- ( P e. Ring -> P e. Grp )
12	9 10 11	3syl	|- ( ph -> P e. Grp )
13	4 1 2	vr1cl	|- ( R e. Ring -> X e. B )
14	9 13	syl	|- ( ph -> X e. B )
15	1 6 3 2	ply1sclf	|- ( R e. Ring -> A : K --> B )
16	9 15	syl	|- ( ph -> A : K --> B )
17	16 8	ffvelrnd	|- ( ph -> ( A ` C ) e. B )
18	2 5	grpsubcl	|- ( ( P e. Grp /\ X e. B /\ ( A ` C ) e. B ) -> ( X .- ( A ` C ) ) e. B )
19	12 14 17 18	syl3anc	|- ( ph -> ( X .- ( A ` C ) ) e. B )
20	7 19	eqeltrid	|- ( ph -> G e. B )