ply1scltm

Description: A scalar is a term with zero exponent. (Contributed by Stefan O'Rear, 29-Mar-2015)

	Ref	Expression
Hypotheses	ply1scltm.k	$⊢ K = {Base}_{R}$
	ply1scltm.p	$⊢ P = {Poly}_{1} (R)$
	ply1scltm.x	$⊢ X = {var}_{1} (R)$
	ply1scltm.m	$⊢ \underset{˙}{\cdot} = \cdot_{P}$
	ply1scltm.n	$⊢ N = {mulGrp}_{P}$
	ply1scltm.e	$⊢ \underset{˙}{\times} = \cdot_{N}$
	ply1scltm.a	$⊢ A = algSc (P)$
Assertion	ply1scltm	$⊢ (R \in Ring \land F \in K) \to A (F) = F \underset{˙}{\cdot} (0 \underset{˙}{\times} X)$

Step	Hyp	Ref	Expression
1		ply1scltm.k	$⊢ K = {Base}_{R}$
2		ply1scltm.p	$⊢ P = {Poly}_{1} (R)$
3		ply1scltm.x	$⊢ X = {var}_{1} (R)$
4		ply1scltm.m	$⊢ \underset{˙}{\cdot} = \cdot_{P}$
5		ply1scltm.n	$⊢ N = {mulGrp}_{P}$
6		ply1scltm.e	$⊢ \underset{˙}{\times} = \cdot_{N}$
7		ply1scltm.a	$⊢ A = algSc (P)$
8	2	ply1sca2	$⊢ I (R) = Scalar (P)$
9		df-base	$⊢ Base = Slot 1$
10	9 1	strfvi	$⊢ K = {Base}_{I (R)}$
11		eqid	$⊢ 1_{P} = 1_{P}$
12	7 8 10 4 11	asclval	$⊢ F \in K \to A (F) = F \underset{˙}{\cdot} 1_{P}$
13	12	adantl	$⊢ (R \in Ring \land F \in K) \to A (F) = F \underset{˙}{\cdot} 1_{P}$
14		eqid	$⊢ {Base}_{P} = {Base}_{P}$
15	3 2 14	vr1cl	$⊢ R \in Ring \to X \in {Base}_{P}$
16	5 14	mgpbas	$⊢ {Base}_{P} = {Base}_{N}$
17	5 11	ringidval	$⊢ 1_{P} = 0_{N}$
18	16 17 6	mulg0	$⊢ X \in {Base}_{P} \to 0 \underset{˙}{\times} X = 1_{P}$
19	15 18	syl	$⊢ R \in Ring \to 0 \underset{˙}{\times} X = 1_{P}$
20	19	adantr	$⊢ (R \in Ring \land F \in K) \to 0 \underset{˙}{\times} X = 1_{P}$
21	20	oveq2d	$⊢ (R \in Ring \land F \in K) \to F \underset{˙}{\cdot} (0 \underset{˙}{\times} X) = F \underset{˙}{\cdot} 1_{P}$
22	13 21	eqtr4d	$⊢ (R \in Ring \land F \in K) \to A (F) = F \underset{˙}{\cdot} (0 \underset{˙}{\times} X)$

Metamath Proof Explorer