cpmatacl - Metamath Proof Explorer

	Metamath Proof Explorer		< Previous Next > Nearby theorems
Mirrors > Home > MPE Home > Th. List > cpmatacl		Structured version Visualization version GIF version

Theorem cpmatacl 22834

Description: The set of all constant polynomial matrices over a ring 𝑅 is closed under addition. (Contributed by AV, 17-Nov-2019.) (Proof shortened by AV, 28-Nov-2019.)

**Hypotheses**
Ref	Expression
cpmatsrngpmat.s	⊢ 𝑆 = (𝑁 ConstPolyMat 𝑅)
cpmatsrngpmat.p	⊢ 𝑃 = (Poly₁‘𝑅)
cpmatsrngpmat.c	⊢ 𝐶 = (𝑁 Mat 𝑃)

**Assertion**
Ref	Expression
cpmatacl	⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) → ∀𝑥 ∈ 𝑆 ∀𝑦 ∈ 𝑆 (𝑥(+_g‘𝐶)𝑦) ∈ 𝑆)

Distinct variable groups: 𝑥,𝑁,𝑦 𝑥,𝑅,𝑦 𝑦,𝑆 Allowed substitution hints: 𝐶(𝑥,𝑦) 𝑃(𝑥,𝑦) 𝑆(𝑥)

Proof of Theorem cpmatacl Dummy variables 𝑖 𝑗 𝑎 𝑏 𝑐 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		cpmatsrngpmat.s	. . . . . 6 ⊢ 𝑆 = (𝑁 ConstPolyMat 𝑅)
2		cpmatsrngpmat.p	. . . . . 6 ⊢ 𝑃 = (Poly₁‘𝑅)
3		cpmatsrngpmat.c	. . . . . 6 ⊢ 𝐶 = (𝑁 Mat 𝑃)
4		eqid 2765	. . . . . 6 ⊢ (Base‘𝐶) = (Base‘𝐶)
5		eqid 2765	. . . . . 6 ⊢ (Base‘𝑅) = (Base‘𝑅)
6		eqid 2765	. . . . . 6 ⊢ (algSc‘𝑃) = (algSc‘𝑃)
7	1, 2, 3, 4, 5, 6	cpmatelimp2 22832	. . . . 5 ⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) → (𝑥 ∈ 𝑆 → (𝑥 ∈ (Base‘𝐶) ∧ ∀𝑖 ∈ 𝑁 ∀𝑗 ∈ 𝑁 ∃𝑎 ∈ (Base‘𝑅)(𝑖𝑥𝑗) = ((algSc‘𝑃)‘𝑎))))
8	1, 2, 3, 4, 5, 6	cpmatelimp2 22832	. . . . . . 7 ⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) → (𝑦 ∈ 𝑆 → (𝑦 ∈ (Base‘𝐶) ∧ ∀𝑖 ∈ 𝑁 ∀𝑗 ∈ 𝑁 ∃𝑏 ∈ (Base‘𝑅)(𝑖𝑦𝑗) = ((algSc‘𝑃)‘𝑏))))
9		r19.26-2 3150	. . . . . . . . . . . . . 14 ⊢ (∀𝑖 ∈ 𝑁 ∀𝑗 ∈ 𝑁 (∃𝑎 ∈ (Base‘𝑅)(𝑖𝑥𝑗) = ((algSc‘𝑃)‘𝑎) ∧ ∃𝑏 ∈ (Base‘𝑅)(𝑖𝑦𝑗) = ((algSc‘𝑃)‘𝑏)) ↔ (∀𝑖 ∈ 𝑁 ∀𝑗 ∈ 𝑁 ∃𝑎 ∈ (Base‘𝑅)(𝑖𝑥𝑗) = ((algSc‘𝑃)‘𝑎) ∧ ∀𝑖 ∈ 𝑁 ∀𝑗 ∈ 𝑁 ∃𝑏 ∈ (Base‘𝑅)(𝑖𝑦𝑗) = ((algSc‘𝑃)‘𝑏)))
10		eqid 2765	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (+_g‘𝑅) = (+_g‘𝑅)
11	5, 10	ringacl 20352	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((𝑅 ∈ Ring ∧ 𝑎 ∈ (Base‘𝑅) ∧ 𝑏 ∈ (Base‘𝑅)) → (𝑎(+_g‘𝑅)𝑏) ∈ (Base‘𝑅))
12	11	3expb 1136	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((𝑅 ∈ Ring ∧ (𝑎 ∈ (Base‘𝑅) ∧ 𝑏 ∈ (Base‘𝑅))) → (𝑎(+_g‘𝑅)𝑏) ∈ (Base‘𝑅))
13	2	ply1sca 22372	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ (𝑅 ∈ Ring → 𝑅 = (Scalar‘𝑃))
14	13	eqcomd 2771	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (𝑅 ∈ Ring → (Scalar‘𝑃) = 𝑅)
15	14	fveq2d 6875	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (𝑅 ∈ Ring → (+_g‘(Scalar‘𝑃)) = (+_g‘𝑅))
16	15	oveqd 7417	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (𝑅 ∈ Ring → (𝑎(+_g‘(Scalar‘𝑃))𝑏) = (𝑎(+_g‘𝑅)𝑏))
17	16	eleq1d 2850	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝑅 ∈ Ring → ((𝑎(+_g‘(Scalar‘𝑃))𝑏) ∈ (Base‘𝑅) ↔ (𝑎(+_g‘𝑅)𝑏) ∈ (Base‘𝑅)))
18	17	adantr 485	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((𝑅 ∈ Ring ∧ (𝑎 ∈ (Base‘𝑅) ∧ 𝑏 ∈ (Base‘𝑅))) → ((𝑎(+_g‘(Scalar‘𝑃))𝑏) ∈ (Base‘𝑅) ↔ (𝑎(+_g‘𝑅)𝑏) ∈ (Base‘𝑅)))
19	12, 18	mpbird 260	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝑅 ∈ Ring ∧ (𝑎 ∈ (Base‘𝑅) ∧ 𝑏 ∈ (Base‘𝑅))) → (𝑎(+_g‘(Scalar‘𝑃))𝑏) ∈ (Base‘𝑅))
20	19	ad5ant25 773	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) ∧ (𝑦 ∈ (Base‘𝐶) ∧ 𝑥 ∈ (Base‘𝐶))) ∧ (𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁)) ∧ (𝑎 ∈ (Base‘𝑅) ∧ 𝑏 ∈ (Base‘𝑅))) → (𝑎(+_g‘(Scalar‘𝑃))𝑏) ∈ (Base‘𝑅))
21	20	adantr 485	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((((((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) ∧ (𝑦 ∈ (Base‘𝐶) ∧ 𝑥 ∈ (Base‘𝐶))) ∧ (𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁)) ∧ (𝑎 ∈ (Base‘𝑅) ∧ 𝑏 ∈ (Base‘𝑅))) ∧ ((𝑖𝑦𝑗) = ((algSc‘𝑃)‘𝑏) ∧ (𝑖𝑥𝑗) = ((algSc‘𝑃)‘𝑎))) → (𝑎(+_g‘(Scalar‘𝑃))𝑏) ∈ (Base‘𝑅))
22		fveq2 6871	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑐 = (𝑎(+_g‘(Scalar‘𝑃))𝑏) → ((algSc‘𝑃)‘𝑐) = ((algSc‘𝑃)‘(𝑎(+_g‘(Scalar‘𝑃))𝑏)))
23	22	eqeq2d 2776	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑐 = (𝑎(+_g‘(Scalar‘𝑃))𝑏) → ((𝑖(𝑥(+_g‘𝐶)𝑦)𝑗) = ((algSc‘𝑃)‘𝑐) ↔ (𝑖(𝑥(+_g‘𝐶)𝑦)𝑗) = ((algSc‘𝑃)‘(𝑎(+_g‘(Scalar‘𝑃))𝑏))))
24	23	adantl 486	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((((((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) ∧ (𝑦 ∈ (Base‘𝐶) ∧ 𝑥 ∈ (Base‘𝐶))) ∧ (𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁)) ∧ (𝑎 ∈ (Base‘𝑅) ∧ 𝑏 ∈ (Base‘𝑅))) ∧ ((𝑖𝑦𝑗) = ((algSc‘𝑃)‘𝑏) ∧ (𝑖𝑥𝑗) = ((algSc‘𝑃)‘𝑎))) ∧ 𝑐 = (𝑎(+_g‘(Scalar‘𝑃))𝑏)) → ((𝑖(𝑥(+_g‘𝐶)𝑦)𝑗) = ((algSc‘𝑃)‘𝑐) ↔ (𝑖(𝑥(+_g‘𝐶)𝑦)𝑗) = ((algSc‘𝑃)‘(𝑎(+_g‘(Scalar‘𝑃))𝑏))))
25		simpr 489	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) ∧ (𝑦 ∈ (Base‘𝐶) ∧ 𝑥 ∈ (Base‘𝐶))) → (𝑦 ∈ (Base‘𝐶) ∧ 𝑥 ∈ (Base‘𝐶)))
26	25	ancomd 466	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) ∧ (𝑦 ∈ (Base‘𝐶) ∧ 𝑥 ∈ (Base‘𝐶))) → (𝑥 ∈ (Base‘𝐶) ∧ 𝑦 ∈ (Base‘𝐶)))
27	26	anim1i 626	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) ∧ (𝑦 ∈ (Base‘𝐶) ∧ 𝑥 ∈ (Base‘𝐶))) ∧ (𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁)) → ((𝑥 ∈ (Base‘𝐶) ∧ 𝑦 ∈ (Base‘𝐶)) ∧ (𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁)))
28	27	ad2antrr 738	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((((((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) ∧ (𝑦 ∈ (Base‘𝐶) ∧ 𝑥 ∈ (Base‘𝐶))) ∧ (𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁)) ∧ (𝑎 ∈ (Base‘𝑅) ∧ 𝑏 ∈ (Base‘𝑅))) ∧ ((𝑖𝑦𝑗) = ((algSc‘𝑃)‘𝑏) ∧ (𝑖𝑥𝑗) = ((algSc‘𝑃)‘𝑎))) → ((𝑥 ∈ (Base‘𝐶) ∧ 𝑦 ∈ (Base‘𝐶)) ∧ (𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁)))
29		eqid 2765	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (+_g‘𝐶) = (+_g‘𝐶)
30		eqid 2765	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (+_g‘𝑃) = (+_g‘𝑃)
31	3, 4, 29, 30	matplusgcell 22551	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((𝑥 ∈ (Base‘𝐶) ∧ 𝑦 ∈ (Base‘𝐶)) ∧ (𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁)) → (𝑖(𝑥(+_g‘𝐶)𝑦)𝑗) = ((𝑖𝑥𝑗)(+_g‘𝑃)(𝑖𝑦𝑗)))
32	28, 31	syl 18	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((((((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) ∧ (𝑦 ∈ (Base‘𝐶) ∧ 𝑥 ∈ (Base‘𝐶))) ∧ (𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁)) ∧ (𝑎 ∈ (Base‘𝑅) ∧ 𝑏 ∈ (Base‘𝑅))) ∧ ((𝑖𝑦𝑗) = ((algSc‘𝑃)‘𝑏) ∧ (𝑖𝑥𝑗) = ((algSc‘𝑃)‘𝑎))) → (𝑖(𝑥(+_g‘𝐶)𝑦)𝑗) = ((𝑖𝑥𝑗)(+_g‘𝑃)(𝑖𝑦𝑗)))
33		oveq12 7409	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (((𝑖𝑥𝑗) = ((algSc‘𝑃)‘𝑎) ∧ (𝑖𝑦𝑗) = ((algSc‘𝑃)‘𝑏)) → ((𝑖𝑥𝑗)(+_g‘𝑃)(𝑖𝑦𝑗)) = (((algSc‘𝑃)‘𝑎)(+_g‘𝑃)((algSc‘𝑃)‘𝑏)))
34	33	ancoms 463	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((𝑖𝑦𝑗) = ((algSc‘𝑃)‘𝑏) ∧ (𝑖𝑥𝑗) = ((algSc‘𝑃)‘𝑎)) → ((𝑖𝑥𝑗)(+_g‘𝑃)(𝑖𝑦𝑗)) = (((algSc‘𝑃)‘𝑎)(+_g‘𝑃)((algSc‘𝑃)‘𝑏)))
35		eqid 2765	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (Scalar‘𝑃) = (Scalar‘𝑃)
36	2	ply1ring 22367	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (𝑅 ∈ Ring → 𝑃 ∈ Ring)
37	36	ad4antlr 745	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (((((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) ∧ (𝑦 ∈ (Base‘𝐶) ∧ 𝑥 ∈ (Base‘𝐶))) ∧ (𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁)) ∧ (𝑎 ∈ (Base‘𝑅) ∧ 𝑏 ∈ (Base‘𝑅))) → 𝑃 ∈ Ring)
38	2	ply1lmod 22371	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (𝑅 ∈ Ring → 𝑃 ∈ LMod)
39	38	ad4antlr 745	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (((((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) ∧ (𝑦 ∈ (Base‘𝐶) ∧ 𝑥 ∈ (Base‘𝐶))) ∧ (𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁)) ∧ (𝑎 ∈ (Base‘𝑅) ∧ 𝑏 ∈ (Base‘𝑅))) → 𝑃 ∈ LMod)
40	6, 35, 37, 39	asclghm 21992	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (((((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) ∧ (𝑦 ∈ (Base‘𝐶) ∧ 𝑥 ∈ (Base‘𝐶))) ∧ (𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁)) ∧ (𝑎 ∈ (Base‘𝑅) ∧ 𝑏 ∈ (Base‘𝑅))) → (algSc‘𝑃) ∈ ((Scalar‘𝑃) GrpHom 𝑃))
41	13	adantl 486	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) → 𝑅 = (Scalar‘𝑃))
42	41	fveq2d 6875	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) → (Base‘𝑅) = (Base‘(Scalar‘𝑃)))
43	42	eleq2d 2851	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) → (𝑎 ∈ (Base‘𝑅) ↔ 𝑎 ∈ (Base‘(Scalar‘𝑃))))
44	43	biimpd 232	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) → (𝑎 ∈ (Base‘𝑅) → 𝑎 ∈ (Base‘(Scalar‘𝑃))))
45	44	ad2antrr 738	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ ((((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) ∧ (𝑦 ∈ (Base‘𝐶) ∧ 𝑥 ∈ (Base‘𝐶))) ∧ (𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁)) → (𝑎 ∈ (Base‘𝑅) → 𝑎 ∈ (Base‘(Scalar‘𝑃))))
46	45	adantrd 496	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) ∧ (𝑦 ∈ (Base‘𝐶) ∧ 𝑥 ∈ (Base‘𝐶))) ∧ (𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁)) → ((𝑎 ∈ (Base‘𝑅) ∧ 𝑏 ∈ (Base‘𝑅)) → 𝑎 ∈ (Base‘(Scalar‘𝑃))))
47	46	imp 411	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (((((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) ∧ (𝑦 ∈ (Base‘𝐶) ∧ 𝑥 ∈ (Base‘𝐶))) ∧ (𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁)) ∧ (𝑎 ∈ (Base‘𝑅) ∧ 𝑏 ∈ (Base‘𝑅))) → 𝑎 ∈ (Base‘(Scalar‘𝑃)))
48	13	ad3antlr 743	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ ((((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) ∧ (𝑦 ∈ (Base‘𝐶) ∧ 𝑥 ∈ (Base‘𝐶))) ∧ (𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁)) → 𝑅 = (Scalar‘𝑃))
49	48	fveq2d 6875	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ ((((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) ∧ (𝑦 ∈ (Base‘𝐶) ∧ 𝑥 ∈ (Base‘𝐶))) ∧ (𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁)) → (Base‘𝑅) = (Base‘(Scalar‘𝑃)))
50	49	eleq2d 2851	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ ((((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) ∧ (𝑦 ∈ (Base‘𝐶) ∧ 𝑥 ∈ (Base‘𝐶))) ∧ (𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁)) → (𝑏 ∈ (Base‘𝑅) ↔ 𝑏 ∈ (Base‘(Scalar‘𝑃))))
51	50	biimpd 232	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ ((((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) ∧ (𝑦 ∈ (Base‘𝐶) ∧ 𝑥 ∈ (Base‘𝐶))) ∧ (𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁)) → (𝑏 ∈ (Base‘𝑅) → 𝑏 ∈ (Base‘(Scalar‘𝑃))))
52	51	adantld 495	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) ∧ (𝑦 ∈ (Base‘𝐶) ∧ 𝑥 ∈ (Base‘𝐶))) ∧ (𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁)) → ((𝑎 ∈ (Base‘𝑅) ∧ 𝑏 ∈ (Base‘𝑅)) → 𝑏 ∈ (Base‘(Scalar‘𝑃))))
53	52	imp 411	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (((((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) ∧ (𝑦 ∈ (Base‘𝐶) ∧ 𝑥 ∈ (Base‘𝐶))) ∧ (𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁)) ∧ (𝑎 ∈ (Base‘𝑅) ∧ 𝑏 ∈ (Base‘𝑅))) → 𝑏 ∈ (Base‘(Scalar‘𝑃)))
54		eqid 2765	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (Base‘(Scalar‘𝑃)) = (Base‘(Scalar‘𝑃))
55		eqid 2765	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (+_g‘(Scalar‘𝑃)) = (+_g‘(Scalar‘𝑃))
56	54, 55, 30	ghmlin 19282	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (((algSc‘𝑃) ∈ ((Scalar‘𝑃) GrpHom 𝑃) ∧ 𝑎 ∈ (Base‘(Scalar‘𝑃)) ∧ 𝑏 ∈ (Base‘(Scalar‘𝑃))) → ((algSc‘𝑃)‘(𝑎(+_g‘(Scalar‘𝑃))𝑏)) = (((algSc‘𝑃)‘𝑎)(+_g‘𝑃)((algSc‘𝑃)‘𝑏)))
57	40, 47, 53, 56	syl3anc 1394	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (((((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) ∧ (𝑦 ∈ (Base‘𝐶) ∧ 𝑥 ∈ (Base‘𝐶))) ∧ (𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁)) ∧ (𝑎 ∈ (Base‘𝑅) ∧ 𝑏 ∈ (Base‘𝑅))) → ((algSc‘𝑃)‘(𝑎(+_g‘(Scalar‘𝑃))𝑏)) = (((algSc‘𝑃)‘𝑎)(+_g‘𝑃)((algSc‘𝑃)‘𝑏)))
58	57	eqcomd 2771	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) ∧ (𝑦 ∈ (Base‘𝐶) ∧ 𝑥 ∈ (Base‘𝐶))) ∧ (𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁)) ∧ (𝑎 ∈ (Base‘𝑅) ∧ 𝑏 ∈ (Base‘𝑅))) → (((algSc‘𝑃)‘𝑎)(+_g‘𝑃)((algSc‘𝑃)‘𝑏)) = ((algSc‘𝑃)‘(𝑎(+_g‘(Scalar‘𝑃))𝑏)))
59	34, 58	sylan9eqr 2822	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((((((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) ∧ (𝑦 ∈ (Base‘𝐶) ∧ 𝑥 ∈ (Base‘𝐶))) ∧ (𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁)) ∧ (𝑎 ∈ (Base‘𝑅) ∧ 𝑏 ∈ (Base‘𝑅))) ∧ ((𝑖𝑦𝑗) = ((algSc‘𝑃)‘𝑏) ∧ (𝑖𝑥𝑗) = ((algSc‘𝑃)‘𝑎))) → ((𝑖𝑥𝑗)(+_g‘𝑃)(𝑖𝑦𝑗)) = ((algSc‘𝑃)‘(𝑎(+_g‘(Scalar‘𝑃))𝑏)))
60	32, 59	eqtrd 2800	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((((((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) ∧ (𝑦 ∈ (Base‘𝐶) ∧ 𝑥 ∈ (Base‘𝐶))) ∧ (𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁)) ∧ (𝑎 ∈ (Base‘𝑅) ∧ 𝑏 ∈ (Base‘𝑅))) ∧ ((𝑖𝑦𝑗) = ((algSc‘𝑃)‘𝑏) ∧ (𝑖𝑥𝑗) = ((algSc‘𝑃)‘𝑎))) → (𝑖(𝑥(+_g‘𝐶)𝑦)𝑗) = ((algSc‘𝑃)‘(𝑎(+_g‘(Scalar‘𝑃))𝑏)))
61	21, 24, 60	rspcedvd 3586	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) ∧ (𝑦 ∈ (Base‘𝐶) ∧ 𝑥 ∈ (Base‘𝐶))) ∧ (𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁)) ∧ (𝑎 ∈ (Base‘𝑅) ∧ 𝑏 ∈ (Base‘𝑅))) ∧ ((𝑖𝑦𝑗) = ((algSc‘𝑃)‘𝑏) ∧ (𝑖𝑥𝑗) = ((algSc‘𝑃)‘𝑎))) → ∃𝑐 ∈ (Base‘𝑅)(𝑖(𝑥(+_g‘𝐶)𝑦)𝑗) = ((algSc‘𝑃)‘𝑐))
62	61	exp32 425	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) ∧ (𝑦 ∈ (Base‘𝐶) ∧ 𝑥 ∈ (Base‘𝐶))) ∧ (𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁)) ∧ (𝑎 ∈ (Base‘𝑅) ∧ 𝑏 ∈ (Base‘𝑅))) → ((𝑖𝑦𝑗) = ((algSc‘𝑃)‘𝑏) → ((𝑖𝑥𝑗) = ((algSc‘𝑃)‘𝑎) → ∃𝑐 ∈ (Base‘𝑅)(𝑖(𝑥(+_g‘𝐶)𝑦)𝑗) = ((algSc‘𝑃)‘𝑐))))
63	62	anassrs 472	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) ∧ (𝑦 ∈ (Base‘𝐶) ∧ 𝑥 ∈ (Base‘𝐶))) ∧ (𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁)) ∧ 𝑎 ∈ (Base‘𝑅)) ∧ 𝑏 ∈ (Base‘𝑅)) → ((𝑖𝑦𝑗) = ((algSc‘𝑃)‘𝑏) → ((𝑖𝑥𝑗) = ((algSc‘𝑃)‘𝑎) → ∃𝑐 ∈ (Base‘𝑅)(𝑖(𝑥(+_g‘𝐶)𝑦)𝑗) = ((algSc‘𝑃)‘𝑐))))
64	63	rexlimdva 3166	. . . . . . . . . . . . . . . . . 18 ⊢ (((((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) ∧ (𝑦 ∈ (Base‘𝐶) ∧ 𝑥 ∈ (Base‘𝐶))) ∧ (𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁)) ∧ 𝑎 ∈ (Base‘𝑅)) → (∃𝑏 ∈ (Base‘𝑅)(𝑖𝑦𝑗) = ((algSc‘𝑃)‘𝑏) → ((𝑖𝑥𝑗) = ((algSc‘𝑃)‘𝑎) → ∃𝑐 ∈ (Base‘𝑅)(𝑖(𝑥(+_g‘𝐶)𝑦)𝑗) = ((algSc‘𝑃)‘𝑐))))
65	64	com23 87	. . . . . . . . . . . . . . . . 17 ⊢ (((((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) ∧ (𝑦 ∈ (Base‘𝐶) ∧ 𝑥 ∈ (Base‘𝐶))) ∧ (𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁)) ∧ 𝑎 ∈ (Base‘𝑅)) → ((𝑖𝑥𝑗) = ((algSc‘𝑃)‘𝑎) → (∃𝑏 ∈ (Base‘𝑅)(𝑖𝑦𝑗) = ((algSc‘𝑃)‘𝑏) → ∃𝑐 ∈ (Base‘𝑅)(𝑖(𝑥(+_g‘𝐶)𝑦)𝑗) = ((algSc‘𝑃)‘𝑐))))
66	65	rexlimdva 3166	. . . . . . . . . . . . . . . 16 ⊢ ((((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) ∧ (𝑦 ∈ (Base‘𝐶) ∧ 𝑥 ∈ (Base‘𝐶))) ∧ (𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁)) → (∃𝑎 ∈ (Base‘𝑅)(𝑖𝑥𝑗) = ((algSc‘𝑃)‘𝑎) → (∃𝑏 ∈ (Base‘𝑅)(𝑖𝑦𝑗) = ((algSc‘𝑃)‘𝑏) → ∃𝑐 ∈ (Base‘𝑅)(𝑖(𝑥(+_g‘𝐶)𝑦)𝑗) = ((algSc‘𝑃)‘𝑐))))
67	66	impd 415	. . . . . . . . . . . . . . 15 ⊢ ((((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) ∧ (𝑦 ∈ (Base‘𝐶) ∧ 𝑥 ∈ (Base‘𝐶))) ∧ (𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁)) → ((∃𝑎 ∈ (Base‘𝑅)(𝑖𝑥𝑗) = ((algSc‘𝑃)‘𝑎) ∧ ∃𝑏 ∈ (Base‘𝑅)(𝑖𝑦𝑗) = ((algSc‘𝑃)‘𝑏)) → ∃𝑐 ∈ (Base‘𝑅)(𝑖(𝑥(+_g‘𝐶)𝑦)𝑗) = ((algSc‘𝑃)‘𝑐)))
68	67	ralimdvva 3212	. . . . . . . . . . . . . 14 ⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) ∧ (𝑦 ∈ (Base‘𝐶) ∧ 𝑥 ∈ (Base‘𝐶))) → (∀𝑖 ∈ 𝑁 ∀𝑗 ∈ 𝑁 (∃𝑎 ∈ (Base‘𝑅)(𝑖𝑥𝑗) = ((algSc‘𝑃)‘𝑎) ∧ ∃𝑏 ∈ (Base‘𝑅)(𝑖𝑦𝑗) = ((algSc‘𝑃)‘𝑏)) → ∀𝑖 ∈ 𝑁 ∀𝑗 ∈ 𝑁 ∃𝑐 ∈ (Base‘𝑅)(𝑖(𝑥(+_g‘𝐶)𝑦)𝑗) = ((algSc‘𝑃)‘𝑐)))
69	9, 68	biimtrrid 246	. . . . . . . . . . . . 13 ⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) ∧ (𝑦 ∈ (Base‘𝐶) ∧ 𝑥 ∈ (Base‘𝐶))) → ((∀𝑖 ∈ 𝑁 ∀𝑗 ∈ 𝑁 ∃𝑎 ∈ (Base‘𝑅)(𝑖𝑥𝑗) = ((algSc‘𝑃)‘𝑎) ∧ ∀𝑖 ∈ 𝑁 ∀𝑗 ∈ 𝑁 ∃𝑏 ∈ (Base‘𝑅)(𝑖𝑦𝑗) = ((algSc‘𝑃)‘𝑏)) → ∀𝑖 ∈ 𝑁 ∀𝑗 ∈ 𝑁 ∃𝑐 ∈ (Base‘𝑅)(𝑖(𝑥(+_g‘𝐶)𝑦)𝑗) = ((algSc‘𝑃)‘𝑐)))
70	69	expd 420	. . . . . . . . . . . 12 ⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) ∧ (𝑦 ∈ (Base‘𝐶) ∧ 𝑥 ∈ (Base‘𝐶))) → (∀𝑖 ∈ 𝑁 ∀𝑗 ∈ 𝑁 ∃𝑎 ∈ (Base‘𝑅)(𝑖𝑥𝑗) = ((algSc‘𝑃)‘𝑎) → (∀𝑖 ∈ 𝑁 ∀𝑗 ∈ 𝑁 ∃𝑏 ∈ (Base‘𝑅)(𝑖𝑦𝑗) = ((algSc‘𝑃)‘𝑏) → ∀𝑖 ∈ 𝑁 ∀𝑗 ∈ 𝑁 ∃𝑐 ∈ (Base‘𝑅)(𝑖(𝑥(+_g‘𝐶)𝑦)𝑗) = ((algSc‘𝑃)‘𝑐))))
71	70	expr 461	. . . . . . . . . . 11 ⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) ∧ 𝑦 ∈ (Base‘𝐶)) → (𝑥 ∈ (Base‘𝐶) → (∀𝑖 ∈ 𝑁 ∀𝑗 ∈ 𝑁 ∃𝑎 ∈ (Base‘𝑅)(𝑖𝑥𝑗) = ((algSc‘𝑃)‘𝑎) → (∀𝑖 ∈ 𝑁 ∀𝑗 ∈ 𝑁 ∃𝑏 ∈ (Base‘𝑅)(𝑖𝑦𝑗) = ((algSc‘𝑃)‘𝑏) → ∀𝑖 ∈ 𝑁 ∀𝑗 ∈ 𝑁 ∃𝑐 ∈ (Base‘𝑅)(𝑖(𝑥(+_g‘𝐶)𝑦)𝑗) = ((algSc‘𝑃)‘𝑐)))))
72	71	impd 415	. . . . . . . . . 10 ⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) ∧ 𝑦 ∈ (Base‘𝐶)) → ((𝑥 ∈ (Base‘𝐶) ∧ ∀𝑖 ∈ 𝑁 ∀𝑗 ∈ 𝑁 ∃𝑎 ∈ (Base‘𝑅)(𝑖𝑥𝑗) = ((algSc‘𝑃)‘𝑎)) → (∀𝑖 ∈ 𝑁 ∀𝑗 ∈ 𝑁 ∃𝑏 ∈ (Base‘𝑅)(𝑖𝑦𝑗) = ((algSc‘𝑃)‘𝑏) → ∀𝑖 ∈ 𝑁 ∀𝑗 ∈ 𝑁 ∃𝑐 ∈ (Base‘𝑅)(𝑖(𝑥(+_g‘𝐶)𝑦)𝑗) = ((algSc‘𝑃)‘𝑐))))
73	72	ex 417	. . . . . . . . 9 ⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) → (𝑦 ∈ (Base‘𝐶) → ((𝑥 ∈ (Base‘𝐶) ∧ ∀𝑖 ∈ 𝑁 ∀𝑗 ∈ 𝑁 ∃𝑎 ∈ (Base‘𝑅)(𝑖𝑥𝑗) = ((algSc‘𝑃)‘𝑎)) → (∀𝑖 ∈ 𝑁 ∀𝑗 ∈ 𝑁 ∃𝑏 ∈ (Base‘𝑅)(𝑖𝑦𝑗) = ((algSc‘𝑃)‘𝑏) → ∀𝑖 ∈ 𝑁 ∀𝑗 ∈ 𝑁 ∃𝑐 ∈ (Base‘𝑅)(𝑖(𝑥(+_g‘𝐶)𝑦)𝑗) = ((algSc‘𝑃)‘𝑐)))))
74	73	com34 92	. . . . . . . 8 ⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) → (𝑦 ∈ (Base‘𝐶) → (∀𝑖 ∈ 𝑁 ∀𝑗 ∈ 𝑁 ∃𝑏 ∈ (Base‘𝑅)(𝑖𝑦𝑗) = ((algSc‘𝑃)‘𝑏) → ((𝑥 ∈ (Base‘𝐶) ∧ ∀𝑖 ∈ 𝑁 ∀𝑗 ∈ 𝑁 ∃𝑎 ∈ (Base‘𝑅)(𝑖𝑥𝑗) = ((algSc‘𝑃)‘𝑎)) → ∀𝑖 ∈ 𝑁 ∀𝑗 ∈ 𝑁 ∃𝑐 ∈ (Base‘𝑅)(𝑖(𝑥(+_g‘𝐶)𝑦)𝑗) = ((algSc‘𝑃)‘𝑐)))))
75	74	impd 415	. . . . . . 7 ⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) → ((𝑦 ∈ (Base‘𝐶) ∧ ∀𝑖 ∈ 𝑁 ∀𝑗 ∈ 𝑁 ∃𝑏 ∈ (Base‘𝑅)(𝑖𝑦𝑗) = ((algSc‘𝑃)‘𝑏)) → ((𝑥 ∈ (Base‘𝐶) ∧ ∀𝑖 ∈ 𝑁 ∀𝑗 ∈ 𝑁 ∃𝑎 ∈ (Base‘𝑅)(𝑖𝑥𝑗) = ((algSc‘𝑃)‘𝑎)) → ∀𝑖 ∈ 𝑁 ∀𝑗 ∈ 𝑁 ∃𝑐 ∈ (Base‘𝑅)(𝑖(𝑥(+_g‘𝐶)𝑦)𝑗) = ((algSc‘𝑃)‘𝑐))))
76	8, 75	syld 48	. . . . . 6 ⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) → (𝑦 ∈ 𝑆 → ((𝑥 ∈ (Base‘𝐶) ∧ ∀𝑖 ∈ 𝑁 ∀𝑗 ∈ 𝑁 ∃𝑎 ∈ (Base‘𝑅)(𝑖𝑥𝑗) = ((algSc‘𝑃)‘𝑎)) → ∀𝑖 ∈ 𝑁 ∀𝑗 ∈ 𝑁 ∃𝑐 ∈ (Base‘𝑅)(𝑖(𝑥(+_g‘𝐶)𝑦)𝑗) = ((algSc‘𝑃)‘𝑐))))
77	76	com23 87	. . . . 5 ⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) → ((𝑥 ∈ (Base‘𝐶) ∧ ∀𝑖 ∈ 𝑁 ∀𝑗 ∈ 𝑁 ∃𝑎 ∈ (Base‘𝑅)(𝑖𝑥𝑗) = ((algSc‘𝑃)‘𝑎)) → (𝑦 ∈ 𝑆 → ∀𝑖 ∈ 𝑁 ∀𝑗 ∈ 𝑁 ∃𝑐 ∈ (Base‘𝑅)(𝑖(𝑥(+_g‘𝐶)𝑦)𝑗) = ((algSc‘𝑃)‘𝑐))))
78	7, 77	syld 48	. . . 4 ⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) → (𝑥 ∈ 𝑆 → (𝑦 ∈ 𝑆 → ∀𝑖 ∈ 𝑁 ∀𝑗 ∈ 𝑁 ∃𝑐 ∈ (Base‘𝑅)(𝑖(𝑥(+_g‘𝐶)𝑦)𝑗) = ((algSc‘𝑃)‘𝑐))))
79	78	imp32 423	. . 3 ⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) ∧ (𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆)) → ∀𝑖 ∈ 𝑁 ∀𝑗 ∈ 𝑁 ∃𝑐 ∈ (Base‘𝑅)(𝑖(𝑥(+_g‘𝐶)𝑦)𝑗) = ((algSc‘𝑃)‘𝑐))
80		simpl 487	. . . . 5 ⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) → 𝑁 ∈ Fin)
81	80	adantr 485	. . . 4 ⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) ∧ (𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆)) → 𝑁 ∈ Fin)
82		simpr 489	. . . . 5 ⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) → 𝑅 ∈ Ring)
83	82	adantr 485	. . . 4 ⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) ∧ (𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆)) → 𝑅 ∈ Ring)
84	2, 3	pmatring 22810	. . . . . 6 ⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) → 𝐶 ∈ Ring)
85	84	adantr 485	. . . . 5 ⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) ∧ (𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆)) → 𝐶 ∈ Ring)
86		simpl 487	. . . . . . . 8 ⊢ ((𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆) → 𝑥 ∈ 𝑆)
87	86	anim2i 628	. . . . . . 7 ⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) ∧ (𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆)) → ((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) ∧ 𝑥 ∈ 𝑆))
88		df-3an 1103	. . . . . . 7 ⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑥 ∈ 𝑆) ↔ ((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) ∧ 𝑥 ∈ 𝑆))
89	87, 88	sylibr 237	. . . . . 6 ⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) ∧ (𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆)) → (𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑥 ∈ 𝑆))
90	1, 2, 3, 4	cpmatpmat 22828	. . . . . 6 ⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑥 ∈ 𝑆) → 𝑥 ∈ (Base‘𝐶))
91	89, 90	syl 18	. . . . 5 ⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) ∧ (𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆)) → 𝑥 ∈ (Base‘𝐶))
92		simpr 489	. . . . . . . 8 ⊢ ((𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆) → 𝑦 ∈ 𝑆)
93	92	anim2i 628	. . . . . . 7 ⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) ∧ (𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆)) → ((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) ∧ 𝑦 ∈ 𝑆))
94		df-3an 1103	. . . . . . 7 ⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑦 ∈ 𝑆) ↔ ((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) ∧ 𝑦 ∈ 𝑆))
95	93, 94	sylibr 237	. . . . . 6 ⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) ∧ (𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆)) → (𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑦 ∈ 𝑆))
96	1, 2, 3, 4	cpmatpmat 22828	. . . . . 6 ⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑦 ∈ 𝑆) → 𝑦 ∈ (Base‘𝐶))
97	95, 96	syl 18	. . . . 5 ⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) ∧ (𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆)) → 𝑦 ∈ (Base‘𝐶))
98	4, 29	ringacl 20352	. . . . 5 ⊢ ((𝐶 ∈ Ring ∧ 𝑥 ∈ (Base‘𝐶) ∧ 𝑦 ∈ (Base‘𝐶)) → (𝑥(+_g‘𝐶)𝑦) ∈ (Base‘𝐶))
99	85, 91, 97, 98	syl3anc 1394	. . . 4 ⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) ∧ (𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆)) → (𝑥(+_g‘𝐶)𝑦) ∈ (Base‘𝐶))
100	1, 2, 3, 4, 5, 6	cpmatel2 22831	. . . 4 ⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ (𝑥(+_g‘𝐶)𝑦) ∈ (Base‘𝐶)) → ((𝑥(+_g‘𝐶)𝑦) ∈ 𝑆 ↔ ∀𝑖 ∈ 𝑁 ∀𝑗 ∈ 𝑁 ∃𝑐 ∈ (Base‘𝑅)(𝑖(𝑥(+_g‘𝐶)𝑦)𝑗) = ((algSc‘𝑃)‘𝑐)))
101	81, 83, 99, 100	syl3anc 1394	. . 3 ⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) ∧ (𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆)) → ((𝑥(+_g‘𝐶)𝑦) ∈ 𝑆 ↔ ∀𝑖 ∈ 𝑁 ∀𝑗 ∈ 𝑁 ∃𝑐 ∈ (Base‘𝑅)(𝑖(𝑥(+_g‘𝐶)𝑦)𝑗) = ((algSc‘𝑃)‘𝑐)))
102	79, 101	mpbird 260	. 2 ⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) ∧ (𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆)) → (𝑥(+_g‘𝐶)𝑦) ∈ 𝑆)
103	102	ralrimivva 3208	1 ⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) → ∀𝑥 ∈ 𝑆 ∀𝑦 ∈ 𝑆 (𝑥(+_g‘𝐶)𝑦) ∈ 𝑆)

Colors of variables: wff setvar class

Syntax hints: → wi 4 ↔ wb 209 ∧ wa 400 ∧ w3a 1101 = wceq 1563 ∈ wcel 2145 ∀wral 3079 ∃wrex 3089 ‘cfv 6525 (class class class)co 7400 Fincfn 8931 Basecbs 17259 +_gcplusg 17300 Scalarcsca 17303 GrpHom cghm 19274 Ringcrg 20306 LModclmod 20950 algSccascl 21962 Poly₁cpl1 22297 Mat cmat 22525 ConstPolyMat ccpmat 22821

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1818 ax-4 1832 ax-5 1933 ax-6 1990 ax-7 2031 ax-8 2147 ax-9 2155 ax-10 2178 ax-11 2194 ax-12 2215 ax-ext 2737 ax-rep 5232 ax-sep 5251 ax-nul 5261 ax-pow 5327 ax-pr 5395 ax-un 7722 ax-cnex 11144 ax-resscn 11145 ax-1cn 11146 ax-icn 11147 ax-addcl 11148 ax-addrcl 11149 ax-mulcl 11150 ax-mulrcl 11151 ax-mulcom 11152 ax-addass 11153 ax-mulass 11154 ax-distr 11155 ax-i2m1 11156 ax-1ne0 11157 ax-1rid 11158 ax-rnegex 11159 ax-rrecex 11160 ax-cnre 11161 ax-pre-lttri 11162 ax-pre-lttrn 11163 ax-pre-ltadd 11164 ax-pre-mulgt0 11165

This theorem depends on definitions: df-bi 210 df-an 401 df-or 861 df-3or 1102 df-3an 1103 df-tru 1566 df-fal 1576 df-ex 1803 df-nf 1807 df-sb 2094 df-mo 2569 df-eu 2599 df-clab 2744 df-cleq 2757 df-clel 2840 df-nfc 2914 df-ne 2961 df-nel 3065 df-ral 3080 df-rex 3090 df-rmo 3370 df-reu 3371 df-rab 3418 df-v 3459 df-sbc 3748 df-csb 3856 df-dif 3910 df-un 3912 df-in 3914 df-ss 3924 df-pss 3927 df-nul 4289 df-if 4484 df-pw 4560 df-sn 4586 df-pr 4588 df-tp 4590 df-op 4592 df-ot 4594 df-uni 4869 df-int 4909 df-iun 4954 df-iin 4955 df-br 5106 df-opab 5168 df-mpt 5187 df-tr 5213 df-id 5547 df-eprel 5552 df-po 5560 df-so 5561 df-fr 5605 df-se 5606 df-we 5607 df-xp 5658 df-rel 5659 df-cnv 5660 df-co 5661 df-dm 5662 df-rn 5663 df-res 5664 df-ima 5665 df-pred 6292 df-ord 6353 df-on 6354 df-lim 6355 df-suc 6356 df-iota 6481 df-fun 6527 df-fn 6528 df-f 6529 df-f1 6530 df-fo 6531 df-f1o 6532 df-fv 6533 df-isom 6534 df-riota 7357 df-ov 7403 df-oprab 7404 df-mpo 7405 df-of 7664 df-ofr 7665 df-om 7851 df-1st 7974 df-2nd 7975 df-supp 8145 df-frecs 8266 df-wrecs 8297 df-recs 8346 df-rdg 8385 df-1o 8441 df-2o 8442 df-er 8682 df-map 8814 df-pm 8815 df-ixp 8884 df-en 8932 df-dom 8933 df-sdom 8934 df-fin 8935 df-fsupp 9310 df-sup 9390 df-oi 9460 df-card 9913 df-pnf 11233 df-mnf 11234 df-xr 11235 df-ltxr 11236 df-le 11237 df-sub 11431 df-neg 11432 df-nn 12225 df-2 12294 df-3 12295 df-4 12296 df-5 12297 df-6 12298 df-7 12299 df-8 12300 df-9 12301 df-n0 12496 df-z 12583 df-dec 12703 df-uz 12854 df-fz 13527 df-fzo 13674 df-seq 14029 df-hash 14358 df-struct 17197 df-sets 17214 df-slot 17232 df-ndx 17244 df-base 17260 df-ress 17281 df-plusg 17313 df-mulr 17314 df-sca 17316 df-vsca 17317 df-ip 17318 df-tset 17319 df-ple 17320 df-ds 17322 df-hom 17324 df-cco 17325 df-0g 17484 df-gsum 17485 df-prds 17490 df-pws 17492 df-mre 17628 df-mrc 17629 df-acs 17631 df-mgm 18688 df-sgrp 18767 df-mnd 18783 df-mhm 18831 df-submnd 18832 df-grp 18993 df-minusg 18994 df-sbg 18995 df-mulg 19125 df-subg 19180 df-ghm 19275 df-cntz 19378 df-cmn 19843 df-abl 19844 df-mgp 20208 df-rng 20222 df-ur 20255 df-srg 20260 df-ring 20308 df-subrng 20622 df-subrg 20646 df-lmod 20952 df-lss 21022 df-sra 21263 df-rgmod 21264 df-dsmm 21842 df-frlm 21857 df-ascl 21965 df-psr 22019 df-mvr 22020 df-mpl 22021 df-opsr 22023 df-psr1 22300 df-vr1 22301 df-ply1 22302 df-coe1 22303 df-mamu 22509 df-mat 22526 df-cpmat 22824

This theorem is referenced by: cpmatsubgpmat 22838

W3C validator