Theorem cpmatinvcl 21019

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

Hypotheses

Ref	Expression
cpmatsrngpmat.s	⊢ 𝑆 = (𝑁 ConstPolyMat 𝑅)
cpmatsrngpmat.p	⊢ 𝑃 = (Poly1‘𝑅)
cpmatsrngpmat.c	⊢ 𝐶 = (𝑁 Mat 𝑃)

Assertion

Ref	Expression
cpmatinvcl	⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) → ∀𝑥 ∈ 𝑆 ((invg‘𝐶)‘𝑥) ∈ 𝑆)

Distinct variable groups:   𝑥,𝑁   𝑥,𝑅

Allowed substitution hints:   𝐶(𝑥)   𝑃(𝑥)   𝑆(𝑥)

Proof of Theorem cpmatinvcl

Dummy variables 𝑖 𝑗 𝑎 𝑐 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		cpmatsrngpmat.s	. . . . . 6 ⊢ 𝑆 = (𝑁 ConstPolyMat 𝑅)
2		cpmatsrngpmat.p	. . . . . 6 ⊢ 𝑃 = (Poly1‘𝑅)
3		cpmatsrngpmat.c	. . . . . 6 ⊢ 𝐶 = (𝑁 Mat 𝑃)
4		eqid 2772	. . . . . 6 ⊢ (Base‘𝐶) = (Base‘𝐶)
5		eqid 2772	. . . . . 6 ⊢ (Base‘𝑅) = (Base‘𝑅)
6		eqid 2772	. . . . . 6 ⊢ (algSc‘𝑃) = (algSc‘𝑃)
7	1, 2, 3, 4, 5, 6	cpmatelimp2 21016	. . . . 5 ⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) → (𝑥 ∈ 𝑆 → (𝑥 ∈ (Base‘𝐶) ∧ ∀𝑖 ∈ 𝑁 ∀𝑗 ∈ 𝑁 ∃𝑎 ∈ (Base‘𝑅)(𝑖𝑥𝑗) = ((algSc‘𝑃)‘𝑎))))
8	2	ply1sca 20114	. . . . . . . . . . . . . . . 16 ⊢ (𝑅 ∈ Ring → 𝑅 = (Scalar‘𝑃))
9	8	adantl 474	. . . . . . . . . . . . . . 15 ⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) → 𝑅 = (Scalar‘𝑃))
10	9	adantr 473	. . . . . . . . . . . . . 14 ⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) ∧ 𝑎 ∈ (Base‘𝑅)) → 𝑅 = (Scalar‘𝑃))
11	10	eqcomd 2778	. . . . . . . . . . . . 13 ⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) ∧ 𝑎 ∈ (Base‘𝑅)) → (Scalar‘𝑃) = 𝑅)
12	11	fveq2d 6497	. . . . . . . . . . . 12 ⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) ∧ 𝑎 ∈ (Base‘𝑅)) → (invg‘(Scalar‘𝑃)) = (invg‘𝑅))
13	12	fveq1d 6495	. . . . . . . . . . 11 ⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) ∧ 𝑎 ∈ (Base‘𝑅)) → ((invg‘(Scalar‘𝑃))‘𝑎) = ((invg‘𝑅)‘𝑎))
14		ringgrp 19015	. . . . . . . . . . . . 13 ⊢ (𝑅 ∈ Ring → 𝑅 ∈ Grp)
15	14	adantl 474	. . . . . . . . . . . 12 ⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) → 𝑅 ∈ Grp)
16		eqid 2772	. . . . . . . . . . . . 13 ⊢ (invg‘𝑅) = (invg‘𝑅)
17	5, 16	grpinvcl 17928	. . . . . . . . . . . 12 ⊢ ((𝑅 ∈ Grp ∧ 𝑎 ∈ (Base‘𝑅)) → ((invg‘𝑅)‘𝑎) ∈ (Base‘𝑅))
18	15, 17	sylan 572	. . . . . . . . . . 11 ⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) ∧ 𝑎 ∈ (Base‘𝑅)) → ((invg‘𝑅)‘𝑎) ∈ (Base‘𝑅))
19	13, 18	eqeltrd 2860	. . . . . . . . . 10 ⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) ∧ 𝑎 ∈ (Base‘𝑅)) → ((invg‘(Scalar‘𝑃))‘𝑎) ∈ (Base‘𝑅))
20	19	ad5ant14 745	. . . . . . . . 9 ⊢ ((((((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) ∧ 𝑥 ∈ (Base‘𝐶)) ∧ (𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁)) ∧ 𝑎 ∈ (Base‘𝑅)) ∧ (𝑖𝑥𝑗) = ((algSc‘𝑃)‘𝑎)) → ((invg‘(Scalar‘𝑃))‘𝑎) ∈ (Base‘𝑅))
21		fveq2 6493	. . . . . . . . . . 11 ⊢ (𝑐 = ((invg‘(Scalar‘𝑃))‘𝑎) → ((algSc‘𝑃)‘𝑐) = ((algSc‘𝑃)‘((invg‘(Scalar‘𝑃))‘𝑎)))
22	21	eqeq2d 2782	. . . . . . . . . 10 ⊢ (𝑐 = ((invg‘(Scalar‘𝑃))‘𝑎) → ((𝑖((invg‘𝐶)‘𝑥)𝑗) = ((algSc‘𝑃)‘𝑐) ↔ (𝑖((invg‘𝐶)‘𝑥)𝑗) = ((algSc‘𝑃)‘((invg‘(Scalar‘𝑃))‘𝑎))))
23	22	adantl 474	. . . . . . . . 9 ⊢ (((((((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) ∧ 𝑥 ∈ (Base‘𝐶)) ∧ (𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁)) ∧ 𝑎 ∈ (Base‘𝑅)) ∧ (𝑖𝑥𝑗) = ((algSc‘𝑃)‘𝑎)) ∧ 𝑐 = ((invg‘(Scalar‘𝑃))‘𝑎)) → ((𝑖((invg‘𝐶)‘𝑥)𝑗) = ((algSc‘𝑃)‘𝑐) ↔ (𝑖((invg‘𝐶)‘𝑥)𝑗) = ((algSc‘𝑃)‘((invg‘(Scalar‘𝑃))‘𝑎))))
24	2	ply1ring 20109	. . . . . . . . . . . . . 14 ⊢ (𝑅 ∈ Ring → 𝑃 ∈ Ring)
25	24	ad3antlr 718	. . . . . . . . . . . . 13 ⊢ ((((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) ∧ 𝑥 ∈ (Base‘𝐶)) ∧ (𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁)) → 𝑃 ∈ Ring)
26		simplr 756	. . . . . . . . . . . . 13 ⊢ ((((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) ∧ 𝑥 ∈ (Base‘𝐶)) ∧ (𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁)) → 𝑥 ∈ (Base‘𝐶))
27		simpr 477	. . . . . . . . . . . . 13 ⊢ ((((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) ∧ 𝑥 ∈ (Base‘𝐶)) ∧ (𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁)) → (𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁))
28	25, 26, 27	3jca 1108	. . . . . . . . . . . 12 ⊢ ((((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) ∧ 𝑥 ∈ (Base‘𝐶)) ∧ (𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁)) → (𝑃 ∈ Ring ∧ 𝑥 ∈ (Base‘𝐶) ∧ (𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁)))
29	28	ad2antrr 713	. . . . . . . . . . 11 ⊢ ((((((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) ∧ 𝑥 ∈ (Base‘𝐶)) ∧ (𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁)) ∧ 𝑎 ∈ (Base‘𝑅)) ∧ (𝑖𝑥𝑗) = ((algSc‘𝑃)‘𝑎)) → (𝑃 ∈ Ring ∧ 𝑥 ∈ (Base‘𝐶) ∧ (𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁)))
30		eqid 2772	. . . . . . . . . . . 12 ⊢ (invg‘𝑃) = (invg‘𝑃)
31		eqid 2772	. . . . . . . . . . . 12 ⊢ (invg‘𝐶) = (invg‘𝐶)
32	3, 4, 30, 31	matinvgcell 20738	. . . . . . . . . . 11 ⊢ ((𝑃 ∈ Ring ∧ 𝑥 ∈ (Base‘𝐶) ∧ (𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁)) → (𝑖((invg‘𝐶)‘𝑥)𝑗) = ((invg‘𝑃)‘(𝑖𝑥𝑗)))
33	29, 32	syl 17	. . . . . . . . . 10 ⊢ ((((((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) ∧ 𝑥 ∈ (Base‘𝐶)) ∧ (𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁)) ∧ 𝑎 ∈ (Base‘𝑅)) ∧ (𝑖𝑥𝑗) = ((algSc‘𝑃)‘𝑎)) → (𝑖((invg‘𝐶)‘𝑥)𝑗) = ((invg‘𝑃)‘(𝑖𝑥𝑗)))
34		fveq2 6493	. . . . . . . . . . 11 ⊢ ((𝑖𝑥𝑗) = ((algSc‘𝑃)‘𝑎) → ((invg‘𝑃)‘(𝑖𝑥𝑗)) = ((invg‘𝑃)‘((algSc‘𝑃)‘𝑎)))
35		eqid 2772	. . . . . . . . . . . . . 14 ⊢ (Scalar‘𝑃) = (Scalar‘𝑃)
36	25	adantr 473	. . . . . . . . . . . . . 14 ⊢ (((((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) ∧ 𝑥 ∈ (Base‘𝐶)) ∧ (𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁)) ∧ 𝑎 ∈ (Base‘𝑅)) → 𝑃 ∈ Ring)
37	2	ply1lmod 20113	. . . . . . . . . . . . . . . 16 ⊢ (𝑅 ∈ Ring → 𝑃 ∈ LMod)
38	37	ad3antlr 718	. . . . . . . . . . . . . . 15 ⊢ ((((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) ∧ 𝑥 ∈ (Base‘𝐶)) ∧ (𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁)) → 𝑃 ∈ LMod)
39	38	adantr 473	. . . . . . . . . . . . . 14 ⊢ (((((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) ∧ 𝑥 ∈ (Base‘𝐶)) ∧ (𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁)) ∧ 𝑎 ∈ (Base‘𝑅)) → 𝑃 ∈ LMod)
40	6, 35, 36, 39	asclghm 19822	. . . . . . . . . . . . 13 ⊢ (((((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) ∧ 𝑥 ∈ (Base‘𝐶)) ∧ (𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁)) ∧ 𝑎 ∈ (Base‘𝑅)) → (algSc‘𝑃) ∈ ((Scalar‘𝑃) GrpHom 𝑃))
41	9	fveq2d 6497	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) → (Base‘𝑅) = (Base‘(Scalar‘𝑃)))
42	41	eleq2d 2845	. . . . . . . . . . . . . . . 16 ⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) → (𝑎 ∈ (Base‘𝑅) ↔ 𝑎 ∈ (Base‘(Scalar‘𝑃))))
43	42	biimpd 221	. . . . . . . . . . . . . . 15 ⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) → (𝑎 ∈ (Base‘𝑅) → 𝑎 ∈ (Base‘(Scalar‘𝑃))))
44	43	ad2antrr 713	. . . . . . . . . . . . . 14 ⊢ ((((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) ∧ 𝑥 ∈ (Base‘𝐶)) ∧ (𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁)) → (𝑎 ∈ (Base‘𝑅) → 𝑎 ∈ (Base‘(Scalar‘𝑃))))
45	44	imp 398	. . . . . . . . . . . . 13 ⊢ (((((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) ∧ 𝑥 ∈ (Base‘𝐶)) ∧ (𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁)) ∧ 𝑎 ∈ (Base‘𝑅)) → 𝑎 ∈ (Base‘(Scalar‘𝑃)))
46		eqid 2772	. . . . . . . . . . . . . 14 ⊢ (Base‘(Scalar‘𝑃)) = (Base‘(Scalar‘𝑃))
47		eqid 2772	. . . . . . . . . . . . . 14 ⊢ (invg‘(Scalar‘𝑃)) = (invg‘(Scalar‘𝑃))
48	46, 47, 30	ghminv 18126	. . . . . . . . . . . . 13 ⊢ (((algSc‘𝑃) ∈ ((Scalar‘𝑃) GrpHom 𝑃) ∧ 𝑎 ∈ (Base‘(Scalar‘𝑃))) → ((algSc‘𝑃)‘((invg‘(Scalar‘𝑃))‘𝑎)) = ((invg‘𝑃)‘((algSc‘𝑃)‘𝑎)))
49	40, 45, 48	syl2anc 576	. . . . . . . . . . . 12 ⊢ (((((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) ∧ 𝑥 ∈ (Base‘𝐶)) ∧ (𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁)) ∧ 𝑎 ∈ (Base‘𝑅)) → ((algSc‘𝑃)‘((invg‘(Scalar‘𝑃))‘𝑎)) = ((invg‘𝑃)‘((algSc‘𝑃)‘𝑎)))
50	49	eqcomd 2778	. . . . . . . . . . 11 ⊢ (((((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) ∧ 𝑥 ∈ (Base‘𝐶)) ∧ (𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁)) ∧ 𝑎 ∈ (Base‘𝑅)) → ((invg‘𝑃)‘((algSc‘𝑃)‘𝑎)) = ((algSc‘𝑃)‘((invg‘(Scalar‘𝑃))‘𝑎)))
51	34, 50	sylan9eqr 2830	. . . . . . . . . 10 ⊢ ((((((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) ∧ 𝑥 ∈ (Base‘𝐶)) ∧ (𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁)) ∧ 𝑎 ∈ (Base‘𝑅)) ∧ (𝑖𝑥𝑗) = ((algSc‘𝑃)‘𝑎)) → ((invg‘𝑃)‘(𝑖𝑥𝑗)) = ((algSc‘𝑃)‘((invg‘(Scalar‘𝑃))‘𝑎)))
52	33, 51	eqtrd 2808	. . . . . . . . 9 ⊢ ((((((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) ∧ 𝑥 ∈ (Base‘𝐶)) ∧ (𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁)) ∧ 𝑎 ∈ (Base‘𝑅)) ∧ (𝑖𝑥𝑗) = ((algSc‘𝑃)‘𝑎)) → (𝑖((invg‘𝐶)‘𝑥)𝑗) = ((algSc‘𝑃)‘((invg‘(Scalar‘𝑃))‘𝑎)))
53	20, 23, 52	rspcedvd 3536	. . . . . . . 8 ⊢ ((((((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) ∧ 𝑥 ∈ (Base‘𝐶)) ∧ (𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁)) ∧ 𝑎 ∈ (Base‘𝑅)) ∧ (𝑖𝑥𝑗) = ((algSc‘𝑃)‘𝑎)) → ∃𝑐 ∈ (Base‘𝑅)(𝑖((invg‘𝐶)‘𝑥)𝑗) = ((algSc‘𝑃)‘𝑐))
54	53	rexlimdva2 3226	. . . . . . 7 ⊢ ((((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) ∧ 𝑥 ∈ (Base‘𝐶)) ∧ (𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁)) → (∃𝑎 ∈ (Base‘𝑅)(𝑖𝑥𝑗) = ((algSc‘𝑃)‘𝑎) → ∃𝑐 ∈ (Base‘𝑅)(𝑖((invg‘𝐶)‘𝑥)𝑗) = ((algSc‘𝑃)‘𝑐)))
55	54	ralimdvva 3123	. . . . . 6 ⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) ∧ 𝑥 ∈ (Base‘𝐶)) → (∀𝑖 ∈ 𝑁 ∀𝑗 ∈ 𝑁 ∃𝑎 ∈ (Base‘𝑅)(𝑖𝑥𝑗) = ((algSc‘𝑃)‘𝑎) → ∀𝑖 ∈ 𝑁 ∀𝑗 ∈ 𝑁 ∃𝑐 ∈ (Base‘𝑅)(𝑖((invg‘𝐶)‘𝑥)𝑗) = ((algSc‘𝑃)‘𝑐)))
56	55	expimpd 446	. . . . 5 ⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) → ((𝑥 ∈ (Base‘𝐶) ∧ ∀𝑖 ∈ 𝑁 ∀𝑗 ∈ 𝑁 ∃𝑎 ∈ (Base‘𝑅)(𝑖𝑥𝑗) = ((algSc‘𝑃)‘𝑎)) → ∀𝑖 ∈ 𝑁 ∀𝑗 ∈ 𝑁 ∃𝑐 ∈ (Base‘𝑅)(𝑖((invg‘𝐶)‘𝑥)𝑗) = ((algSc‘𝑃)‘𝑐)))
57	7, 56	syld 47	. . . 4 ⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) → (𝑥 ∈ 𝑆 → ∀𝑖 ∈ 𝑁 ∀𝑗 ∈ 𝑁 ∃𝑐 ∈ (Base‘𝑅)(𝑖((invg‘𝐶)‘𝑥)𝑗) = ((algSc‘𝑃)‘𝑐)))
58	57	imp 398	. . 3 ⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) ∧ 𝑥 ∈ 𝑆) → ∀𝑖 ∈ 𝑁 ∀𝑗 ∈ 𝑁 ∃𝑐 ∈ (Base‘𝑅)(𝑖((invg‘𝐶)‘𝑥)𝑗) = ((algSc‘𝑃)‘𝑐))
59		simpll 754	. . . 4 ⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) ∧ 𝑥 ∈ 𝑆) → 𝑁 ∈ Fin)
60		simplr 756	. . . 4 ⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) ∧ 𝑥 ∈ 𝑆) → 𝑅 ∈ Ring)
61	2, 3	pmatring 20995	. . . . . . 7 ⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) → 𝐶 ∈ Ring)
62		ringgrp 19015	. . . . . . 7 ⊢ (𝐶 ∈ Ring → 𝐶 ∈ Grp)
63	61, 62	syl 17	. . . . . 6 ⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) → 𝐶 ∈ Grp)
64	63	adantr 473	. . . . 5 ⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) ∧ 𝑥 ∈ 𝑆) → 𝐶 ∈ Grp)
65	1, 2, 3, 4	cpmatpmat 21012	. . . . . 6 ⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑥 ∈ 𝑆) → 𝑥 ∈ (Base‘𝐶))
66	65	3expa 1098	. . . . 5 ⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) ∧ 𝑥 ∈ 𝑆) → 𝑥 ∈ (Base‘𝐶))
67	4, 31	grpinvcl 17928	. . . . 5 ⊢ ((𝐶 ∈ Grp ∧ 𝑥 ∈ (Base‘𝐶)) → ((invg‘𝐶)‘𝑥) ∈ (Base‘𝐶))
68	64, 66, 67	syl2anc 576	. . . 4 ⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) ∧ 𝑥 ∈ 𝑆) → ((invg‘𝐶)‘𝑥) ∈ (Base‘𝐶))
69	1, 2, 3, 4, 5, 6	cpmatel2 21015	. . . 4 ⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ ((invg‘𝐶)‘𝑥) ∈ (Base‘𝐶)) → (((invg‘𝐶)‘𝑥) ∈ 𝑆 ↔ ∀𝑖 ∈ 𝑁 ∀𝑗 ∈ 𝑁 ∃𝑐 ∈ (Base‘𝑅)(𝑖((invg‘𝐶)‘𝑥)𝑗) = ((algSc‘𝑃)‘𝑐)))
70	59, 60, 68, 69	syl3anc 1351	. . 3 ⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) ∧ 𝑥 ∈ 𝑆) → (((invg‘𝐶)‘𝑥) ∈ 𝑆 ↔ ∀𝑖 ∈ 𝑁 ∀𝑗 ∈ 𝑁 ∃𝑐 ∈ (Base‘𝑅)(𝑖((invg‘𝐶)‘𝑥)𝑗) = ((algSc‘𝑃)‘𝑐)))
71	58, 70	mpbird 249	. 2 ⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) ∧ 𝑥 ∈ 𝑆) → ((invg‘𝐶)‘𝑥) ∈ 𝑆)
72	71	ralrimiva 3126	1 ⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) → ∀𝑥 ∈ 𝑆 ((invg‘𝐶)‘𝑥) ∈ 𝑆)

Syntax hints:   → wi 4   ↔ wb 198   ∧ wa 387   ∧ w3a 1068   = wceq 1507   ∈ wcel 2048  ∀wral 3082  ∃wrex 3083  ‘cfv 6182  (class class class)co 6970  Fincfn 8298  Basecbs 16329  Scalarcsca 16414  Grpcgrp 17881  inv_gcminusg 17882   GrpHom cghm 18116  Ringcrg 19010  LModclmod 19346  algSccascl 19795  Poly₁cpl1 20038   Mat cmat 20710   ConstPolyMat ccpmat 21005

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1758  ax-4 1772  ax-5 1869  ax-6 1928  ax-7 1964  ax-8 2050  ax-9 2057  ax-10 2077  ax-11 2091  ax-12 2104  ax-13 2299  ax-ext 2745  ax-rep 5043  ax-sep 5054  ax-nul 5061  ax-pow 5113  ax-pr 5180  ax-un 7273  ax-cnex 10383  ax-resscn 10384  ax-1cn 10385  ax-icn 10386  ax-addcl 10387  ax-addrcl 10388  ax-mulcl 10389  ax-mulrcl 10390  ax-mulcom 10391  ax-addass 10392  ax-mulass 10393  ax-distr 10394  ax-i2m1 10395  ax-1ne0 10396  ax-1rid 10397  ax-rnegex 10398  ax-rrecex 10399  ax-cnre 10400  ax-pre-lttri 10401  ax-pre-lttrn 10402  ax-pre-ltadd 10403  ax-pre-mulgt0 10404

This theorem depends on definitions:  df-bi 199  df-an 388  df-or 834  df-3or 1069  df-3an 1070  df-tru 1510  df-fal 1520  df-ex 1743  df-nf 1747  df-sb 2014  df-mo 2544  df-eu 2580  df-clab 2754  df-cleq 2765  df-clel 2840  df-nfc 2912  df-ne 2962  df-nel 3068  df-ral 3087  df-rex 3088  df-reu 3089  df-rmo 3090  df-rab 3091  df-v 3411  df-sbc 3678  df-csb 3783  df-dif 3828  df-un 3830  df-in 3832  df-ss 3839  df-pss 3841  df-nul 4174  df-if 4345  df-pw 4418  df-sn 4436  df-pr 4438  df-tp 4440  df-op 4442  df-ot 4444  df-uni 4707  df-int 4744  df-iun 4788  df-iin 4789  df-br 4924  df-opab 4986  df-mpt 5003  df-tr 5025  df-id 5305  df-eprel 5310  df-po 5319  df-so 5320  df-fr 5359  df-se 5360  df-we 5361  df-xp 5406  df-rel 5407  df-cnv 5408  df-co 5409  df-dm 5410  df-rn 5411  df-res 5412  df-ima 5413  df-pred 5980  df-ord 6026  df-on 6027  df-lim 6028  df-suc 6029  df-iota 6146  df-fun 6184  df-fn 6185  df-f 6186  df-f1 6187  df-fo 6188  df-f1o 6189  df-fv 6190  df-isom 6191  df-riota 6931  df-ov 6973  df-oprab 6974  df-mpo 6975  df-of 7221  df-ofr 7222  df-om 7391  df-1st 7494  df-2nd 7495  df-supp 7627  df-wrecs 7743  df-recs 7805  df-rdg 7843  df-1o 7897  df-2o 7898  df-oadd 7901  df-er 8081  df-map 8200  df-pm 8201  df-ixp 8252  df-en 8299  df-dom 8300  df-sdom 8301  df-fin 8302  df-fsupp 8621  df-sup 8693  df-oi 8761  df-card 9154  df-pnf 10468  df-mnf 10469  df-xr 10470  df-ltxr 10471  df-le 10472  df-sub 10664  df-neg 10665  df-nn 11432  df-2 11496  df-3 11497  df-4 11498  df-5 11499  df-6 11500  df-7 11501  df-8 11502  df-9 11503  df-n0 11701  df-z 11787  df-dec 11905  df-uz 12052  df-fz 12702  df-fzo 12843  df-seq 13178  df-hash 13499  df-struct 16331  df-ndx 16332  df-slot 16333  df-base 16335  df-sets 16336  df-ress 16337  df-plusg 16424  df-mulr 16425  df-sca 16427  df-vsca 16428  df-ip 16429  df-tset 16430  df-ple 16431  df-ds 16433  df-hom 16435  df-cco 16436  df-0g 16561  df-gsum 16562  df-prds 16567  df-pws 16569  df-mre 16705  df-mrc 16706  df-acs 16708  df-mgm 17700  df-sgrp 17742  df-mnd 17753  df-mhm 17793  df-submnd 17794  df-grp 17884  df-minusg 17885  df-sbg 17886  df-mulg 18002  df-subg 18050  df-ghm 18117  df-cntz 18208  df-cmn 18658  df-abl 18659  df-mgp 18953  df-ur 18965  df-srg 18969  df-ring 19012  df-subrg 19246  df-lmod 19348  df-lss 19416  df-sra 19656  df-rgmod 19657  df-ascl 19798  df-psr 19840  df-mvr 19841  df-mpl 19842  df-opsr 19844  df-psr1 20041  df-vr1 20042  df-ply1 20043  df-coe1 20044  df-dsmm 20568  df-frlm 20583  df-mamu 20687  df-mat 20711  df-cpmat 21008

This theorem is referenced by:  cpmatsubgpmat  21022