Step | Hyp | Ref
| Expression |
1 | | cpmatsrngpmat.s |
. . . . . 6
⊢ 𝑆 = (𝑁 ConstPolyMat 𝑅) |
2 | | cpmatsrngpmat.p |
. . . . . 6
⊢ 𝑃 = (Poly1‘𝑅) |
3 | | cpmatsrngpmat.c |
. . . . . 6
⊢ 𝐶 = (𝑁 Mat 𝑃) |
4 | | eqid 2610 |
. . . . . 6
⊢
(Base‘𝐶) =
(Base‘𝐶) |
5 | | eqid 2610 |
. . . . . 6
⊢
(Base‘𝑅) =
(Base‘𝑅) |
6 | | eqid 2610 |
. . . . . 6
⊢
(algSc‘𝑃) =
(algSc‘𝑃) |
7 | 1, 2, 3, 4, 5, 6 | cpmatelimp2 20338 |
. . . . 5
⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) → (𝑥 ∈ 𝑆 → (𝑥 ∈ (Base‘𝐶) ∧ ∀𝑖 ∈ 𝑁 ∀𝑗 ∈ 𝑁 ∃𝑎 ∈ (Base‘𝑅)(𝑖𝑥𝑗) = ((algSc‘𝑃)‘𝑎)))) |
8 | 1, 2, 3, 4, 5, 6 | cpmatelimp2 20338 |
. . . . . . 7
⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) → (𝑦 ∈ 𝑆 → (𝑦 ∈ (Base‘𝐶) ∧ ∀𝑖 ∈ 𝑁 ∀𝑗 ∈ 𝑁 ∃𝑏 ∈ (Base‘𝑅)(𝑖𝑦𝑗) = ((algSc‘𝑃)‘𝑏)))) |
9 | | r19.26-2 3047 |
. . . . . . . . . . . . . 14
⊢
(∀𝑖 ∈
𝑁 ∀𝑗 ∈ 𝑁 (∃𝑎 ∈ (Base‘𝑅)(𝑖𝑥𝑗) = ((algSc‘𝑃)‘𝑎) ∧ ∃𝑏 ∈ (Base‘𝑅)(𝑖𝑦𝑗) = ((algSc‘𝑃)‘𝑏)) ↔ (∀𝑖 ∈ 𝑁 ∀𝑗 ∈ 𝑁 ∃𝑎 ∈ (Base‘𝑅)(𝑖𝑥𝑗) = ((algSc‘𝑃)‘𝑎) ∧ ∀𝑖 ∈ 𝑁 ∀𝑗 ∈ 𝑁 ∃𝑏 ∈ (Base‘𝑅)(𝑖𝑦𝑗) = ((algSc‘𝑃)‘𝑏))) |
10 | | eqid 2610 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢
(+g‘𝑅) = (+g‘𝑅) |
11 | 5, 10 | ringacl 18401 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ ((𝑅 ∈ Ring ∧ 𝑎 ∈ (Base‘𝑅) ∧ 𝑏 ∈ (Base‘𝑅)) → (𝑎(+g‘𝑅)𝑏) ∈ (Base‘𝑅)) |
12 | 11 | 3expb 1258 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ ((𝑅 ∈ Ring ∧ (𝑎 ∈ (Base‘𝑅) ∧ 𝑏 ∈ (Base‘𝑅))) → (𝑎(+g‘𝑅)𝑏) ∈ (Base‘𝑅)) |
13 | 2 | ply1sca 19444 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
⊢ (𝑅 ∈ Ring → 𝑅 = (Scalar‘𝑃)) |
14 | 13 | eqcomd 2616 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
⊢ (𝑅 ∈ Ring →
(Scalar‘𝑃) = 𝑅) |
15 | 14 | fveq2d 6107 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
⊢ (𝑅 ∈ Ring →
(+g‘(Scalar‘𝑃)) = (+g‘𝑅)) |
16 | 15 | oveqd 6566 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢ (𝑅 ∈ Ring → (𝑎(+g‘(Scalar‘𝑃))𝑏) = (𝑎(+g‘𝑅)𝑏)) |
17 | 16 | eleq1d 2672 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ (𝑅 ∈ Ring → ((𝑎(+g‘(Scalar‘𝑃))𝑏) ∈ (Base‘𝑅) ↔ (𝑎(+g‘𝑅)𝑏) ∈ (Base‘𝑅))) |
18 | 17 | adantr 480 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ ((𝑅 ∈ Ring ∧ (𝑎 ∈ (Base‘𝑅) ∧ 𝑏 ∈ (Base‘𝑅))) → ((𝑎(+g‘(Scalar‘𝑃))𝑏) ∈ (Base‘𝑅) ↔ (𝑎(+g‘𝑅)𝑏) ∈ (Base‘𝑅))) |
19 | 12, 18 | mpbird 246 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ ((𝑅 ∈ Ring ∧ (𝑎 ∈ (Base‘𝑅) ∧ 𝑏 ∈ (Base‘𝑅))) → (𝑎(+g‘(Scalar‘𝑃))𝑏) ∈ (Base‘𝑅)) |
20 | 19 | ex 449 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (𝑅 ∈ Ring → ((𝑎 ∈ (Base‘𝑅) ∧ 𝑏 ∈ (Base‘𝑅)) → (𝑎(+g‘(Scalar‘𝑃))𝑏) ∈ (Base‘𝑅))) |
21 | 20 | ad3antlr 763 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ ((((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) ∧ (𝑦 ∈ (Base‘𝐶) ∧ 𝑥 ∈ (Base‘𝐶))) ∧ (𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁)) → ((𝑎 ∈ (Base‘𝑅) ∧ 𝑏 ∈ (Base‘𝑅)) → (𝑎(+g‘(Scalar‘𝑃))𝑏) ∈ (Base‘𝑅))) |
22 | 21 | imp 444 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢
(((((𝑁 ∈ Fin
∧ 𝑅 ∈ Ring) ∧
(𝑦 ∈ (Base‘𝐶) ∧ 𝑥 ∈ (Base‘𝐶))) ∧ (𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁)) ∧ (𝑎 ∈ (Base‘𝑅) ∧ 𝑏 ∈ (Base‘𝑅))) → (𝑎(+g‘(Scalar‘𝑃))𝑏) ∈ (Base‘𝑅)) |
23 | 22 | adantr 480 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢
((((((𝑁 ∈ Fin
∧ 𝑅 ∈ Ring) ∧
(𝑦 ∈ (Base‘𝐶) ∧ 𝑥 ∈ (Base‘𝐶))) ∧ (𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁)) ∧ (𝑎 ∈ (Base‘𝑅) ∧ 𝑏 ∈ (Base‘𝑅))) ∧ ((𝑖𝑦𝑗) = ((algSc‘𝑃)‘𝑏) ∧ (𝑖𝑥𝑗) = ((algSc‘𝑃)‘𝑎))) → (𝑎(+g‘(Scalar‘𝑃))𝑏) ∈ (Base‘𝑅)) |
24 | | fveq2 6103 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (𝑐 = (𝑎(+g‘(Scalar‘𝑃))𝑏) → ((algSc‘𝑃)‘𝑐) = ((algSc‘𝑃)‘(𝑎(+g‘(Scalar‘𝑃))𝑏))) |
25 | 24 | eqeq2d 2620 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (𝑐 = (𝑎(+g‘(Scalar‘𝑃))𝑏) → ((𝑖(𝑥(+g‘𝐶)𝑦)𝑗) = ((algSc‘𝑃)‘𝑐) ↔ (𝑖(𝑥(+g‘𝐶)𝑦)𝑗) = ((algSc‘𝑃)‘(𝑎(+g‘(Scalar‘𝑃))𝑏)))) |
26 | 25 | adantl 481 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢
(((((((𝑁 ∈ Fin
∧ 𝑅 ∈ Ring) ∧
(𝑦 ∈ (Base‘𝐶) ∧ 𝑥 ∈ (Base‘𝐶))) ∧ (𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁)) ∧ (𝑎 ∈ (Base‘𝑅) ∧ 𝑏 ∈ (Base‘𝑅))) ∧ ((𝑖𝑦𝑗) = ((algSc‘𝑃)‘𝑏) ∧ (𝑖𝑥𝑗) = ((algSc‘𝑃)‘𝑎))) ∧ 𝑐 = (𝑎(+g‘(Scalar‘𝑃))𝑏)) → ((𝑖(𝑥(+g‘𝐶)𝑦)𝑗) = ((algSc‘𝑃)‘𝑐) ↔ (𝑖(𝑥(+g‘𝐶)𝑦)𝑗) = ((algSc‘𝑃)‘(𝑎(+g‘(Scalar‘𝑃))𝑏)))) |
27 | | simpr 476 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) ∧ (𝑦 ∈ (Base‘𝐶) ∧ 𝑥 ∈ (Base‘𝐶))) → (𝑦 ∈ (Base‘𝐶) ∧ 𝑥 ∈ (Base‘𝐶))) |
28 | 27 | ancomd 466 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) ∧ (𝑦 ∈ (Base‘𝐶) ∧ 𝑥 ∈ (Base‘𝐶))) → (𝑥 ∈ (Base‘𝐶) ∧ 𝑦 ∈ (Base‘𝐶))) |
29 | 28 | anim1i 590 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ ((((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) ∧ (𝑦 ∈ (Base‘𝐶) ∧ 𝑥 ∈ (Base‘𝐶))) ∧ (𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁)) → ((𝑥 ∈ (Base‘𝐶) ∧ 𝑦 ∈ (Base‘𝐶)) ∧ (𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁))) |
30 | 29 | ad2antrr 758 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢
((((((𝑁 ∈ Fin
∧ 𝑅 ∈ Ring) ∧
(𝑦 ∈ (Base‘𝐶) ∧ 𝑥 ∈ (Base‘𝐶))) ∧ (𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁)) ∧ (𝑎 ∈ (Base‘𝑅) ∧ 𝑏 ∈ (Base‘𝑅))) ∧ ((𝑖𝑦𝑗) = ((algSc‘𝑃)‘𝑏) ∧ (𝑖𝑥𝑗) = ((algSc‘𝑃)‘𝑎))) → ((𝑥 ∈ (Base‘𝐶) ∧ 𝑦 ∈ (Base‘𝐶)) ∧ (𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁))) |
31 | | eqid 2610 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢
(+g‘𝐶) = (+g‘𝐶) |
32 | | eqid 2610 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢
(+g‘𝑃) = (+g‘𝑃) |
33 | 3, 4, 31, 32 | matplusgcell 20058 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (((𝑥 ∈ (Base‘𝐶) ∧ 𝑦 ∈ (Base‘𝐶)) ∧ (𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁)) → (𝑖(𝑥(+g‘𝐶)𝑦)𝑗) = ((𝑖𝑥𝑗)(+g‘𝑃)(𝑖𝑦𝑗))) |
34 | 30, 33 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢
((((((𝑁 ∈ Fin
∧ 𝑅 ∈ Ring) ∧
(𝑦 ∈ (Base‘𝐶) ∧ 𝑥 ∈ (Base‘𝐶))) ∧ (𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁)) ∧ (𝑎 ∈ (Base‘𝑅) ∧ 𝑏 ∈ (Base‘𝑅))) ∧ ((𝑖𝑦𝑗) = ((algSc‘𝑃)‘𝑏) ∧ (𝑖𝑥𝑗) = ((algSc‘𝑃)‘𝑎))) → (𝑖(𝑥(+g‘𝐶)𝑦)𝑗) = ((𝑖𝑥𝑗)(+g‘𝑃)(𝑖𝑦𝑗))) |
35 | | oveq12 6558 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (((𝑖𝑥𝑗) = ((algSc‘𝑃)‘𝑎) ∧ (𝑖𝑦𝑗) = ((algSc‘𝑃)‘𝑏)) → ((𝑖𝑥𝑗)(+g‘𝑃)(𝑖𝑦𝑗)) = (((algSc‘𝑃)‘𝑎)(+g‘𝑃)((algSc‘𝑃)‘𝑏))) |
36 | 35 | ancoms 468 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (((𝑖𝑦𝑗) = ((algSc‘𝑃)‘𝑏) ∧ (𝑖𝑥𝑗) = ((algSc‘𝑃)‘𝑎)) → ((𝑖𝑥𝑗)(+g‘𝑃)(𝑖𝑦𝑗)) = (((algSc‘𝑃)‘𝑎)(+g‘𝑃)((algSc‘𝑃)‘𝑏))) |
37 | | eqid 2610 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢
(Scalar‘𝑃) =
(Scalar‘𝑃) |
38 | 2 | ply1ring 19439 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ (𝑅 ∈ Ring → 𝑃 ∈ Ring) |
39 | 38 | ad4antlr 765 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢
(((((𝑁 ∈ Fin
∧ 𝑅 ∈ Ring) ∧
(𝑦 ∈ (Base‘𝐶) ∧ 𝑥 ∈ (Base‘𝐶))) ∧ (𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁)) ∧ (𝑎 ∈ (Base‘𝑅) ∧ 𝑏 ∈ (Base‘𝑅))) → 𝑃 ∈ Ring) |
40 | 2 | ply1lmod 19443 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ (𝑅 ∈ Ring → 𝑃 ∈ LMod) |
41 | 40 | ad4antlr 765 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢
(((((𝑁 ∈ Fin
∧ 𝑅 ∈ Ring) ∧
(𝑦 ∈ (Base‘𝐶) ∧ 𝑥 ∈ (Base‘𝐶))) ∧ (𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁)) ∧ (𝑎 ∈ (Base‘𝑅) ∧ 𝑏 ∈ (Base‘𝑅))) → 𝑃 ∈ LMod) |
42 | 6, 37, 39, 41 | asclghm 19159 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢
(((((𝑁 ∈ Fin
∧ 𝑅 ∈ Ring) ∧
(𝑦 ∈ (Base‘𝐶) ∧ 𝑥 ∈ (Base‘𝐶))) ∧ (𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁)) ∧ (𝑎 ∈ (Base‘𝑅) ∧ 𝑏 ∈ (Base‘𝑅))) → (algSc‘𝑃) ∈ ((Scalar‘𝑃) GrpHom 𝑃)) |
43 | 13 | adantl 481 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) → 𝑅 = (Scalar‘𝑃)) |
44 | 43 | fveq2d 6107 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) →
(Base‘𝑅) =
(Base‘(Scalar‘𝑃))) |
45 | 44 | eleq2d 2673 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) → (𝑎 ∈ (Base‘𝑅) ↔ 𝑎 ∈ (Base‘(Scalar‘𝑃)))) |
46 | 45 | biimpd 218 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) → (𝑎 ∈ (Base‘𝑅) → 𝑎 ∈ (Base‘(Scalar‘𝑃)))) |
47 | 46 | ad2antrr 758 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ ((((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) ∧ (𝑦 ∈ (Base‘𝐶) ∧ 𝑥 ∈ (Base‘𝐶))) ∧ (𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁)) → (𝑎 ∈ (Base‘𝑅) → 𝑎 ∈ (Base‘(Scalar‘𝑃)))) |
48 | 47 | adantrd 483 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ ((((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) ∧ (𝑦 ∈ (Base‘𝐶) ∧ 𝑥 ∈ (Base‘𝐶))) ∧ (𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁)) → ((𝑎 ∈ (Base‘𝑅) ∧ 𝑏 ∈ (Base‘𝑅)) → 𝑎 ∈ (Base‘(Scalar‘𝑃)))) |
49 | 48 | imp 444 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢
(((((𝑁 ∈ Fin
∧ 𝑅 ∈ Ring) ∧
(𝑦 ∈ (Base‘𝐶) ∧ 𝑥 ∈ (Base‘𝐶))) ∧ (𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁)) ∧ (𝑎 ∈ (Base‘𝑅) ∧ 𝑏 ∈ (Base‘𝑅))) → 𝑎 ∈ (Base‘(Scalar‘𝑃))) |
50 | 13 | ad3antlr 763 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
⊢ ((((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) ∧ (𝑦 ∈ (Base‘𝐶) ∧ 𝑥 ∈ (Base‘𝐶))) ∧ (𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁)) → 𝑅 = (Scalar‘𝑃)) |
51 | 50 | fveq2d 6107 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
⊢ ((((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) ∧ (𝑦 ∈ (Base‘𝐶) ∧ 𝑥 ∈ (Base‘𝐶))) ∧ (𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁)) → (Base‘𝑅) = (Base‘(Scalar‘𝑃))) |
52 | 51 | eleq2d 2673 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢ ((((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) ∧ (𝑦 ∈ (Base‘𝐶) ∧ 𝑥 ∈ (Base‘𝐶))) ∧ (𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁)) → (𝑏 ∈ (Base‘𝑅) ↔ 𝑏 ∈ (Base‘(Scalar‘𝑃)))) |
53 | 52 | biimpd 218 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ ((((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) ∧ (𝑦 ∈ (Base‘𝐶) ∧ 𝑥 ∈ (Base‘𝐶))) ∧ (𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁)) → (𝑏 ∈ (Base‘𝑅) → 𝑏 ∈ (Base‘(Scalar‘𝑃)))) |
54 | 53 | adantld 482 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ ((((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) ∧ (𝑦 ∈ (Base‘𝐶) ∧ 𝑥 ∈ (Base‘𝐶))) ∧ (𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁)) → ((𝑎 ∈ (Base‘𝑅) ∧ 𝑏 ∈ (Base‘𝑅)) → 𝑏 ∈ (Base‘(Scalar‘𝑃)))) |
55 | 54 | imp 444 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢
(((((𝑁 ∈ Fin
∧ 𝑅 ∈ Ring) ∧
(𝑦 ∈ (Base‘𝐶) ∧ 𝑥 ∈ (Base‘𝐶))) ∧ (𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁)) ∧ (𝑎 ∈ (Base‘𝑅) ∧ 𝑏 ∈ (Base‘𝑅))) → 𝑏 ∈ (Base‘(Scalar‘𝑃))) |
56 | | eqid 2610 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢
(Base‘(Scalar‘𝑃)) = (Base‘(Scalar‘𝑃)) |
57 | | eqid 2610 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢
(+g‘(Scalar‘𝑃)) =
(+g‘(Scalar‘𝑃)) |
58 | 56, 57, 32 | ghmlin 17488 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢
(((algSc‘𝑃)
∈ ((Scalar‘𝑃)
GrpHom 𝑃) ∧ 𝑎 ∈
(Base‘(Scalar‘𝑃)) ∧ 𝑏 ∈ (Base‘(Scalar‘𝑃))) → ((algSc‘𝑃)‘(𝑎(+g‘(Scalar‘𝑃))𝑏)) = (((algSc‘𝑃)‘𝑎)(+g‘𝑃)((algSc‘𝑃)‘𝑏))) |
59 | 42, 49, 55, 58 | syl3anc 1318 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢
(((((𝑁 ∈ Fin
∧ 𝑅 ∈ Ring) ∧
(𝑦 ∈ (Base‘𝐶) ∧ 𝑥 ∈ (Base‘𝐶))) ∧ (𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁)) ∧ (𝑎 ∈ (Base‘𝑅) ∧ 𝑏 ∈ (Base‘𝑅))) → ((algSc‘𝑃)‘(𝑎(+g‘(Scalar‘𝑃))𝑏)) = (((algSc‘𝑃)‘𝑎)(+g‘𝑃)((algSc‘𝑃)‘𝑏))) |
60 | 59 | eqcomd 2616 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢
(((((𝑁 ∈ Fin
∧ 𝑅 ∈ Ring) ∧
(𝑦 ∈ (Base‘𝐶) ∧ 𝑥 ∈ (Base‘𝐶))) ∧ (𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁)) ∧ (𝑎 ∈ (Base‘𝑅) ∧ 𝑏 ∈ (Base‘𝑅))) → (((algSc‘𝑃)‘𝑎)(+g‘𝑃)((algSc‘𝑃)‘𝑏)) = ((algSc‘𝑃)‘(𝑎(+g‘(Scalar‘𝑃))𝑏))) |
61 | 36, 60 | sylan9eqr 2666 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢
((((((𝑁 ∈ Fin
∧ 𝑅 ∈ Ring) ∧
(𝑦 ∈ (Base‘𝐶) ∧ 𝑥 ∈ (Base‘𝐶))) ∧ (𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁)) ∧ (𝑎 ∈ (Base‘𝑅) ∧ 𝑏 ∈ (Base‘𝑅))) ∧ ((𝑖𝑦𝑗) = ((algSc‘𝑃)‘𝑏) ∧ (𝑖𝑥𝑗) = ((algSc‘𝑃)‘𝑎))) → ((𝑖𝑥𝑗)(+g‘𝑃)(𝑖𝑦𝑗)) = ((algSc‘𝑃)‘(𝑎(+g‘(Scalar‘𝑃))𝑏))) |
62 | 34, 61 | eqtrd 2644 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢
((((((𝑁 ∈ Fin
∧ 𝑅 ∈ Ring) ∧
(𝑦 ∈ (Base‘𝐶) ∧ 𝑥 ∈ (Base‘𝐶))) ∧ (𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁)) ∧ (𝑎 ∈ (Base‘𝑅) ∧ 𝑏 ∈ (Base‘𝑅))) ∧ ((𝑖𝑦𝑗) = ((algSc‘𝑃)‘𝑏) ∧ (𝑖𝑥𝑗) = ((algSc‘𝑃)‘𝑎))) → (𝑖(𝑥(+g‘𝐶)𝑦)𝑗) = ((algSc‘𝑃)‘(𝑎(+g‘(Scalar‘𝑃))𝑏))) |
63 | 23, 26, 62 | rspcedvd 3289 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢
((((((𝑁 ∈ Fin
∧ 𝑅 ∈ Ring) ∧
(𝑦 ∈ (Base‘𝐶) ∧ 𝑥 ∈ (Base‘𝐶))) ∧ (𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁)) ∧ (𝑎 ∈ (Base‘𝑅) ∧ 𝑏 ∈ (Base‘𝑅))) ∧ ((𝑖𝑦𝑗) = ((algSc‘𝑃)‘𝑏) ∧ (𝑖𝑥𝑗) = ((algSc‘𝑃)‘𝑎))) → ∃𝑐 ∈ (Base‘𝑅)(𝑖(𝑥(+g‘𝐶)𝑦)𝑗) = ((algSc‘𝑃)‘𝑐)) |
64 | 63 | ex 449 |
. . . . . . . . . . . . . . . . . . . . 21
⊢
(((((𝑁 ∈ Fin
∧ 𝑅 ∈ Ring) ∧
(𝑦 ∈ (Base‘𝐶) ∧ 𝑥 ∈ (Base‘𝐶))) ∧ (𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁)) ∧ (𝑎 ∈ (Base‘𝑅) ∧ 𝑏 ∈ (Base‘𝑅))) → (((𝑖𝑦𝑗) = ((algSc‘𝑃)‘𝑏) ∧ (𝑖𝑥𝑗) = ((algSc‘𝑃)‘𝑎)) → ∃𝑐 ∈ (Base‘𝑅)(𝑖(𝑥(+g‘𝐶)𝑦)𝑗) = ((algSc‘𝑃)‘𝑐))) |
65 | 64 | expd 451 |
. . . . . . . . . . . . . . . . . . . 20
⊢
(((((𝑁 ∈ Fin
∧ 𝑅 ∈ Ring) ∧
(𝑦 ∈ (Base‘𝐶) ∧ 𝑥 ∈ (Base‘𝐶))) ∧ (𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁)) ∧ (𝑎 ∈ (Base‘𝑅) ∧ 𝑏 ∈ (Base‘𝑅))) → ((𝑖𝑦𝑗) = ((algSc‘𝑃)‘𝑏) → ((𝑖𝑥𝑗) = ((algSc‘𝑃)‘𝑎) → ∃𝑐 ∈ (Base‘𝑅)(𝑖(𝑥(+g‘𝐶)𝑦)𝑗) = ((algSc‘𝑃)‘𝑐)))) |
66 | 65 | anassrs 678 |
. . . . . . . . . . . . . . . . . . 19
⊢
((((((𝑁 ∈ Fin
∧ 𝑅 ∈ Ring) ∧
(𝑦 ∈ (Base‘𝐶) ∧ 𝑥 ∈ (Base‘𝐶))) ∧ (𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁)) ∧ 𝑎 ∈ (Base‘𝑅)) ∧ 𝑏 ∈ (Base‘𝑅)) → ((𝑖𝑦𝑗) = ((algSc‘𝑃)‘𝑏) → ((𝑖𝑥𝑗) = ((algSc‘𝑃)‘𝑎) → ∃𝑐 ∈ (Base‘𝑅)(𝑖(𝑥(+g‘𝐶)𝑦)𝑗) = ((algSc‘𝑃)‘𝑐)))) |
67 | 66 | rexlimdva 3013 |
. . . . . . . . . . . . . . . . . 18
⊢
(((((𝑁 ∈ Fin
∧ 𝑅 ∈ Ring) ∧
(𝑦 ∈ (Base‘𝐶) ∧ 𝑥 ∈ (Base‘𝐶))) ∧ (𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁)) ∧ 𝑎 ∈ (Base‘𝑅)) → (∃𝑏 ∈ (Base‘𝑅)(𝑖𝑦𝑗) = ((algSc‘𝑃)‘𝑏) → ((𝑖𝑥𝑗) = ((algSc‘𝑃)‘𝑎) → ∃𝑐 ∈ (Base‘𝑅)(𝑖(𝑥(+g‘𝐶)𝑦)𝑗) = ((algSc‘𝑃)‘𝑐)))) |
68 | 67 | com23 84 |
. . . . . . . . . . . . . . . . 17
⊢
(((((𝑁 ∈ Fin
∧ 𝑅 ∈ Ring) ∧
(𝑦 ∈ (Base‘𝐶) ∧ 𝑥 ∈ (Base‘𝐶))) ∧ (𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁)) ∧ 𝑎 ∈ (Base‘𝑅)) → ((𝑖𝑥𝑗) = ((algSc‘𝑃)‘𝑎) → (∃𝑏 ∈ (Base‘𝑅)(𝑖𝑦𝑗) = ((algSc‘𝑃)‘𝑏) → ∃𝑐 ∈ (Base‘𝑅)(𝑖(𝑥(+g‘𝐶)𝑦)𝑗) = ((algSc‘𝑃)‘𝑐)))) |
69 | 68 | rexlimdva 3013 |
. . . . . . . . . . . . . . . 16
⊢ ((((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) ∧ (𝑦 ∈ (Base‘𝐶) ∧ 𝑥 ∈ (Base‘𝐶))) ∧ (𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁)) → (∃𝑎 ∈ (Base‘𝑅)(𝑖𝑥𝑗) = ((algSc‘𝑃)‘𝑎) → (∃𝑏 ∈ (Base‘𝑅)(𝑖𝑦𝑗) = ((algSc‘𝑃)‘𝑏) → ∃𝑐 ∈ (Base‘𝑅)(𝑖(𝑥(+g‘𝐶)𝑦)𝑗) = ((algSc‘𝑃)‘𝑐)))) |
70 | 69 | impd 446 |
. . . . . . . . . . . . . . 15
⊢ ((((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) ∧ (𝑦 ∈ (Base‘𝐶) ∧ 𝑥 ∈ (Base‘𝐶))) ∧ (𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁)) → ((∃𝑎 ∈ (Base‘𝑅)(𝑖𝑥𝑗) = ((algSc‘𝑃)‘𝑎) ∧ ∃𝑏 ∈ (Base‘𝑅)(𝑖𝑦𝑗) = ((algSc‘𝑃)‘𝑏)) → ∃𝑐 ∈ (Base‘𝑅)(𝑖(𝑥(+g‘𝐶)𝑦)𝑗) = ((algSc‘𝑃)‘𝑐))) |
71 | 70 | ralimdvva 2947 |
. . . . . . . . . . . . . 14
⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) ∧ (𝑦 ∈ (Base‘𝐶) ∧ 𝑥 ∈ (Base‘𝐶))) → (∀𝑖 ∈ 𝑁 ∀𝑗 ∈ 𝑁 (∃𝑎 ∈ (Base‘𝑅)(𝑖𝑥𝑗) = ((algSc‘𝑃)‘𝑎) ∧ ∃𝑏 ∈ (Base‘𝑅)(𝑖𝑦𝑗) = ((algSc‘𝑃)‘𝑏)) → ∀𝑖 ∈ 𝑁 ∀𝑗 ∈ 𝑁 ∃𝑐 ∈ (Base‘𝑅)(𝑖(𝑥(+g‘𝐶)𝑦)𝑗) = ((algSc‘𝑃)‘𝑐))) |
72 | 9, 71 | syl5bir 232 |
. . . . . . . . . . . . 13
⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) ∧ (𝑦 ∈ (Base‘𝐶) ∧ 𝑥 ∈ (Base‘𝐶))) → ((∀𝑖 ∈ 𝑁 ∀𝑗 ∈ 𝑁 ∃𝑎 ∈ (Base‘𝑅)(𝑖𝑥𝑗) = ((algSc‘𝑃)‘𝑎) ∧ ∀𝑖 ∈ 𝑁 ∀𝑗 ∈ 𝑁 ∃𝑏 ∈ (Base‘𝑅)(𝑖𝑦𝑗) = ((algSc‘𝑃)‘𝑏)) → ∀𝑖 ∈ 𝑁 ∀𝑗 ∈ 𝑁 ∃𝑐 ∈ (Base‘𝑅)(𝑖(𝑥(+g‘𝐶)𝑦)𝑗) = ((algSc‘𝑃)‘𝑐))) |
73 | 72 | expd 451 |
. . . . . . . . . . . 12
⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) ∧ (𝑦 ∈ (Base‘𝐶) ∧ 𝑥 ∈ (Base‘𝐶))) → (∀𝑖 ∈ 𝑁 ∀𝑗 ∈ 𝑁 ∃𝑎 ∈ (Base‘𝑅)(𝑖𝑥𝑗) = ((algSc‘𝑃)‘𝑎) → (∀𝑖 ∈ 𝑁 ∀𝑗 ∈ 𝑁 ∃𝑏 ∈ (Base‘𝑅)(𝑖𝑦𝑗) = ((algSc‘𝑃)‘𝑏) → ∀𝑖 ∈ 𝑁 ∀𝑗 ∈ 𝑁 ∃𝑐 ∈ (Base‘𝑅)(𝑖(𝑥(+g‘𝐶)𝑦)𝑗) = ((algSc‘𝑃)‘𝑐)))) |
74 | 73 | expr 641 |
. . . . . . . . . . 11
⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) ∧ 𝑦 ∈ (Base‘𝐶)) → (𝑥 ∈ (Base‘𝐶) → (∀𝑖 ∈ 𝑁 ∀𝑗 ∈ 𝑁 ∃𝑎 ∈ (Base‘𝑅)(𝑖𝑥𝑗) = ((algSc‘𝑃)‘𝑎) → (∀𝑖 ∈ 𝑁 ∀𝑗 ∈ 𝑁 ∃𝑏 ∈ (Base‘𝑅)(𝑖𝑦𝑗) = ((algSc‘𝑃)‘𝑏) → ∀𝑖 ∈ 𝑁 ∀𝑗 ∈ 𝑁 ∃𝑐 ∈ (Base‘𝑅)(𝑖(𝑥(+g‘𝐶)𝑦)𝑗) = ((algSc‘𝑃)‘𝑐))))) |
75 | 74 | impd 446 |
. . . . . . . . . 10
⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) ∧ 𝑦 ∈ (Base‘𝐶)) → ((𝑥 ∈ (Base‘𝐶) ∧ ∀𝑖 ∈ 𝑁 ∀𝑗 ∈ 𝑁 ∃𝑎 ∈ (Base‘𝑅)(𝑖𝑥𝑗) = ((algSc‘𝑃)‘𝑎)) → (∀𝑖 ∈ 𝑁 ∀𝑗 ∈ 𝑁 ∃𝑏 ∈ (Base‘𝑅)(𝑖𝑦𝑗) = ((algSc‘𝑃)‘𝑏) → ∀𝑖 ∈ 𝑁 ∀𝑗 ∈ 𝑁 ∃𝑐 ∈ (Base‘𝑅)(𝑖(𝑥(+g‘𝐶)𝑦)𝑗) = ((algSc‘𝑃)‘𝑐)))) |
76 | 75 | ex 449 |
. . . . . . . . 9
⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) → (𝑦 ∈ (Base‘𝐶) → ((𝑥 ∈ (Base‘𝐶) ∧ ∀𝑖 ∈ 𝑁 ∀𝑗 ∈ 𝑁 ∃𝑎 ∈ (Base‘𝑅)(𝑖𝑥𝑗) = ((algSc‘𝑃)‘𝑎)) → (∀𝑖 ∈ 𝑁 ∀𝑗 ∈ 𝑁 ∃𝑏 ∈ (Base‘𝑅)(𝑖𝑦𝑗) = ((algSc‘𝑃)‘𝑏) → ∀𝑖 ∈ 𝑁 ∀𝑗 ∈ 𝑁 ∃𝑐 ∈ (Base‘𝑅)(𝑖(𝑥(+g‘𝐶)𝑦)𝑗) = ((algSc‘𝑃)‘𝑐))))) |
77 | 76 | com34 89 |
. . . . . . . 8
⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) → (𝑦 ∈ (Base‘𝐶) → (∀𝑖 ∈ 𝑁 ∀𝑗 ∈ 𝑁 ∃𝑏 ∈ (Base‘𝑅)(𝑖𝑦𝑗) = ((algSc‘𝑃)‘𝑏) → ((𝑥 ∈ (Base‘𝐶) ∧ ∀𝑖 ∈ 𝑁 ∀𝑗 ∈ 𝑁 ∃𝑎 ∈ (Base‘𝑅)(𝑖𝑥𝑗) = ((algSc‘𝑃)‘𝑎)) → ∀𝑖 ∈ 𝑁 ∀𝑗 ∈ 𝑁 ∃𝑐 ∈ (Base‘𝑅)(𝑖(𝑥(+g‘𝐶)𝑦)𝑗) = ((algSc‘𝑃)‘𝑐))))) |
78 | 77 | impd 446 |
. . . . . . 7
⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) → ((𝑦 ∈ (Base‘𝐶) ∧ ∀𝑖 ∈ 𝑁 ∀𝑗 ∈ 𝑁 ∃𝑏 ∈ (Base‘𝑅)(𝑖𝑦𝑗) = ((algSc‘𝑃)‘𝑏)) → ((𝑥 ∈ (Base‘𝐶) ∧ ∀𝑖 ∈ 𝑁 ∀𝑗 ∈ 𝑁 ∃𝑎 ∈ (Base‘𝑅)(𝑖𝑥𝑗) = ((algSc‘𝑃)‘𝑎)) → ∀𝑖 ∈ 𝑁 ∀𝑗 ∈ 𝑁 ∃𝑐 ∈ (Base‘𝑅)(𝑖(𝑥(+g‘𝐶)𝑦)𝑗) = ((algSc‘𝑃)‘𝑐)))) |
79 | 8, 78 | syld 46 |
. . . . . 6
⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) → (𝑦 ∈ 𝑆 → ((𝑥 ∈ (Base‘𝐶) ∧ ∀𝑖 ∈ 𝑁 ∀𝑗 ∈ 𝑁 ∃𝑎 ∈ (Base‘𝑅)(𝑖𝑥𝑗) = ((algSc‘𝑃)‘𝑎)) → ∀𝑖 ∈ 𝑁 ∀𝑗 ∈ 𝑁 ∃𝑐 ∈ (Base‘𝑅)(𝑖(𝑥(+g‘𝐶)𝑦)𝑗) = ((algSc‘𝑃)‘𝑐)))) |
80 | 79 | com23 84 |
. . . . 5
⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) → ((𝑥 ∈ (Base‘𝐶) ∧ ∀𝑖 ∈ 𝑁 ∀𝑗 ∈ 𝑁 ∃𝑎 ∈ (Base‘𝑅)(𝑖𝑥𝑗) = ((algSc‘𝑃)‘𝑎)) → (𝑦 ∈ 𝑆 → ∀𝑖 ∈ 𝑁 ∀𝑗 ∈ 𝑁 ∃𝑐 ∈ (Base‘𝑅)(𝑖(𝑥(+g‘𝐶)𝑦)𝑗) = ((algSc‘𝑃)‘𝑐)))) |
81 | 7, 80 | syld 46 |
. . . 4
⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) → (𝑥 ∈ 𝑆 → (𝑦 ∈ 𝑆 → ∀𝑖 ∈ 𝑁 ∀𝑗 ∈ 𝑁 ∃𝑐 ∈ (Base‘𝑅)(𝑖(𝑥(+g‘𝐶)𝑦)𝑗) = ((algSc‘𝑃)‘𝑐)))) |
82 | 81 | imp32 448 |
. . 3
⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) ∧ (𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆)) → ∀𝑖 ∈ 𝑁 ∀𝑗 ∈ 𝑁 ∃𝑐 ∈ (Base‘𝑅)(𝑖(𝑥(+g‘𝐶)𝑦)𝑗) = ((algSc‘𝑃)‘𝑐)) |
83 | | simpl 472 |
. . . . 5
⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) → 𝑁 ∈ Fin) |
84 | 83 | adantr 480 |
. . . 4
⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) ∧ (𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆)) → 𝑁 ∈ Fin) |
85 | | simpr 476 |
. . . . 5
⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) → 𝑅 ∈ Ring) |
86 | 85 | adantr 480 |
. . . 4
⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) ∧ (𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆)) → 𝑅 ∈ Ring) |
87 | 2, 3 | pmatring 20317 |
. . . . . 6
⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) → 𝐶 ∈ Ring) |
88 | 87 | adantr 480 |
. . . . 5
⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) ∧ (𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆)) → 𝐶 ∈ Ring) |
89 | | simpl 472 |
. . . . . . . 8
⊢ ((𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆) → 𝑥 ∈ 𝑆) |
90 | 89 | anim2i 591 |
. . . . . . 7
⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) ∧ (𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆)) → ((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) ∧ 𝑥 ∈ 𝑆)) |
91 | | df-3an 1033 |
. . . . . . 7
⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑥 ∈ 𝑆) ↔ ((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) ∧ 𝑥 ∈ 𝑆)) |
92 | 90, 91 | sylibr 223 |
. . . . . 6
⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) ∧ (𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆)) → (𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑥 ∈ 𝑆)) |
93 | 1, 2, 3, 4 | cpmatpmat 20334 |
. . . . . 6
⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑥 ∈ 𝑆) → 𝑥 ∈ (Base‘𝐶)) |
94 | 92, 93 | syl 17 |
. . . . 5
⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) ∧ (𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆)) → 𝑥 ∈ (Base‘𝐶)) |
95 | | simpr 476 |
. . . . . . . 8
⊢ ((𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆) → 𝑦 ∈ 𝑆) |
96 | 95 | anim2i 591 |
. . . . . . 7
⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) ∧ (𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆)) → ((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) ∧ 𝑦 ∈ 𝑆)) |
97 | | df-3an 1033 |
. . . . . . 7
⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑦 ∈ 𝑆) ↔ ((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) ∧ 𝑦 ∈ 𝑆)) |
98 | 96, 97 | sylibr 223 |
. . . . . 6
⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) ∧ (𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆)) → (𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑦 ∈ 𝑆)) |
99 | 1, 2, 3, 4 | cpmatpmat 20334 |
. . . . . 6
⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑦 ∈ 𝑆) → 𝑦 ∈ (Base‘𝐶)) |
100 | 98, 99 | syl 17 |
. . . . 5
⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) ∧ (𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆)) → 𝑦 ∈ (Base‘𝐶)) |
101 | 4, 31 | ringacl 18401 |
. . . . 5
⊢ ((𝐶 ∈ Ring ∧ 𝑥 ∈ (Base‘𝐶) ∧ 𝑦 ∈ (Base‘𝐶)) → (𝑥(+g‘𝐶)𝑦) ∈ (Base‘𝐶)) |
102 | 88, 94, 100, 101 | syl3anc 1318 |
. . . 4
⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) ∧ (𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆)) → (𝑥(+g‘𝐶)𝑦) ∈ (Base‘𝐶)) |
103 | 1, 2, 3, 4, 5, 6 | cpmatel2 20337 |
. . . 4
⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ (𝑥(+g‘𝐶)𝑦) ∈ (Base‘𝐶)) → ((𝑥(+g‘𝐶)𝑦) ∈ 𝑆 ↔ ∀𝑖 ∈ 𝑁 ∀𝑗 ∈ 𝑁 ∃𝑐 ∈ (Base‘𝑅)(𝑖(𝑥(+g‘𝐶)𝑦)𝑗) = ((algSc‘𝑃)‘𝑐))) |
104 | 84, 86, 102, 103 | syl3anc 1318 |
. . 3
⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) ∧ (𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆)) → ((𝑥(+g‘𝐶)𝑦) ∈ 𝑆 ↔ ∀𝑖 ∈ 𝑁 ∀𝑗 ∈ 𝑁 ∃𝑐 ∈ (Base‘𝑅)(𝑖(𝑥(+g‘𝐶)𝑦)𝑗) = ((algSc‘𝑃)‘𝑐))) |
105 | 82, 104 | mpbird 246 |
. 2
⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) ∧ (𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆)) → (𝑥(+g‘𝐶)𝑦) ∈ 𝑆) |
106 | 105 | ralrimivva 2954 |
1
⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) →
∀𝑥 ∈ 𝑆 ∀𝑦 ∈ 𝑆 (𝑥(+g‘𝐶)𝑦) ∈ 𝑆) |