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𝐶 ) ‘ 𝑥 ) ∈ 𝑆 )