Step |
Hyp |
Ref |
Expression |
1 |
|
cayhamlem2.k |
⊢ 𝐾 = ( Base ‘ 𝑅 ) |
2 |
|
cayhamlem2.a |
⊢ 𝐴 = ( 𝑁 Mat 𝑅 ) |
3 |
|
cayhamlem2.b |
⊢ 𝐵 = ( Base ‘ 𝐴 ) |
4 |
|
cayhamlem2.1 |
⊢ 1 = ( 1r ‘ 𝐴 ) |
5 |
|
cayhamlem2.m |
⊢ ∗ = ( ·𝑠 ‘ 𝐴 ) |
6 |
|
cayhamlem2.e |
⊢ ↑ = ( .g ‘ ( mulGrp ‘ 𝐴 ) ) |
7 |
|
cayhamlem2.r |
⊢ · = ( .r ‘ 𝐴 ) |
8 |
|
elmapi |
⊢ ( 𝐻 ∈ ( 𝐾 ↑m ℕ0 ) → 𝐻 : ℕ0 ⟶ 𝐾 ) |
9 |
8
|
ffvelrnda |
⊢ ( ( 𝐻 ∈ ( 𝐾 ↑m ℕ0 ) ∧ 𝐿 ∈ ℕ0 ) → ( 𝐻 ‘ 𝐿 ) ∈ 𝐾 ) |
10 |
9
|
adantl |
⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) ∧ ( 𝐻 ∈ ( 𝐾 ↑m ℕ0 ) ∧ 𝐿 ∈ ℕ0 ) ) → ( 𝐻 ‘ 𝐿 ) ∈ 𝐾 ) |
11 |
2
|
matsca2 |
⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ) → 𝑅 = ( Scalar ‘ 𝐴 ) ) |
12 |
11
|
3adant3 |
⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) → 𝑅 = ( Scalar ‘ 𝐴 ) ) |
13 |
12
|
fveq2d |
⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) → ( Base ‘ 𝑅 ) = ( Base ‘ ( Scalar ‘ 𝐴 ) ) ) |
14 |
1 13
|
syl5req |
⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) → ( Base ‘ ( Scalar ‘ 𝐴 ) ) = 𝐾 ) |
15 |
14
|
eleq2d |
⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) → ( ( 𝐻 ‘ 𝐿 ) ∈ ( Base ‘ ( Scalar ‘ 𝐴 ) ) ↔ ( 𝐻 ‘ 𝐿 ) ∈ 𝐾 ) ) |
16 |
15
|
adantr |
⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) ∧ ( 𝐻 ∈ ( 𝐾 ↑m ℕ0 ) ∧ 𝐿 ∈ ℕ0 ) ) → ( ( 𝐻 ‘ 𝐿 ) ∈ ( Base ‘ ( Scalar ‘ 𝐴 ) ) ↔ ( 𝐻 ‘ 𝐿 ) ∈ 𝐾 ) ) |
17 |
10 16
|
mpbird |
⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) ∧ ( 𝐻 ∈ ( 𝐾 ↑m ℕ0 ) ∧ 𝐿 ∈ ℕ0 ) ) → ( 𝐻 ‘ 𝐿 ) ∈ ( Base ‘ ( Scalar ‘ 𝐴 ) ) ) |
18 |
|
eqid |
⊢ ( algSc ‘ 𝐴 ) = ( algSc ‘ 𝐴 ) |
19 |
|
eqid |
⊢ ( Scalar ‘ 𝐴 ) = ( Scalar ‘ 𝐴 ) |
20 |
|
eqid |
⊢ ( Base ‘ ( Scalar ‘ 𝐴 ) ) = ( Base ‘ ( Scalar ‘ 𝐴 ) ) |
21 |
18 19 20 5 4
|
asclval |
⊢ ( ( 𝐻 ‘ 𝐿 ) ∈ ( Base ‘ ( Scalar ‘ 𝐴 ) ) → ( ( algSc ‘ 𝐴 ) ‘ ( 𝐻 ‘ 𝐿 ) ) = ( ( 𝐻 ‘ 𝐿 ) ∗ 1 ) ) |
22 |
17 21
|
syl |
⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) ∧ ( 𝐻 ∈ ( 𝐾 ↑m ℕ0 ) ∧ 𝐿 ∈ ℕ0 ) ) → ( ( algSc ‘ 𝐴 ) ‘ ( 𝐻 ‘ 𝐿 ) ) = ( ( 𝐻 ‘ 𝐿 ) ∗ 1 ) ) |
23 |
22
|
eqcomd |
⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) ∧ ( 𝐻 ∈ ( 𝐾 ↑m ℕ0 ) ∧ 𝐿 ∈ ℕ0 ) ) → ( ( 𝐻 ‘ 𝐿 ) ∗ 1 ) = ( ( algSc ‘ 𝐴 ) ‘ ( 𝐻 ‘ 𝐿 ) ) ) |
24 |
23
|
oveq2d |
⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) ∧ ( 𝐻 ∈ ( 𝐾 ↑m ℕ0 ) ∧ 𝐿 ∈ ℕ0 ) ) → ( ( 𝐿 ↑ 𝑀 ) · ( ( 𝐻 ‘ 𝐿 ) ∗ 1 ) ) = ( ( 𝐿 ↑ 𝑀 ) · ( ( algSc ‘ 𝐴 ) ‘ ( 𝐻 ‘ 𝐿 ) ) ) ) |
25 |
2
|
matassa |
⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ) → 𝐴 ∈ AssAlg ) |
26 |
25
|
3adant3 |
⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) → 𝐴 ∈ AssAlg ) |
27 |
26
|
adantr |
⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) ∧ ( 𝐻 ∈ ( 𝐾 ↑m ℕ0 ) ∧ 𝐿 ∈ ℕ0 ) ) → 𝐴 ∈ AssAlg ) |
28 |
|
crngring |
⊢ ( 𝑅 ∈ CRing → 𝑅 ∈ Ring ) |
29 |
28
|
anim2i |
⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ) → ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ) |
30 |
29
|
3adant3 |
⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) → ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ) |
31 |
2
|
matring |
⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) → 𝐴 ∈ Ring ) |
32 |
|
eqid |
⊢ ( mulGrp ‘ 𝐴 ) = ( mulGrp ‘ 𝐴 ) |
33 |
32
|
ringmgp |
⊢ ( 𝐴 ∈ Ring → ( mulGrp ‘ 𝐴 ) ∈ Mnd ) |
34 |
30 31 33
|
3syl |
⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) → ( mulGrp ‘ 𝐴 ) ∈ Mnd ) |
35 |
34
|
adantr |
⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) ∧ ( 𝐻 ∈ ( 𝐾 ↑m ℕ0 ) ∧ 𝐿 ∈ ℕ0 ) ) → ( mulGrp ‘ 𝐴 ) ∈ Mnd ) |
36 |
|
simprr |
⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) ∧ ( 𝐻 ∈ ( 𝐾 ↑m ℕ0 ) ∧ 𝐿 ∈ ℕ0 ) ) → 𝐿 ∈ ℕ0 ) |
37 |
|
simpl3 |
⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) ∧ ( 𝐻 ∈ ( 𝐾 ↑m ℕ0 ) ∧ 𝐿 ∈ ℕ0 ) ) → 𝑀 ∈ 𝐵 ) |
38 |
32 3
|
mgpbas |
⊢ 𝐵 = ( Base ‘ ( mulGrp ‘ 𝐴 ) ) |
39 |
38 6
|
mulgnn0cl |
⊢ ( ( ( mulGrp ‘ 𝐴 ) ∈ Mnd ∧ 𝐿 ∈ ℕ0 ∧ 𝑀 ∈ 𝐵 ) → ( 𝐿 ↑ 𝑀 ) ∈ 𝐵 ) |
40 |
35 36 37 39
|
syl3anc |
⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) ∧ ( 𝐻 ∈ ( 𝐾 ↑m ℕ0 ) ∧ 𝐿 ∈ ℕ0 ) ) → ( 𝐿 ↑ 𝑀 ) ∈ 𝐵 ) |
41 |
18 19 20 3 7 5
|
asclmul2 |
⊢ ( ( 𝐴 ∈ AssAlg ∧ ( 𝐻 ‘ 𝐿 ) ∈ ( Base ‘ ( Scalar ‘ 𝐴 ) ) ∧ ( 𝐿 ↑ 𝑀 ) ∈ 𝐵 ) → ( ( 𝐿 ↑ 𝑀 ) · ( ( algSc ‘ 𝐴 ) ‘ ( 𝐻 ‘ 𝐿 ) ) ) = ( ( 𝐻 ‘ 𝐿 ) ∗ ( 𝐿 ↑ 𝑀 ) ) ) |
42 |
27 17 40 41
|
syl3anc |
⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) ∧ ( 𝐻 ∈ ( 𝐾 ↑m ℕ0 ) ∧ 𝐿 ∈ ℕ0 ) ) → ( ( 𝐿 ↑ 𝑀 ) · ( ( algSc ‘ 𝐴 ) ‘ ( 𝐻 ‘ 𝐿 ) ) ) = ( ( 𝐻 ‘ 𝐿 ) ∗ ( 𝐿 ↑ 𝑀 ) ) ) |
43 |
24 42
|
eqtr2d |
⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) ∧ ( 𝐻 ∈ ( 𝐾 ↑m ℕ0 ) ∧ 𝐿 ∈ ℕ0 ) ) → ( ( 𝐻 ‘ 𝐿 ) ∗ ( 𝐿 ↑ 𝑀 ) ) = ( ( 𝐿 ↑ 𝑀 ) · ( ( 𝐻 ‘ 𝐿 ) ∗ 1 ) ) ) |