Step | Hyp | Ref
| Expression |
1 | | cpmatsrngpmat.s |
. . . . . 6
⊢ 𝑆 = (𝑁 ConstPolyMat 𝑅) |
2 | | cpmatsrngpmat.p |
. . . . . 6
⊢ 𝑃 = (Poly1‘𝑅) |
3 | | cpmatsrngpmat.c |
. . . . . 6
⊢ 𝐶 = (𝑁 Mat 𝑃) |
4 | | eqid 2738 |
. . . . . 6
⊢
(Base‘𝐶) =
(Base‘𝐶) |
5 | | eqid 2738 |
. . . . . 6
⊢
(Base‘𝑅) =
(Base‘𝑅) |
6 | | eqid 2738 |
. . . . . 6
⊢
(algSc‘𝑃) =
(algSc‘𝑃) |
7 | 1, 2, 3, 4, 5, 6 | cpmatelimp2 21863 |
. . . . 5
⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) → (𝑥 ∈ 𝑆 → (𝑥 ∈ (Base‘𝐶) ∧ ∀𝑖 ∈ 𝑁 ∀𝑗 ∈ 𝑁 ∃𝑎 ∈ (Base‘𝑅)(𝑖𝑥𝑗) = ((algSc‘𝑃)‘𝑎)))) |
8 | 2 | ply1sca 21424 |
. . . . . . . . . . . . . . . 16
⊢ (𝑅 ∈ Ring → 𝑅 = (Scalar‘𝑃)) |
9 | 8 | adantl 482 |
. . . . . . . . . . . . . . 15
⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) → 𝑅 = (Scalar‘𝑃)) |
10 | 9 | adantr 481 |
. . . . . . . . . . . . . 14
⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) ∧ 𝑎 ∈ (Base‘𝑅)) → 𝑅 = (Scalar‘𝑃)) |
11 | 10 | eqcomd 2744 |
. . . . . . . . . . . . 13
⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) ∧ 𝑎 ∈ (Base‘𝑅)) → (Scalar‘𝑃) = 𝑅) |
12 | 11 | fveq2d 6778 |
. . . . . . . . . . . 12
⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) ∧ 𝑎 ∈ (Base‘𝑅)) →
(invg‘(Scalar‘𝑃)) = (invg‘𝑅)) |
13 | 12 | fveq1d 6776 |
. . . . . . . . . . 11
⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) ∧ 𝑎 ∈ (Base‘𝑅)) →
((invg‘(Scalar‘𝑃))‘𝑎) = ((invg‘𝑅)‘𝑎)) |
14 | | ringgrp 19788 |
. . . . . . . . . . . . 13
⊢ (𝑅 ∈ Ring → 𝑅 ∈ Grp) |
15 | 14 | adantl 482 |
. . . . . . . . . . . 12
⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) → 𝑅 ∈ Grp) |
16 | | eqid 2738 |
. . . . . . . . . . . . 13
⊢
(invg‘𝑅) = (invg‘𝑅) |
17 | 5, 16 | grpinvcl 18627 |
. . . . . . . . . . . 12
⊢ ((𝑅 ∈ Grp ∧ 𝑎 ∈ (Base‘𝑅)) →
((invg‘𝑅)‘𝑎) ∈ (Base‘𝑅)) |
18 | 15, 17 | sylan 580 |
. . . . . . . . . . 11
⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) ∧ 𝑎 ∈ (Base‘𝑅)) →
((invg‘𝑅)‘𝑎) ∈ (Base‘𝑅)) |
19 | 13, 18 | eqeltrd 2839 |
. . . . . . . . . 10
⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) ∧ 𝑎 ∈ (Base‘𝑅)) →
((invg‘(Scalar‘𝑃))‘𝑎) ∈ (Base‘𝑅)) |
20 | 19 | ad5ant14 755 |
. . . . . . . . 9
⊢
((((((𝑁 ∈ Fin
∧ 𝑅 ∈ Ring) ∧
𝑥 ∈ (Base‘𝐶)) ∧ (𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁)) ∧ 𝑎 ∈ (Base‘𝑅)) ∧ (𝑖𝑥𝑗) = ((algSc‘𝑃)‘𝑎)) →
((invg‘(Scalar‘𝑃))‘𝑎) ∈ (Base‘𝑅)) |
21 | | fveq2 6774 |
. . . . . . . . . . 11
⊢ (𝑐 =
((invg‘(Scalar‘𝑃))‘𝑎) → ((algSc‘𝑃)‘𝑐) = ((algSc‘𝑃)‘((invg‘(Scalar‘𝑃))‘𝑎))) |
22 | 21 | eqeq2d 2749 |
. . . . . . . . . 10
⊢ (𝑐 =
((invg‘(Scalar‘𝑃))‘𝑎) → ((𝑖((invg‘𝐶)‘𝑥)𝑗) = ((algSc‘𝑃)‘𝑐) ↔ (𝑖((invg‘𝐶)‘𝑥)𝑗) = ((algSc‘𝑃)‘((invg‘(Scalar‘𝑃))‘𝑎)))) |
23 | 22 | adantl 482 |
. . . . . . . . 9
⊢
(((((((𝑁 ∈ Fin
∧ 𝑅 ∈ Ring) ∧
𝑥 ∈ (Base‘𝐶)) ∧ (𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁)) ∧ 𝑎 ∈ (Base‘𝑅)) ∧ (𝑖𝑥𝑗) = ((algSc‘𝑃)‘𝑎)) ∧ 𝑐 =
((invg‘(Scalar‘𝑃))‘𝑎)) → ((𝑖((invg‘𝐶)‘𝑥)𝑗) = ((algSc‘𝑃)‘𝑐) ↔ (𝑖((invg‘𝐶)‘𝑥)𝑗) = ((algSc‘𝑃)‘((invg‘(Scalar‘𝑃))‘𝑎)))) |
24 | 2 | ply1ring 21419 |
. . . . . . . . . . . . . 14
⊢ (𝑅 ∈ Ring → 𝑃 ∈ Ring) |
25 | 24 | ad3antlr 728 |
. . . . . . . . . . . . 13
⊢ ((((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) ∧ 𝑥 ∈ (Base‘𝐶)) ∧ (𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁)) → 𝑃 ∈ Ring) |
26 | | simplr 766 |
. . . . . . . . . . . . 13
⊢ ((((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) ∧ 𝑥 ∈ (Base‘𝐶)) ∧ (𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁)) → 𝑥 ∈ (Base‘𝐶)) |
27 | | simpr 485 |
. . . . . . . . . . . . 13
⊢ ((((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) ∧ 𝑥 ∈ (Base‘𝐶)) ∧ (𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁)) → (𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁)) |
28 | 25, 26, 27 | 3jca 1127 |
. . . . . . . . . . . 12
⊢ ((((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) ∧ 𝑥 ∈ (Base‘𝐶)) ∧ (𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁)) → (𝑃 ∈ Ring ∧ 𝑥 ∈ (Base‘𝐶) ∧ (𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁))) |
29 | 28 | ad2antrr 723 |
. . . . . . . . . . 11
⊢
((((((𝑁 ∈ Fin
∧ 𝑅 ∈ Ring) ∧
𝑥 ∈ (Base‘𝐶)) ∧ (𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁)) ∧ 𝑎 ∈ (Base‘𝑅)) ∧ (𝑖𝑥𝑗) = ((algSc‘𝑃)‘𝑎)) → (𝑃 ∈ Ring ∧ 𝑥 ∈ (Base‘𝐶) ∧ (𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁))) |
30 | | eqid 2738 |
. . . . . . . . . . . 12
⊢
(invg‘𝑃) = (invg‘𝑃) |
31 | | eqid 2738 |
. . . . . . . . . . . 12
⊢
(invg‘𝐶) = (invg‘𝐶) |
32 | 3, 4, 30, 31 | matinvgcell 21584 |
. . . . . . . . . . 11
⊢ ((𝑃 ∈ Ring ∧ 𝑥 ∈ (Base‘𝐶) ∧ (𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁)) → (𝑖((invg‘𝐶)‘𝑥)𝑗) = ((invg‘𝑃)‘(𝑖𝑥𝑗))) |
33 | 29, 32 | syl 17 |
. . . . . . . . . 10
⊢
((((((𝑁 ∈ Fin
∧ 𝑅 ∈ Ring) ∧
𝑥 ∈ (Base‘𝐶)) ∧ (𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁)) ∧ 𝑎 ∈ (Base‘𝑅)) ∧ (𝑖𝑥𝑗) = ((algSc‘𝑃)‘𝑎)) → (𝑖((invg‘𝐶)‘𝑥)𝑗) = ((invg‘𝑃)‘(𝑖𝑥𝑗))) |
34 | | fveq2 6774 |
. . . . . . . . . . 11
⊢ ((𝑖𝑥𝑗) = ((algSc‘𝑃)‘𝑎) → ((invg‘𝑃)‘(𝑖𝑥𝑗)) = ((invg‘𝑃)‘((algSc‘𝑃)‘𝑎))) |
35 | | eqid 2738 |
. . . . . . . . . . . . . 14
⊢
(Scalar‘𝑃) =
(Scalar‘𝑃) |
36 | 25 | adantr 481 |
. . . . . . . . . . . . . 14
⊢
(((((𝑁 ∈ Fin
∧ 𝑅 ∈ Ring) ∧
𝑥 ∈ (Base‘𝐶)) ∧ (𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁)) ∧ 𝑎 ∈ (Base‘𝑅)) → 𝑃 ∈ Ring) |
37 | 2 | ply1lmod 21423 |
. . . . . . . . . . . . . . . 16
⊢ (𝑅 ∈ Ring → 𝑃 ∈ LMod) |
38 | 37 | ad3antlr 728 |
. . . . . . . . . . . . . . 15
⊢ ((((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) ∧ 𝑥 ∈ (Base‘𝐶)) ∧ (𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁)) → 𝑃 ∈ LMod) |
39 | 38 | adantr 481 |
. . . . . . . . . . . . . 14
⊢
(((((𝑁 ∈ Fin
∧ 𝑅 ∈ Ring) ∧
𝑥 ∈ (Base‘𝐶)) ∧ (𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁)) ∧ 𝑎 ∈ (Base‘𝑅)) → 𝑃 ∈ LMod) |
40 | 6, 35, 36, 39 | asclghm 21087 |
. . . . . . . . . . . . 13
⊢
(((((𝑁 ∈ Fin
∧ 𝑅 ∈ Ring) ∧
𝑥 ∈ (Base‘𝐶)) ∧ (𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁)) ∧ 𝑎 ∈ (Base‘𝑅)) → (algSc‘𝑃) ∈ ((Scalar‘𝑃) GrpHom 𝑃)) |
41 | 9 | fveq2d 6778 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) →
(Base‘𝑅) =
(Base‘(Scalar‘𝑃))) |
42 | 41 | eleq2d 2824 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) → (𝑎 ∈ (Base‘𝑅) ↔ 𝑎 ∈ (Base‘(Scalar‘𝑃)))) |
43 | 42 | biimpd 228 |
. . . . . . . . . . . . . . 15
⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) → (𝑎 ∈ (Base‘𝑅) → 𝑎 ∈ (Base‘(Scalar‘𝑃)))) |
44 | 43 | ad2antrr 723 |
. . . . . . . . . . . . . 14
⊢ ((((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) ∧ 𝑥 ∈ (Base‘𝐶)) ∧ (𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁)) → (𝑎 ∈ (Base‘𝑅) → 𝑎 ∈ (Base‘(Scalar‘𝑃)))) |
45 | 44 | imp 407 |
. . . . . . . . . . . . 13
⊢
(((((𝑁 ∈ Fin
∧ 𝑅 ∈ Ring) ∧
𝑥 ∈ (Base‘𝐶)) ∧ (𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁)) ∧ 𝑎 ∈ (Base‘𝑅)) → 𝑎 ∈ (Base‘(Scalar‘𝑃))) |
46 | | eqid 2738 |
. . . . . . . . . . . . . 14
⊢
(Base‘(Scalar‘𝑃)) = (Base‘(Scalar‘𝑃)) |
47 | | eqid 2738 |
. . . . . . . . . . . . . 14
⊢
(invg‘(Scalar‘𝑃)) =
(invg‘(Scalar‘𝑃)) |
48 | 46, 47, 30 | ghminv 18841 |
. . . . . . . . . . . . 13
⊢
(((algSc‘𝑃)
∈ ((Scalar‘𝑃)
GrpHom 𝑃) ∧ 𝑎 ∈
(Base‘(Scalar‘𝑃))) → ((algSc‘𝑃)‘((invg‘(Scalar‘𝑃))‘𝑎)) = ((invg‘𝑃)‘((algSc‘𝑃)‘𝑎))) |
49 | 40, 45, 48 | syl2anc 584 |
. . . . . . . . . . . 12
⊢
(((((𝑁 ∈ Fin
∧ 𝑅 ∈ Ring) ∧
𝑥 ∈ (Base‘𝐶)) ∧ (𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁)) ∧ 𝑎 ∈ (Base‘𝑅)) → ((algSc‘𝑃)‘((invg‘(Scalar‘𝑃))‘𝑎)) = ((invg‘𝑃)‘((algSc‘𝑃)‘𝑎))) |
50 | 49 | eqcomd 2744 |
. . . . . . . . . . 11
⊢
(((((𝑁 ∈ Fin
∧ 𝑅 ∈ Ring) ∧
𝑥 ∈ (Base‘𝐶)) ∧ (𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁)) ∧ 𝑎 ∈ (Base‘𝑅)) → ((invg‘𝑃)‘((algSc‘𝑃)‘𝑎)) = ((algSc‘𝑃)‘((invg‘(Scalar‘𝑃))‘𝑎))) |
51 | 34, 50 | sylan9eqr 2800 |
. . . . . . . . . 10
⊢
((((((𝑁 ∈ Fin
∧ 𝑅 ∈ Ring) ∧
𝑥 ∈ (Base‘𝐶)) ∧ (𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁)) ∧ 𝑎 ∈ (Base‘𝑅)) ∧ (𝑖𝑥𝑗) = ((algSc‘𝑃)‘𝑎)) → ((invg‘𝑃)‘(𝑖𝑥𝑗)) = ((algSc‘𝑃)‘((invg‘(Scalar‘𝑃))‘𝑎))) |
52 | 33, 51 | eqtrd 2778 |
. . . . . . . . 9
⊢
((((((𝑁 ∈ Fin
∧ 𝑅 ∈ Ring) ∧
𝑥 ∈ (Base‘𝐶)) ∧ (𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁)) ∧ 𝑎 ∈ (Base‘𝑅)) ∧ (𝑖𝑥𝑗) = ((algSc‘𝑃)‘𝑎)) → (𝑖((invg‘𝐶)‘𝑥)𝑗) = ((algSc‘𝑃)‘((invg‘(Scalar‘𝑃))‘𝑎))) |
53 | 20, 23, 52 | rspcedvd 3563 |
. . . . . . . 8
⊢
((((((𝑁 ∈ Fin
∧ 𝑅 ∈ Ring) ∧
𝑥 ∈ (Base‘𝐶)) ∧ (𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁)) ∧ 𝑎 ∈ (Base‘𝑅)) ∧ (𝑖𝑥𝑗) = ((algSc‘𝑃)‘𝑎)) → ∃𝑐 ∈ (Base‘𝑅)(𝑖((invg‘𝐶)‘𝑥)𝑗) = ((algSc‘𝑃)‘𝑐)) |
54 | 53 | rexlimdva2 3216 |
. . . . . . 7
⊢ ((((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) ∧ 𝑥 ∈ (Base‘𝐶)) ∧ (𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁)) → (∃𝑎 ∈ (Base‘𝑅)(𝑖𝑥𝑗) = ((algSc‘𝑃)‘𝑎) → ∃𝑐 ∈ (Base‘𝑅)(𝑖((invg‘𝐶)‘𝑥)𝑗) = ((algSc‘𝑃)‘𝑐))) |
55 | 54 | ralimdvva 3126 |
. . . . . 6
⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) ∧ 𝑥 ∈ (Base‘𝐶)) → (∀𝑖 ∈ 𝑁 ∀𝑗 ∈ 𝑁 ∃𝑎 ∈ (Base‘𝑅)(𝑖𝑥𝑗) = ((algSc‘𝑃)‘𝑎) → ∀𝑖 ∈ 𝑁 ∀𝑗 ∈ 𝑁 ∃𝑐 ∈ (Base‘𝑅)(𝑖((invg‘𝐶)‘𝑥)𝑗) = ((algSc‘𝑃)‘𝑐))) |
56 | 55 | expimpd 454 |
. . . . 5
⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) → ((𝑥 ∈ (Base‘𝐶) ∧ ∀𝑖 ∈ 𝑁 ∀𝑗 ∈ 𝑁 ∃𝑎 ∈ (Base‘𝑅)(𝑖𝑥𝑗) = ((algSc‘𝑃)‘𝑎)) → ∀𝑖 ∈ 𝑁 ∀𝑗 ∈ 𝑁 ∃𝑐 ∈ (Base‘𝑅)(𝑖((invg‘𝐶)‘𝑥)𝑗) = ((algSc‘𝑃)‘𝑐))) |
57 | 7, 56 | syld 47 |
. . . 4
⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) → (𝑥 ∈ 𝑆 → ∀𝑖 ∈ 𝑁 ∀𝑗 ∈ 𝑁 ∃𝑐 ∈ (Base‘𝑅)(𝑖((invg‘𝐶)‘𝑥)𝑗) = ((algSc‘𝑃)‘𝑐))) |
58 | 57 | imp 407 |
. . 3
⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) ∧ 𝑥 ∈ 𝑆) → ∀𝑖 ∈ 𝑁 ∀𝑗 ∈ 𝑁 ∃𝑐 ∈ (Base‘𝑅)(𝑖((invg‘𝐶)‘𝑥)𝑗) = ((algSc‘𝑃)‘𝑐)) |
59 | | simpll 764 |
. . . 4
⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) ∧ 𝑥 ∈ 𝑆) → 𝑁 ∈ Fin) |
60 | | simplr 766 |
. . . 4
⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) ∧ 𝑥 ∈ 𝑆) → 𝑅 ∈ Ring) |
61 | 2, 3 | pmatring 21841 |
. . . . . . 7
⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) → 𝐶 ∈ Ring) |
62 | | ringgrp 19788 |
. . . . . . 7
⊢ (𝐶 ∈ Ring → 𝐶 ∈ Grp) |
63 | 61, 62 | syl 17 |
. . . . . 6
⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) → 𝐶 ∈ Grp) |
64 | 63 | adantr 481 |
. . . . 5
⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) ∧ 𝑥 ∈ 𝑆) → 𝐶 ∈ Grp) |
65 | 1, 2, 3, 4 | cpmatpmat 21859 |
. . . . . 6
⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑥 ∈ 𝑆) → 𝑥 ∈ (Base‘𝐶)) |
66 | 65 | 3expa 1117 |
. . . . 5
⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) ∧ 𝑥 ∈ 𝑆) → 𝑥 ∈ (Base‘𝐶)) |
67 | 4, 31 | grpinvcl 18627 |
. . . . 5
⊢ ((𝐶 ∈ Grp ∧ 𝑥 ∈ (Base‘𝐶)) →
((invg‘𝐶)‘𝑥) ∈ (Base‘𝐶)) |
68 | 64, 66, 67 | syl2anc 584 |
. . . 4
⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) ∧ 𝑥 ∈ 𝑆) → ((invg‘𝐶)‘𝑥) ∈ (Base‘𝐶)) |
69 | 1, 2, 3, 4, 5, 6 | cpmatel2 21862 |
. . . 4
⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧
((invg‘𝐶)‘𝑥) ∈ (Base‘𝐶)) → (((invg‘𝐶)‘𝑥) ∈ 𝑆 ↔ ∀𝑖 ∈ 𝑁 ∀𝑗 ∈ 𝑁 ∃𝑐 ∈ (Base‘𝑅)(𝑖((invg‘𝐶)‘𝑥)𝑗) = ((algSc‘𝑃)‘𝑐))) |
70 | 59, 60, 68, 69 | syl3anc 1370 |
. . 3
⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) ∧ 𝑥 ∈ 𝑆) → (((invg‘𝐶)‘𝑥) ∈ 𝑆 ↔ ∀𝑖 ∈ 𝑁 ∀𝑗 ∈ 𝑁 ∃𝑐 ∈ (Base‘𝑅)(𝑖((invg‘𝐶)‘𝑥)𝑗) = ((algSc‘𝑃)‘𝑐))) |
71 | 58, 70 | mpbird 256 |
. 2
⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) ∧ 𝑥 ∈ 𝑆) → ((invg‘𝐶)‘𝑥) ∈ 𝑆) |
72 | 71 | ralrimiva 3103 |
1
⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) →
∀𝑥 ∈ 𝑆 ((invg‘𝐶)‘𝑥) ∈ 𝑆) |