Step |
Hyp |
Ref |
Expression |
1 |
|
mat2pmatbas.t |
⊢ 𝑇 = ( 𝑁 matToPolyMat 𝑅 ) |
2 |
|
mat2pmatbas.a |
⊢ 𝐴 = ( 𝑁 Mat 𝑅 ) |
3 |
|
mat2pmatbas.b |
⊢ 𝐵 = ( Base ‘ 𝐴 ) |
4 |
|
mat2pmatbas.p |
⊢ 𝑃 = ( Poly1 ‘ 𝑅 ) |
5 |
|
mat2pmatbas.c |
⊢ 𝐶 = ( 𝑁 Mat 𝑃 ) |
6 |
|
mat2pmatbas0.h |
⊢ 𝐻 = ( Base ‘ 𝐶 ) |
7 |
|
eqid |
⊢ ( +g ‘ 𝐴 ) = ( +g ‘ 𝐴 ) |
8 |
|
eqid |
⊢ ( +g ‘ 𝐶 ) = ( +g ‘ 𝐶 ) |
9 |
2
|
matgrp |
⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) → 𝐴 ∈ Grp ) |
10 |
4 5
|
pmatring |
⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) → 𝐶 ∈ Ring ) |
11 |
|
ringgrp |
⊢ ( 𝐶 ∈ Ring → 𝐶 ∈ Grp ) |
12 |
10 11
|
syl |
⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) → 𝐶 ∈ Grp ) |
13 |
1 2 3 4 5 6
|
mat2pmatf |
⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) → 𝑇 : 𝐵 ⟶ 𝐻 ) |
14 |
|
eqid |
⊢ ( Base ‘ 𝑃 ) = ( Base ‘ 𝑃 ) |
15 |
|
simpl |
⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) → 𝑁 ∈ Fin ) |
16 |
15
|
adantr |
⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ) → 𝑁 ∈ Fin ) |
17 |
4
|
ply1ring |
⊢ ( 𝑅 ∈ Ring → 𝑃 ∈ Ring ) |
18 |
17
|
ad2antlr |
⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ) → 𝑃 ∈ Ring ) |
19 |
|
simp1lr |
⊢ ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ) ∧ 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁 ) → 𝑅 ∈ Ring ) |
20 |
|
eqid |
⊢ ( Base ‘ 𝑅 ) = ( Base ‘ 𝑅 ) |
21 |
|
simp2 |
⊢ ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ) ∧ 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁 ) → 𝑖 ∈ 𝑁 ) |
22 |
|
simp3 |
⊢ ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ) ∧ 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁 ) → 𝑗 ∈ 𝑁 ) |
23 |
|
simp1rl |
⊢ ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ) ∧ 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁 ) → 𝑥 ∈ 𝐵 ) |
24 |
2 20 3 21 22 23
|
matecld |
⊢ ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ) ∧ 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁 ) → ( 𝑖 𝑥 𝑗 ) ∈ ( Base ‘ 𝑅 ) ) |
25 |
|
eqid |
⊢ ( algSc ‘ 𝑃 ) = ( algSc ‘ 𝑃 ) |
26 |
4 25 20 14
|
ply1sclcl |
⊢ ( ( 𝑅 ∈ Ring ∧ ( 𝑖 𝑥 𝑗 ) ∈ ( Base ‘ 𝑅 ) ) → ( ( algSc ‘ 𝑃 ) ‘ ( 𝑖 𝑥 𝑗 ) ) ∈ ( Base ‘ 𝑃 ) ) |
27 |
19 24 26
|
syl2anc |
⊢ ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ) ∧ 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁 ) → ( ( algSc ‘ 𝑃 ) ‘ ( 𝑖 𝑥 𝑗 ) ) ∈ ( Base ‘ 𝑃 ) ) |
28 |
5 14 6 16 18 27
|
matbas2d |
⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ) → ( 𝑖 ∈ 𝑁 , 𝑗 ∈ 𝑁 ↦ ( ( algSc ‘ 𝑃 ) ‘ ( 𝑖 𝑥 𝑗 ) ) ) ∈ 𝐻 ) |
29 |
|
simp1rr |
⊢ ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ) ∧ 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁 ) → 𝑦 ∈ 𝐵 ) |
30 |
2 20 3 21 22 29
|
matecld |
⊢ ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ) ∧ 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁 ) → ( 𝑖 𝑦 𝑗 ) ∈ ( Base ‘ 𝑅 ) ) |
31 |
4 25 20 14
|
ply1sclcl |
⊢ ( ( 𝑅 ∈ Ring ∧ ( 𝑖 𝑦 𝑗 ) ∈ ( Base ‘ 𝑅 ) ) → ( ( algSc ‘ 𝑃 ) ‘ ( 𝑖 𝑦 𝑗 ) ) ∈ ( Base ‘ 𝑃 ) ) |
32 |
19 30 31
|
syl2anc |
⊢ ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ) ∧ 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁 ) → ( ( algSc ‘ 𝑃 ) ‘ ( 𝑖 𝑦 𝑗 ) ) ∈ ( Base ‘ 𝑃 ) ) |
33 |
5 14 6 16 18 32
|
matbas2d |
⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ) → ( 𝑖 ∈ 𝑁 , 𝑗 ∈ 𝑁 ↦ ( ( algSc ‘ 𝑃 ) ‘ ( 𝑖 𝑦 𝑗 ) ) ) ∈ 𝐻 ) |
34 |
|
eqid |
⊢ ( +g ‘ 𝑃 ) = ( +g ‘ 𝑃 ) |
35 |
5 6 8 34
|
matplusg2 |
⊢ ( ( ( 𝑖 ∈ 𝑁 , 𝑗 ∈ 𝑁 ↦ ( ( algSc ‘ 𝑃 ) ‘ ( 𝑖 𝑥 𝑗 ) ) ) ∈ 𝐻 ∧ ( 𝑖 ∈ 𝑁 , 𝑗 ∈ 𝑁 ↦ ( ( algSc ‘ 𝑃 ) ‘ ( 𝑖 𝑦 𝑗 ) ) ) ∈ 𝐻 ) → ( ( 𝑖 ∈ 𝑁 , 𝑗 ∈ 𝑁 ↦ ( ( algSc ‘ 𝑃 ) ‘ ( 𝑖 𝑥 𝑗 ) ) ) ( +g ‘ 𝐶 ) ( 𝑖 ∈ 𝑁 , 𝑗 ∈ 𝑁 ↦ ( ( algSc ‘ 𝑃 ) ‘ ( 𝑖 𝑦 𝑗 ) ) ) ) = ( ( 𝑖 ∈ 𝑁 , 𝑗 ∈ 𝑁 ↦ ( ( algSc ‘ 𝑃 ) ‘ ( 𝑖 𝑥 𝑗 ) ) ) ∘f ( +g ‘ 𝑃 ) ( 𝑖 ∈ 𝑁 , 𝑗 ∈ 𝑁 ↦ ( ( algSc ‘ 𝑃 ) ‘ ( 𝑖 𝑦 𝑗 ) ) ) ) ) |
36 |
28 33 35
|
syl2anc |
⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ) → ( ( 𝑖 ∈ 𝑁 , 𝑗 ∈ 𝑁 ↦ ( ( algSc ‘ 𝑃 ) ‘ ( 𝑖 𝑥 𝑗 ) ) ) ( +g ‘ 𝐶 ) ( 𝑖 ∈ 𝑁 , 𝑗 ∈ 𝑁 ↦ ( ( algSc ‘ 𝑃 ) ‘ ( 𝑖 𝑦 𝑗 ) ) ) ) = ( ( 𝑖 ∈ 𝑁 , 𝑗 ∈ 𝑁 ↦ ( ( algSc ‘ 𝑃 ) ‘ ( 𝑖 𝑥 𝑗 ) ) ) ∘f ( +g ‘ 𝑃 ) ( 𝑖 ∈ 𝑁 , 𝑗 ∈ 𝑁 ↦ ( ( algSc ‘ 𝑃 ) ‘ ( 𝑖 𝑦 𝑗 ) ) ) ) ) |
37 |
|
fvexd |
⊢ ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ) ∧ 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁 ) → ( ( algSc ‘ 𝑃 ) ‘ ( 𝑖 𝑥 𝑗 ) ) ∈ V ) |
38 |
|
fvexd |
⊢ ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ) ∧ 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁 ) → ( ( algSc ‘ 𝑃 ) ‘ ( 𝑖 𝑦 𝑗 ) ) ∈ V ) |
39 |
|
eqidd |
⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ) → ( 𝑖 ∈ 𝑁 , 𝑗 ∈ 𝑁 ↦ ( ( algSc ‘ 𝑃 ) ‘ ( 𝑖 𝑥 𝑗 ) ) ) = ( 𝑖 ∈ 𝑁 , 𝑗 ∈ 𝑁 ↦ ( ( algSc ‘ 𝑃 ) ‘ ( 𝑖 𝑥 𝑗 ) ) ) ) |
40 |
|
eqidd |
⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ) → ( 𝑖 ∈ 𝑁 , 𝑗 ∈ 𝑁 ↦ ( ( algSc ‘ 𝑃 ) ‘ ( 𝑖 𝑦 𝑗 ) ) ) = ( 𝑖 ∈ 𝑁 , 𝑗 ∈ 𝑁 ↦ ( ( algSc ‘ 𝑃 ) ‘ ( 𝑖 𝑦 𝑗 ) ) ) ) |
41 |
16 16 37 38 39 40
|
offval22 |
⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ) → ( ( 𝑖 ∈ 𝑁 , 𝑗 ∈ 𝑁 ↦ ( ( algSc ‘ 𝑃 ) ‘ ( 𝑖 𝑥 𝑗 ) ) ) ∘f ( +g ‘ 𝑃 ) ( 𝑖 ∈ 𝑁 , 𝑗 ∈ 𝑁 ↦ ( ( algSc ‘ 𝑃 ) ‘ ( 𝑖 𝑦 𝑗 ) ) ) ) = ( 𝑖 ∈ 𝑁 , 𝑗 ∈ 𝑁 ↦ ( ( ( algSc ‘ 𝑃 ) ‘ ( 𝑖 𝑥 𝑗 ) ) ( +g ‘ 𝑃 ) ( ( algSc ‘ 𝑃 ) ‘ ( 𝑖 𝑦 𝑗 ) ) ) ) ) |
42 |
|
simpr |
⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ) → ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ) |
43 |
42
|
3ad2ant1 |
⊢ ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ) ∧ 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁 ) → ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ) |
44 |
|
3simpc |
⊢ ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ) ∧ 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁 ) → ( 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁 ) ) |
45 |
|
eqid |
⊢ ( +g ‘ 𝑅 ) = ( +g ‘ 𝑅 ) |
46 |
2 3 7 45
|
matplusgcell |
⊢ ( ( ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ∧ ( 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁 ) ) → ( 𝑖 ( 𝑥 ( +g ‘ 𝐴 ) 𝑦 ) 𝑗 ) = ( ( 𝑖 𝑥 𝑗 ) ( +g ‘ 𝑅 ) ( 𝑖 𝑦 𝑗 ) ) ) |
47 |
43 44 46
|
syl2anc |
⊢ ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ) ∧ 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁 ) → ( 𝑖 ( 𝑥 ( +g ‘ 𝐴 ) 𝑦 ) 𝑗 ) = ( ( 𝑖 𝑥 𝑗 ) ( +g ‘ 𝑅 ) ( 𝑖 𝑦 𝑗 ) ) ) |
48 |
4
|
ply1sca |
⊢ ( 𝑅 ∈ Ring → 𝑅 = ( Scalar ‘ 𝑃 ) ) |
49 |
48
|
adantl |
⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) → 𝑅 = ( Scalar ‘ 𝑃 ) ) |
50 |
49
|
fveq2d |
⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) → ( +g ‘ 𝑅 ) = ( +g ‘ ( Scalar ‘ 𝑃 ) ) ) |
51 |
50
|
oveqd |
⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) → ( ( 𝑖 𝑥 𝑗 ) ( +g ‘ 𝑅 ) ( 𝑖 𝑦 𝑗 ) ) = ( ( 𝑖 𝑥 𝑗 ) ( +g ‘ ( Scalar ‘ 𝑃 ) ) ( 𝑖 𝑦 𝑗 ) ) ) |
52 |
51
|
adantr |
⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ) → ( ( 𝑖 𝑥 𝑗 ) ( +g ‘ 𝑅 ) ( 𝑖 𝑦 𝑗 ) ) = ( ( 𝑖 𝑥 𝑗 ) ( +g ‘ ( Scalar ‘ 𝑃 ) ) ( 𝑖 𝑦 𝑗 ) ) ) |
53 |
52
|
3ad2ant1 |
⊢ ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ) ∧ 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁 ) → ( ( 𝑖 𝑥 𝑗 ) ( +g ‘ 𝑅 ) ( 𝑖 𝑦 𝑗 ) ) = ( ( 𝑖 𝑥 𝑗 ) ( +g ‘ ( Scalar ‘ 𝑃 ) ) ( 𝑖 𝑦 𝑗 ) ) ) |
54 |
47 53
|
eqtrd |
⊢ ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ) ∧ 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁 ) → ( 𝑖 ( 𝑥 ( +g ‘ 𝐴 ) 𝑦 ) 𝑗 ) = ( ( 𝑖 𝑥 𝑗 ) ( +g ‘ ( Scalar ‘ 𝑃 ) ) ( 𝑖 𝑦 𝑗 ) ) ) |
55 |
54
|
fveq2d |
⊢ ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ) ∧ 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁 ) → ( ( algSc ‘ 𝑃 ) ‘ ( 𝑖 ( 𝑥 ( +g ‘ 𝐴 ) 𝑦 ) 𝑗 ) ) = ( ( algSc ‘ 𝑃 ) ‘ ( ( 𝑖 𝑥 𝑗 ) ( +g ‘ ( Scalar ‘ 𝑃 ) ) ( 𝑖 𝑦 𝑗 ) ) ) ) |
56 |
|
eqid |
⊢ ( Scalar ‘ 𝑃 ) = ( Scalar ‘ 𝑃 ) |
57 |
18
|
3ad2ant1 |
⊢ ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ) ∧ 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁 ) → 𝑃 ∈ Ring ) |
58 |
4
|
ply1lmod |
⊢ ( 𝑅 ∈ Ring → 𝑃 ∈ LMod ) |
59 |
58
|
ad2antlr |
⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ) → 𝑃 ∈ LMod ) |
60 |
59
|
3ad2ant1 |
⊢ ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ) ∧ 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁 ) → 𝑃 ∈ LMod ) |
61 |
25 56 57 60
|
asclghm |
⊢ ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ) ∧ 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁 ) → ( algSc ‘ 𝑃 ) ∈ ( ( Scalar ‘ 𝑃 ) GrpHom 𝑃 ) ) |
62 |
49
|
eqcomd |
⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) → ( Scalar ‘ 𝑃 ) = 𝑅 ) |
63 |
62
|
fveq2d |
⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) → ( Base ‘ ( Scalar ‘ 𝑃 ) ) = ( Base ‘ 𝑅 ) ) |
64 |
63
|
eleq2d |
⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) → ( ( 𝑖 𝑥 𝑗 ) ∈ ( Base ‘ ( Scalar ‘ 𝑃 ) ) ↔ ( 𝑖 𝑥 𝑗 ) ∈ ( Base ‘ 𝑅 ) ) ) |
65 |
64
|
adantr |
⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ) → ( ( 𝑖 𝑥 𝑗 ) ∈ ( Base ‘ ( Scalar ‘ 𝑃 ) ) ↔ ( 𝑖 𝑥 𝑗 ) ∈ ( Base ‘ 𝑅 ) ) ) |
66 |
65
|
3ad2ant1 |
⊢ ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ) ∧ 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁 ) → ( ( 𝑖 𝑥 𝑗 ) ∈ ( Base ‘ ( Scalar ‘ 𝑃 ) ) ↔ ( 𝑖 𝑥 𝑗 ) ∈ ( Base ‘ 𝑅 ) ) ) |
67 |
24 66
|
mpbird |
⊢ ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ) ∧ 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁 ) → ( 𝑖 𝑥 𝑗 ) ∈ ( Base ‘ ( Scalar ‘ 𝑃 ) ) ) |
68 |
63
|
eleq2d |
⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) → ( ( 𝑖 𝑦 𝑗 ) ∈ ( Base ‘ ( Scalar ‘ 𝑃 ) ) ↔ ( 𝑖 𝑦 𝑗 ) ∈ ( Base ‘ 𝑅 ) ) ) |
69 |
68
|
adantr |
⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ) → ( ( 𝑖 𝑦 𝑗 ) ∈ ( Base ‘ ( Scalar ‘ 𝑃 ) ) ↔ ( 𝑖 𝑦 𝑗 ) ∈ ( Base ‘ 𝑅 ) ) ) |
70 |
69
|
3ad2ant1 |
⊢ ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ) ∧ 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁 ) → ( ( 𝑖 𝑦 𝑗 ) ∈ ( Base ‘ ( Scalar ‘ 𝑃 ) ) ↔ ( 𝑖 𝑦 𝑗 ) ∈ ( Base ‘ 𝑅 ) ) ) |
71 |
30 70
|
mpbird |
⊢ ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ) ∧ 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁 ) → ( 𝑖 𝑦 𝑗 ) ∈ ( Base ‘ ( Scalar ‘ 𝑃 ) ) ) |
72 |
|
eqid |
⊢ ( Base ‘ ( Scalar ‘ 𝑃 ) ) = ( Base ‘ ( Scalar ‘ 𝑃 ) ) |
73 |
|
eqid |
⊢ ( +g ‘ ( Scalar ‘ 𝑃 ) ) = ( +g ‘ ( Scalar ‘ 𝑃 ) ) |
74 |
72 73 34
|
ghmlin |
⊢ ( ( ( algSc ‘ 𝑃 ) ∈ ( ( Scalar ‘ 𝑃 ) GrpHom 𝑃 ) ∧ ( 𝑖 𝑥 𝑗 ) ∈ ( Base ‘ ( Scalar ‘ 𝑃 ) ) ∧ ( 𝑖 𝑦 𝑗 ) ∈ ( Base ‘ ( Scalar ‘ 𝑃 ) ) ) → ( ( algSc ‘ 𝑃 ) ‘ ( ( 𝑖 𝑥 𝑗 ) ( +g ‘ ( Scalar ‘ 𝑃 ) ) ( 𝑖 𝑦 𝑗 ) ) ) = ( ( ( algSc ‘ 𝑃 ) ‘ ( 𝑖 𝑥 𝑗 ) ) ( +g ‘ 𝑃 ) ( ( algSc ‘ 𝑃 ) ‘ ( 𝑖 𝑦 𝑗 ) ) ) ) |
75 |
61 67 71 74
|
syl3anc |
⊢ ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ) ∧ 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁 ) → ( ( algSc ‘ 𝑃 ) ‘ ( ( 𝑖 𝑥 𝑗 ) ( +g ‘ ( Scalar ‘ 𝑃 ) ) ( 𝑖 𝑦 𝑗 ) ) ) = ( ( ( algSc ‘ 𝑃 ) ‘ ( 𝑖 𝑥 𝑗 ) ) ( +g ‘ 𝑃 ) ( ( algSc ‘ 𝑃 ) ‘ ( 𝑖 𝑦 𝑗 ) ) ) ) |
76 |
55 75
|
eqtr2d |
⊢ ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ) ∧ 𝑖 ∈ 𝑁 ∧ 𝑗 ∈ 𝑁 ) → ( ( ( algSc ‘ 𝑃 ) ‘ ( 𝑖 𝑥 𝑗 ) ) ( +g ‘ 𝑃 ) ( ( algSc ‘ 𝑃 ) ‘ ( 𝑖 𝑦 𝑗 ) ) ) = ( ( algSc ‘ 𝑃 ) ‘ ( 𝑖 ( 𝑥 ( +g ‘ 𝐴 ) 𝑦 ) 𝑗 ) ) ) |
77 |
76
|
mpoeq3dva |
⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ) → ( 𝑖 ∈ 𝑁 , 𝑗 ∈ 𝑁 ↦ ( ( ( algSc ‘ 𝑃 ) ‘ ( 𝑖 𝑥 𝑗 ) ) ( +g ‘ 𝑃 ) ( ( algSc ‘ 𝑃 ) ‘ ( 𝑖 𝑦 𝑗 ) ) ) ) = ( 𝑖 ∈ 𝑁 , 𝑗 ∈ 𝑁 ↦ ( ( algSc ‘ 𝑃 ) ‘ ( 𝑖 ( 𝑥 ( +g ‘ 𝐴 ) 𝑦 ) 𝑗 ) ) ) ) |
78 |
41 77
|
eqtrd |
⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ) → ( ( 𝑖 ∈ 𝑁 , 𝑗 ∈ 𝑁 ↦ ( ( algSc ‘ 𝑃 ) ‘ ( 𝑖 𝑥 𝑗 ) ) ) ∘f ( +g ‘ 𝑃 ) ( 𝑖 ∈ 𝑁 , 𝑗 ∈ 𝑁 ↦ ( ( algSc ‘ 𝑃 ) ‘ ( 𝑖 𝑦 𝑗 ) ) ) ) = ( 𝑖 ∈ 𝑁 , 𝑗 ∈ 𝑁 ↦ ( ( algSc ‘ 𝑃 ) ‘ ( 𝑖 ( 𝑥 ( +g ‘ 𝐴 ) 𝑦 ) 𝑗 ) ) ) ) |
79 |
36 78
|
eqtr2d |
⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ) → ( 𝑖 ∈ 𝑁 , 𝑗 ∈ 𝑁 ↦ ( ( algSc ‘ 𝑃 ) ‘ ( 𝑖 ( 𝑥 ( +g ‘ 𝐴 ) 𝑦 ) 𝑗 ) ) ) = ( ( 𝑖 ∈ 𝑁 , 𝑗 ∈ 𝑁 ↦ ( ( algSc ‘ 𝑃 ) ‘ ( 𝑖 𝑥 𝑗 ) ) ) ( +g ‘ 𝐶 ) ( 𝑖 ∈ 𝑁 , 𝑗 ∈ 𝑁 ↦ ( ( algSc ‘ 𝑃 ) ‘ ( 𝑖 𝑦 𝑗 ) ) ) ) ) |
80 |
|
simpl |
⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ) → ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ) |
81 |
2
|
matring |
⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) → 𝐴 ∈ Ring ) |
82 |
|
ringmnd |
⊢ ( 𝐴 ∈ Ring → 𝐴 ∈ Mnd ) |
83 |
81 82
|
syl |
⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) → 𝐴 ∈ Mnd ) |
84 |
83
|
anim1i |
⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ) → ( 𝐴 ∈ Mnd ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ) ) |
85 |
|
3anass |
⊢ ( ( 𝐴 ∈ Mnd ∧ 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ↔ ( 𝐴 ∈ Mnd ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ) ) |
86 |
84 85
|
sylibr |
⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ) → ( 𝐴 ∈ Mnd ∧ 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ) |
87 |
3 7
|
mndcl |
⊢ ( ( 𝐴 ∈ Mnd ∧ 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) → ( 𝑥 ( +g ‘ 𝐴 ) 𝑦 ) ∈ 𝐵 ) |
88 |
86 87
|
syl |
⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ) → ( 𝑥 ( +g ‘ 𝐴 ) 𝑦 ) ∈ 𝐵 ) |
89 |
|
df-3an |
⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ ( 𝑥 ( +g ‘ 𝐴 ) 𝑦 ) ∈ 𝐵 ) ↔ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ ( 𝑥 ( +g ‘ 𝐴 ) 𝑦 ) ∈ 𝐵 ) ) |
90 |
80 88 89
|
sylanbrc |
⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ) → ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ ( 𝑥 ( +g ‘ 𝐴 ) 𝑦 ) ∈ 𝐵 ) ) |
91 |
1 2 3 4 25
|
mat2pmatval |
⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ ( 𝑥 ( +g ‘ 𝐴 ) 𝑦 ) ∈ 𝐵 ) → ( 𝑇 ‘ ( 𝑥 ( +g ‘ 𝐴 ) 𝑦 ) ) = ( 𝑖 ∈ 𝑁 , 𝑗 ∈ 𝑁 ↦ ( ( algSc ‘ 𝑃 ) ‘ ( 𝑖 ( 𝑥 ( +g ‘ 𝐴 ) 𝑦 ) 𝑗 ) ) ) ) |
92 |
90 91
|
syl |
⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ) → ( 𝑇 ‘ ( 𝑥 ( +g ‘ 𝐴 ) 𝑦 ) ) = ( 𝑖 ∈ 𝑁 , 𝑗 ∈ 𝑁 ↦ ( ( algSc ‘ 𝑃 ) ‘ ( 𝑖 ( 𝑥 ( +g ‘ 𝐴 ) 𝑦 ) 𝑗 ) ) ) ) |
93 |
|
simpl |
⊢ ( ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) → 𝑥 ∈ 𝐵 ) |
94 |
93
|
anim2i |
⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ) → ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ 𝑥 ∈ 𝐵 ) ) |
95 |
|
df-3an |
⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑥 ∈ 𝐵 ) ↔ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ 𝑥 ∈ 𝐵 ) ) |
96 |
94 95
|
sylibr |
⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ) → ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑥 ∈ 𝐵 ) ) |
97 |
1 2 3 4 25
|
mat2pmatval |
⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑥 ∈ 𝐵 ) → ( 𝑇 ‘ 𝑥 ) = ( 𝑖 ∈ 𝑁 , 𝑗 ∈ 𝑁 ↦ ( ( algSc ‘ 𝑃 ) ‘ ( 𝑖 𝑥 𝑗 ) ) ) ) |
98 |
96 97
|
syl |
⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ) → ( 𝑇 ‘ 𝑥 ) = ( 𝑖 ∈ 𝑁 , 𝑗 ∈ 𝑁 ↦ ( ( algSc ‘ 𝑃 ) ‘ ( 𝑖 𝑥 𝑗 ) ) ) ) |
99 |
|
simpr |
⊢ ( ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) → 𝑦 ∈ 𝐵 ) |
100 |
99
|
anim2i |
⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ) → ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ 𝑦 ∈ 𝐵 ) ) |
101 |
|
df-3an |
⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑦 ∈ 𝐵 ) ↔ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ 𝑦 ∈ 𝐵 ) ) |
102 |
100 101
|
sylibr |
⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ) → ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑦 ∈ 𝐵 ) ) |
103 |
1 2 3 4 25
|
mat2pmatval |
⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑦 ∈ 𝐵 ) → ( 𝑇 ‘ 𝑦 ) = ( 𝑖 ∈ 𝑁 , 𝑗 ∈ 𝑁 ↦ ( ( algSc ‘ 𝑃 ) ‘ ( 𝑖 𝑦 𝑗 ) ) ) ) |
104 |
102 103
|
syl |
⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ) → ( 𝑇 ‘ 𝑦 ) = ( 𝑖 ∈ 𝑁 , 𝑗 ∈ 𝑁 ↦ ( ( algSc ‘ 𝑃 ) ‘ ( 𝑖 𝑦 𝑗 ) ) ) ) |
105 |
98 104
|
oveq12d |
⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ) → ( ( 𝑇 ‘ 𝑥 ) ( +g ‘ 𝐶 ) ( 𝑇 ‘ 𝑦 ) ) = ( ( 𝑖 ∈ 𝑁 , 𝑗 ∈ 𝑁 ↦ ( ( algSc ‘ 𝑃 ) ‘ ( 𝑖 𝑥 𝑗 ) ) ) ( +g ‘ 𝐶 ) ( 𝑖 ∈ 𝑁 , 𝑗 ∈ 𝑁 ↦ ( ( algSc ‘ 𝑃 ) ‘ ( 𝑖 𝑦 𝑗 ) ) ) ) ) |
106 |
79 92 105
|
3eqtr4d |
⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ) → ( 𝑇 ‘ ( 𝑥 ( +g ‘ 𝐴 ) 𝑦 ) ) = ( ( 𝑇 ‘ 𝑥 ) ( +g ‘ 𝐶 ) ( 𝑇 ‘ 𝑦 ) ) ) |
107 |
3 6 7 8 9 12 13 106
|
isghmd |
⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) → 𝑇 ∈ ( 𝐴 GrpHom 𝐶 ) ) |