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	⊢ 𝑃 = ( Poly1 ‘ 𝑅 )
	linply1.b	⊢ 𝐵 = ( Base ‘ 𝑃 )
	linply1.k	⊢ 𝐾 = ( Base ‘ 𝑅 )
	linply1.x	⊢ 𝑋 = ( var1 ‘ 𝑅 )
	linply1.m	⊢ − = ( -g ‘ 𝑃 )
	linply1.a	⊢ 𝐴 = ( algSc ‘ 𝑃 )
	linply1.g	⊢ 𝐺 = ( 𝑋 − ( 𝐴 ‘ 𝐶 ) )
	linply1.c	⊢ ( 𝜑 → 𝐶 ∈ 𝐾 )
	linply1.r	⊢ ( 𝜑 → 𝑅 ∈ Ring )
Assertion	linply1	⊢ ( 𝜑 → 𝐺 ∈ 𝐵 )

Proof

Step	Hyp	Ref	Expression
1		linply1.p	⊢ 𝑃 = ( Poly1 ‘ 𝑅 )
2		linply1.b	⊢ 𝐵 = ( Base ‘ 𝑃 )
3		linply1.k	⊢ 𝐾 = ( Base ‘ 𝑅 )
4		linply1.x	⊢ 𝑋 = ( var1 ‘ 𝑅 )
5		linply1.m	⊢ − = ( -g ‘ 𝑃 )
6		linply1.a	⊢ 𝐴 = ( algSc ‘ 𝑃 )
7		linply1.g	⊢ 𝐺 = ( 𝑋 − ( 𝐴 ‘ 𝐶 ) )
8		linply1.c	⊢ ( 𝜑 → 𝐶 ∈ 𝐾 )
9		linply1.r	⊢ ( 𝜑 → 𝑅 ∈ Ring )
10	1	ply1ring	⊢ ( 𝑅 ∈ Ring → 𝑃 ∈ Ring )
11		ringgrp	⊢ ( 𝑃 ∈ Ring → 𝑃 ∈ Grp )
12	9 10 11	3syl	⊢ ( 𝜑 → 𝑃 ∈ Grp )
13	4 1 2	vr1cl	⊢ ( 𝑅 ∈ Ring → 𝑋 ∈ 𝐵 )
14	9 13	syl	⊢ ( 𝜑 → 𝑋 ∈ 𝐵 )
15	1 6 3 2	ply1sclf	⊢ ( 𝑅 ∈ Ring → 𝐴 : 𝐾 ⟶ 𝐵 )
16	9 15	syl	⊢ ( 𝜑 → 𝐴 : 𝐾 ⟶ 𝐵 )
17	16 8	ffvelrnd	⊢ ( 𝜑 → ( 𝐴 ‘ 𝐶 ) ∈ 𝐵 )
18	2 5	grpsubcl	⊢ ( ( 𝑃 ∈ Grp ∧ 𝑋 ∈ 𝐵 ∧ ( 𝐴 ‘ 𝐶 ) ∈ 𝐵 ) → ( 𝑋 − ( 𝐴 ‘ 𝐶 ) ) ∈ 𝐵 )
19	12 14 17 18	syl3anc	⊢ ( 𝜑 → ( 𝑋 − ( 𝐴 ‘ 𝐶 ) ) ∈ 𝐵 )
20	7 19	eqeltrid	⊢ ( 𝜑 → 𝐺 ∈ 𝐵 )