Metamath Proof Explorer

Theorem cpmatinvcl

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

Ref Expression
Hypotheses cpmatsrngpmat.s ⊢ 𝑆 = ( 𝑁 ConstPolyMat 𝑅 )
cpmatsrngpmat.p ⊢ 𝑃 = ( Poly1 ‘ 𝑅 )
cpmatsrngpmat.c ⊢ 𝐶 = ( 𝑁 Mat 𝑃 )
Assertion cpmatinvcl ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) → ∀ 𝑥 ∈ 𝑆 ( ( invg ‘ 𝐶 ) ‘ 𝑥 ) ∈ 𝑆 )

Proof

Step Hyp Ref Expression
1 cpmatsrngpmat.s ⊢ 𝑆 = ( 𝑁 ConstPolyMat 𝑅 )
2 cpmatsrngpmat.p ⊢ 𝑃 = ( Poly1 ‘ 𝑅 )
3 cpmatsrngpmat.c ⊢ 𝐶 = ( 𝑁 Mat 𝑃 )
4 eqid ⊢ ( Base ‘ 𝐶 ) = ( Base ‘ 𝐶 )
5 eqid ⊢ ( Base ‘ 𝑅 ) = ( Base ‘ 𝑅 )
6 eqid ⊢ ( algSc ‘ 𝑃 ) = ( algSc ‘ 𝑃 )
7 1 2 3 4 5 6 cpmatelimp2 ⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) → ( 𝑥 ∈ 𝑆 → ( 𝑥 ∈ ( Base ‘ 𝐶 ) ∧ ∀ 𝑖 ∈ 𝑁 ∀ 𝑗 ∈ 𝑁 ∃ 𝑎 ∈ ( Base ‘ 𝑅 ) ( 𝑖 𝑥 𝑗 ) = ( ( algSc ‘ 𝑃 ) ‘ 𝑎 ) ) ) )
8 2 ply1sca ⊢ ( 𝑅 ∈ Ring → 𝑅 = ( Scalar ‘ 𝑃 ) )
9 8 adantl ⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) → 𝑅 = ( Scalar ‘ 𝑃 ) )
10 9 adantr ⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ 𝑎 ∈ ( Base ‘ 𝑅 ) ) → 𝑅 = ( Scalar ‘ 𝑃 ) )
11 10 eqcomd ⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ 𝑎 ∈ ( Base ‘ 𝑅 ) ) → ( Scalar ‘ 𝑃 ) = 𝑅 )
12 11 fveq2d ⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ 𝑎 ∈ ( Base ‘ 𝑅 ) ) → ( invg ‘ ( Scalar ‘ 𝑃 ) ) = ( invg ‘ 𝑅 ) )
13 12 fveq1d ⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ 𝑎 ∈ ( Base ‘ 𝑅 ) ) → ( ( invg ‘ ( Scalar ‘ 𝑃 ) ) ‘ 𝑎 ) = ( ( invg ‘ 𝑅 ) ‘ 𝑎 ) )
14 ringgrp ⊢ ( 𝑅 ∈ Ring → 𝑅 ∈ Grp )
15 14 adantl ⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) → 𝑅 ∈ Grp )
16 eqid ⊢ ( invg ‘ 𝑅 ) = ( invg ‘ 𝑅 )
17 5 16 grpinvcl ⊢ ( ( 𝑅 ∈ Grp ∧ 𝑎 ∈ ( Base ‘ 𝑅 ) ) → ( ( invg ‘ 𝑅 ) ‘ 𝑎 ) ∈ ( Base ‘ 𝑅 ) )
18 15 17 sylan ⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ 𝑎 ∈ ( Base ‘ 𝑅 ) ) → ( ( invg ‘ 𝑅 ) ‘ 𝑎 ) ∈ ( Base ‘ 𝑅 ) )
19 13 18 eqeltrd ⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ 𝑎 ∈ ( Base ‘ 𝑅 ) ) → ( ( invg ‘ ( Scalar ‘ 𝑃 ) ) ‘ 𝑎 ) ∈ ( Base ‘ 𝑅 ) )
20 19 ad5ant14 ⊢ ( ( ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ 𝑥 ∈ ( Base ‘ 𝐶 ) ) ∧ ( 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁 ) ) ∧ 𝑎 ∈ ( Base ‘ 𝑅 ) ) ∧ ( 𝑖 𝑥 𝑗 ) = ( ( algSc ‘ 𝑃 ) ‘ 𝑎 ) ) → ( ( invg ‘ ( Scalar ‘ 𝑃 ) ) ‘ 𝑎 ) ∈ ( Base ‘ 𝑅 ) )
21 fveq2 ⊢ ( 𝑐 = ( ( invg ‘ ( Scalar ‘ 𝑃 ) ) ‘ 𝑎 ) → ( ( algSc ‘ 𝑃 ) ‘ 𝑐 ) = ( ( algSc ‘ 𝑃 ) ‘ ( ( invg ‘ ( Scalar ‘ 𝑃 ) ) ‘ 𝑎 ) ) )
22 21 eqeq2d ⊢ ( 𝑐 = ( ( invg ‘ ( Scalar ‘ 𝑃 ) ) ‘ 𝑎 ) → ( ( 𝑖 ( ( invg ‘ 𝐶 ) ‘ 𝑥 ) 𝑗 ) = ( ( algSc ‘ 𝑃 ) ‘ 𝑐 ) ↔ ( 𝑖 ( ( invg ‘ 𝐶 ) ‘ 𝑥 ) 𝑗 ) = ( ( algSc ‘ 𝑃 ) ‘ ( ( invg ‘ ( Scalar ‘ 𝑃 ) ) ‘ 𝑎 ) ) ) )
23 22 adantl ⊢ ( ( ( ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ 𝑥 ∈ ( Base ‘ 𝐶 ) ) ∧ ( 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁 ) ) ∧ 𝑎 ∈ ( Base ‘ 𝑅 ) ) ∧ ( 𝑖 𝑥 𝑗 ) = ( ( algSc ‘ 𝑃 ) ‘ 𝑎 ) ) ∧ 𝑐 = ( ( invg ‘ ( Scalar ‘ 𝑃 ) ) ‘ 𝑎 ) ) → ( ( 𝑖 ( ( invg ‘ 𝐶 ) ‘ 𝑥 ) 𝑗 ) = ( ( algSc ‘ 𝑃 ) ‘ 𝑐 ) ↔ ( 𝑖 ( ( invg ‘ 𝐶 ) ‘ 𝑥 ) 𝑗 ) = ( ( algSc ‘ 𝑃 ) ‘ ( ( invg ‘ ( Scalar ‘ 𝑃 ) ) ‘ 𝑎 ) ) ) )
24 2 ply1ring ⊢ ( 𝑅 ∈ Ring → 𝑃 ∈ Ring )
25 24 ad3antlr ⊢ ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ 𝑥 ∈ ( Base ‘ 𝐶 ) ) ∧ ( 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁 ) ) → 𝑃 ∈ Ring )
26 simplr ⊢ ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ 𝑥 ∈ ( Base ‘ 𝐶 ) ) ∧ ( 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁 ) ) → 𝑥 ∈ ( Base ‘ 𝐶 ) )
27 simpr ⊢ ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ 𝑥 ∈ ( Base ‘ 𝐶 ) ) ∧ ( 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁 ) ) → ( 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁 ) )
28 25 26 27 3jca ⊢ ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ 𝑥 ∈ ( Base ‘ 𝐶 ) ) ∧ ( 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁 ) ) → ( 𝑃 ∈ Ring ∧ 𝑥 ∈ ( Base ‘ 𝐶 ) ∧ ( 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁 ) ) )
29 28 ad2antrr ⊢ ( ( ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ 𝑥 ∈ ( Base ‘ 𝐶 ) ) ∧ ( 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁 ) ) ∧ 𝑎 ∈ ( Base ‘ 𝑅 ) ) ∧ ( 𝑖 𝑥 𝑗 ) = ( ( algSc ‘ 𝑃 ) ‘ 𝑎 ) ) → ( 𝑃 ∈ Ring ∧ 𝑥 ∈ ( Base ‘ 𝐶 ) ∧ ( 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁 ) ) )
30 eqid ⊢ ( invg ‘ 𝑃 ) = ( invg ‘ 𝑃 )
31 eqid ⊢ ( invg ‘ 𝐶 ) = ( invg ‘ 𝐶 )
32 3 4 30 31 matinvgcell ⊢ ( ( 𝑃 ∈ Ring ∧ 𝑥 ∈ ( Base ‘ 𝐶 ) ∧ ( 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁 ) ) → ( 𝑖 ( ( invg ‘ 𝐶 ) ‘ 𝑥 ) 𝑗 ) = ( ( invg ‘ 𝑃 ) ‘ ( 𝑖 𝑥 𝑗 ) ) )
33 29 32 syl ⊢ ( ( ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ 𝑥 ∈ ( Base ‘ 𝐶 ) ) ∧ ( 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁 ) ) ∧ 𝑎 ∈ ( Base ‘ 𝑅 ) ) ∧ ( 𝑖 𝑥 𝑗 ) = ( ( algSc ‘ 𝑃 ) ‘ 𝑎 ) ) → ( 𝑖 ( ( invg ‘ 𝐶 ) ‘ 𝑥 ) 𝑗 ) = ( ( invg ‘ 𝑃 ) ‘ ( 𝑖 𝑥 𝑗 ) ) )
34 fveq2 ⊢ ( ( 𝑖 𝑥 𝑗 ) = ( ( algSc ‘ 𝑃 ) ‘ 𝑎 ) → ( ( invg ‘ 𝑃 ) ‘ ( 𝑖 𝑥 𝑗 ) ) = ( ( invg ‘ 𝑃 ) ‘ ( ( algSc ‘ 𝑃 ) ‘ 𝑎 ) ) )
35 eqid ⊢ ( Scalar ‘ 𝑃 ) = ( Scalar ‘ 𝑃 )
36 25 adantr ⊢ ( ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ 𝑥 ∈ ( Base ‘ 𝐶 ) ) ∧ ( 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁 ) ) ∧ 𝑎 ∈ ( Base ‘ 𝑅 ) ) → 𝑃 ∈ Ring )
37 2 ply1lmod ⊢ ( 𝑅 ∈ Ring → 𝑃 ∈ LMod )
38 37 ad3antlr ⊢ ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ 𝑥 ∈ ( Base ‘ 𝐶 ) ) ∧ ( 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁 ) ) → 𝑃 ∈ LMod )
39 38 adantr ⊢ ( ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ 𝑥 ∈ ( Base ‘ 𝐶 ) ) ∧ ( 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁 ) ) ∧ 𝑎 ∈ ( Base ‘ 𝑅 ) ) → 𝑃 ∈ LMod )
40 6 35 36 39 asclghm ⊢ ( ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ 𝑥 ∈ ( Base ‘ 𝐶 ) ) ∧ ( 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁 ) ) ∧ 𝑎 ∈ ( Base ‘ 𝑅 ) ) → ( algSc ‘ 𝑃 ) ∈ ( ( Scalar ‘ 𝑃 ) GrpHom 𝑃 ) )
41 9 fveq2d ⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) → ( Base ‘ 𝑅 ) = ( Base ‘ ( Scalar ‘ 𝑃 ) ) )
42 41 eleq2d ⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) → ( 𝑎 ∈ ( Base ‘ 𝑅 ) ↔ 𝑎 ∈ ( Base ‘ ( Scalar ‘ 𝑃 ) ) ) )
43 42 biimpd ⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) → ( 𝑎 ∈ ( Base ‘ 𝑅 ) → 𝑎 ∈ ( Base ‘ ( Scalar ‘ 𝑃 ) ) ) )
44 43 ad2antrr ⊢ ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ 𝑥 ∈ ( Base ‘ 𝐶 ) ) ∧ ( 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁 ) ) → ( 𝑎 ∈ ( Base ‘ 𝑅 ) → 𝑎 ∈ ( Base ‘ ( Scalar ‘ 𝑃 ) ) ) )
45 44 imp ⊢ ( ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ 𝑥 ∈ ( Base ‘ 𝐶 ) ) ∧ ( 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁 ) ) ∧ 𝑎 ∈ ( Base ‘ 𝑅 ) ) → 𝑎 ∈ ( Base ‘ ( Scalar ‘ 𝑃 ) ) )
46 eqid ⊢ ( Base ‘ ( Scalar ‘ 𝑃 ) ) = ( Base ‘ ( Scalar ‘ 𝑃 ) )
47 eqid ⊢ ( invg ‘ ( Scalar ‘ 𝑃 ) ) = ( invg ‘ ( Scalar ‘ 𝑃 ) )
48 46 47 30 ghminv ⊢ ( ( ( algSc ‘ 𝑃 ) ∈ ( ( Scalar ‘ 𝑃 ) GrpHom 𝑃 ) ∧ 𝑎 ∈ ( Base ‘ ( Scalar ‘ 𝑃 ) ) ) → ( ( algSc ‘ 𝑃 ) ‘ ( ( invg ‘ ( Scalar ‘ 𝑃 ) ) ‘ 𝑎 ) ) = ( ( invg ‘ 𝑃 ) ‘ ( ( algSc ‘ 𝑃 ) ‘ 𝑎 ) ) )
49 40 45 48 syl2anc ⊢ ( ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ 𝑥 ∈ ( Base ‘ 𝐶 ) ) ∧ ( 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁 ) ) ∧ 𝑎 ∈ ( Base ‘ 𝑅 ) ) → ( ( algSc ‘ 𝑃 ) ‘ ( ( invg ‘ ( Scalar ‘ 𝑃 ) ) ‘ 𝑎 ) ) = ( ( invg ‘ 𝑃 ) ‘ ( ( algSc ‘ 𝑃 ) ‘ 𝑎 ) ) )
50 49 eqcomd ⊢ ( ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ 𝑥 ∈ ( Base ‘ 𝐶 ) ) ∧ ( 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁 ) ) ∧ 𝑎 ∈ ( Base ‘ 𝑅 ) ) → ( ( invg ‘ 𝑃 ) ‘ ( ( algSc ‘ 𝑃 ) ‘ 𝑎 ) ) = ( ( algSc ‘ 𝑃 ) ‘ ( ( invg ‘ ( Scalar ‘ 𝑃 ) ) ‘ 𝑎 ) ) )
51 34 50 sylan9eqr ⊢ ( ( ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ 𝑥 ∈ ( Base ‘ 𝐶 ) ) ∧ ( 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁 ) ) ∧ 𝑎 ∈ ( Base ‘ 𝑅 ) ) ∧ ( 𝑖 𝑥 𝑗 ) = ( ( algSc ‘ 𝑃 ) ‘ 𝑎 ) ) → ( ( invg ‘ 𝑃 ) ‘ ( 𝑖 𝑥 𝑗 ) ) = ( ( algSc ‘ 𝑃 ) ‘ ( ( invg ‘ ( Scalar ‘ 𝑃 ) ) ‘ 𝑎 ) ) )
52 33 51 eqtrd ⊢ ( ( ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ 𝑥 ∈ ( Base ‘ 𝐶 ) ) ∧ ( 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁 ) ) ∧ 𝑎 ∈ ( Base ‘ 𝑅 ) ) ∧ ( 𝑖 𝑥 𝑗 ) = ( ( algSc ‘ 𝑃 ) ‘ 𝑎 ) ) → ( 𝑖 ( ( invg ‘ 𝐶 ) ‘ 𝑥 ) 𝑗 ) = ( ( algSc ‘ 𝑃 ) ‘ ( ( invg ‘ ( Scalar ‘ 𝑃 ) ) ‘ 𝑎 ) ) )
53 20 23 52 rspcedvd ⊢ ( ( ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ 𝑥 ∈ ( Base ‘ 𝐶 ) ) ∧ ( 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁 ) ) ∧ 𝑎 ∈ ( Base ‘ 𝑅 ) ) ∧ ( 𝑖 𝑥 𝑗 ) = ( ( algSc ‘ 𝑃 ) ‘ 𝑎 ) ) → ∃ 𝑐 ∈ ( Base ‘ 𝑅 ) ( 𝑖 ( ( invg ‘ 𝐶 ) ‘ 𝑥 ) 𝑗 ) = ( ( algSc ‘ 𝑃 ) ‘ 𝑐 ) )
54 53 rexlimdva2 ⊢ ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ 𝑥 ∈ ( Base ‘ 𝐶 ) ) ∧ ( 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁 ) ) → ( ∃ 𝑎 ∈ ( Base ‘ 𝑅 ) ( 𝑖 𝑥 𝑗 ) = ( ( algSc ‘ 𝑃 ) ‘ 𝑎 ) → ∃ 𝑐 ∈ ( Base ‘ 𝑅 ) ( 𝑖 ( ( invg ‘ 𝐶 ) ‘ 𝑥 ) 𝑗 ) = ( ( algSc ‘ 𝑃 ) ‘ 𝑐 ) ) )
55 54 ralimdvva ⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ 𝑥 ∈ ( Base ‘ 𝐶 ) ) → ( ∀ 𝑖 ∈ 𝑁 ∀ 𝑗 ∈ 𝑁 ∃ 𝑎 ∈ ( Base ‘ 𝑅 ) ( 𝑖 𝑥 𝑗 ) = ( ( algSc ‘ 𝑃 ) ‘ 𝑎 ) → ∀ 𝑖 ∈ 𝑁 ∀ 𝑗 ∈ 𝑁 ∃ 𝑐 ∈ ( Base ‘ 𝑅 ) ( 𝑖 ( ( invg ‘ 𝐶 ) ‘ 𝑥 ) 𝑗 ) = ( ( algSc ‘ 𝑃 ) ‘ 𝑐 ) ) )
56 55 expimpd ⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) → ( ( 𝑥 ∈ ( Base ‘ 𝐶 ) ∧ ∀ 𝑖 ∈ 𝑁 ∀ 𝑗 ∈ 𝑁 ∃ 𝑎 ∈ ( Base ‘ 𝑅 ) ( 𝑖 𝑥 𝑗 ) = ( ( algSc ‘ 𝑃 ) ‘ 𝑎 ) ) → ∀ 𝑖 ∈ 𝑁 ∀ 𝑗 ∈ 𝑁 ∃ 𝑐 ∈ ( Base ‘ 𝑅 ) ( 𝑖 ( ( invg ‘ 𝐶 ) ‘ 𝑥 ) 𝑗 ) = ( ( algSc ‘ 𝑃 ) ‘ 𝑐 ) ) )
57 7 56 syld ⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) → ( 𝑥 ∈ 𝑆 → ∀ 𝑖 ∈ 𝑁 ∀ 𝑗 ∈ 𝑁 ∃ 𝑐 ∈ ( Base ‘ 𝑅 ) ( 𝑖 ( ( invg ‘ 𝐶 ) ‘ 𝑥 ) 𝑗 ) = ( ( algSc ‘ 𝑃 ) ‘ 𝑐 ) ) )
58 57 imp ⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ 𝑥 ∈ 𝑆 ) → ∀ 𝑖 ∈ 𝑁 ∀ 𝑗 ∈ 𝑁 ∃ 𝑐 ∈ ( Base ‘ 𝑅 ) ( 𝑖 ( ( invg ‘ 𝐶 ) ‘ 𝑥 ) 𝑗 ) = ( ( algSc ‘ 𝑃 ) ‘ 𝑐 ) )
59 simpll ⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ 𝑥 ∈ 𝑆 ) → 𝑁 ∈ Fin )
60 simplr ⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ 𝑥 ∈ 𝑆 ) → 𝑅 ∈ Ring )
61 2 3 pmatring ⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) → 𝐶 ∈ Ring )
62 ringgrp ⊢ ( 𝐶 ∈ Ring → 𝐶 ∈ Grp )
63 61 62 syl ⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) → 𝐶 ∈ Grp )
64 63 adantr ⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ 𝑥 ∈ 𝑆 ) → 𝐶 ∈ Grp )
65 1 2 3 4 cpmatpmat ⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑥 ∈ 𝑆 ) → 𝑥 ∈ ( Base ‘ 𝐶 ) )
66 65 3expa ⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ 𝑥 ∈ 𝑆 ) → 𝑥 ∈ ( Base ‘ 𝐶 ) )
67 4 31 grpinvcl ⊢ ( ( 𝐶 ∈ Grp ∧ 𝑥 ∈ ( Base ‘ 𝐶 ) ) → ( ( invg ‘ 𝐶 ) ‘ 𝑥 ) ∈ ( Base ‘ 𝐶 ) )
68 64 66 67 syl2anc ⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ 𝑥 ∈ 𝑆 ) → ( ( invg ‘ 𝐶 ) ‘ 𝑥 ) ∈ ( Base ‘ 𝐶 ) )
69 1 2 3 4 5 6 cpmatel2 ⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ ( ( invg ‘ 𝐶 ) ‘ 𝑥 ) ∈ ( Base ‘ 𝐶 ) ) → ( ( ( invg ‘ 𝐶 ) ‘ 𝑥 ) ∈ 𝑆 ↔ ∀ 𝑖 ∈ 𝑁 ∀ 𝑗 ∈ 𝑁 ∃ 𝑐 ∈ ( Base ‘ 𝑅 ) ( 𝑖 ( ( invg ‘ 𝐶 ) ‘ 𝑥 ) 𝑗 ) = ( ( algSc ‘ 𝑃 ) ‘ 𝑐 ) ) )
70 59 60 68 69 syl3anc ⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ 𝑥 ∈ 𝑆 ) → ( ( ( invg ‘ 𝐶 ) ‘ 𝑥 ) ∈ 𝑆 ↔ ∀ 𝑖 ∈ 𝑁 ∀ 𝑗 ∈ 𝑁 ∃ 𝑐 ∈ ( Base ‘ 𝑅 ) ( 𝑖 ( ( invg ‘ 𝐶 ) ‘ 𝑥 ) 𝑗 ) = ( ( algSc ‘ 𝑃 ) ‘ 𝑐 ) ) )
71 58 70 mpbird ⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ 𝑥 ∈ 𝑆 ) → ( ( invg ‘ 𝐶 ) ‘ 𝑥 ) ∈ 𝑆 )
72 71 ralrimiva ⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) → ∀ 𝑥 ∈ 𝑆 ( ( invg ‘ 𝐶 ) ‘ 𝑥 ) ∈ 𝑆 )