Metamath Proof Explorer

Theorem cayhamlem2

Description: Lemma for cayhamlem3 . (Contributed by AV, 24-Nov-2019)

Ref Expression
Hypotheses cayhamlem2.k ⊢ 𝐾 = ( Base ‘ 𝑅 )
cayhamlem2.a ⊢ 𝐴 = ( 𝑁 Mat 𝑅 )
cayhamlem2.b ⊢ 𝐵 = ( Base ‘ 𝐴 )
cayhamlem2.1 ⊢ 1 = ( 1r ‘ 𝐴 )
cayhamlem2.m ⊢ ∗ = ( ·𝑠 ‘ 𝐴 )
cayhamlem2.e ⊢ ↑ = ( .g ‘ ( mulGrp ‘ 𝐴 ) )
cayhamlem2.r ⊢ · = ( .r ‘ 𝐴 )
Assertion cayhamlem2 ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) ∧ ( 𝐻 ∈ ( 𝐾 ↑m ℕ0 ) ∧ 𝐿 ∈ ℕ0 ) ) → ( ( 𝐻 ‘ 𝐿 ) ∗ ( 𝐿 ↑ 𝑀 ) ) = ( ( 𝐿 ↑ 𝑀 ) · ( ( 𝐻 ‘ 𝐿 ) ∗ 1 ) ) )

Proof

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 ffvelcdmda ⊢ ( ( 𝐻 ∈ ( 𝐾 ↑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 eqtr2id ⊢ ( ( 𝑁 ∈ 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 eqid ⊢ ( mulGrp ‘ 𝐴 ) = ( mulGrp ‘ 𝐴 )
29 28 3 mgpbas ⊢ 𝐵 = ( Base ‘ ( mulGrp ‘ 𝐴 ) )
30 crngring ⊢ ( 𝑅 ∈ CRing → 𝑅 ∈ Ring )
31 30 anim2i ⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ) → ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) )
32 31 3adant3 ⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) → ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) )
33 2 matring ⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) → 𝐴 ∈ Ring )
34 28 ringmgp ⊢ ( 𝐴 ∈ Ring → ( mulGrp ‘ 𝐴 ) ∈ Mnd )
35 32 33 34 3syl ⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) → ( mulGrp ‘ 𝐴 ) ∈ Mnd )
36 35 adantr ⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) ∧ ( 𝐻 ∈ ( 𝐾 ↑m ℕ0 ) ∧ 𝐿 ∈ ℕ0 ) ) → ( mulGrp ‘ 𝐴 ) ∈ Mnd )
37 simprr ⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) ∧ ( 𝐻 ∈ ( 𝐾 ↑m ℕ0 ) ∧ 𝐿 ∈ ℕ0 ) ) → 𝐿 ∈ ℕ0 )
38 simpl3 ⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) ∧ ( 𝐻 ∈ ( 𝐾 ↑m ℕ0 ) ∧ 𝐿 ∈ ℕ0 ) ) → 𝑀 ∈ 𝐵 )
39 29 6 36 37 38 mulgnn0cld ⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) ∧ ( 𝐻 ∈ ( 𝐾 ↑m ℕ0 ) ∧ 𝐿 ∈ ℕ0 ) ) → ( 𝐿 ↑ 𝑀 ) ∈ 𝐵 )
40 18 19 20 3 7 5 asclmul2 ⊢ ( ( 𝐴 ∈ AssAlg ∧ ( 𝐻 ‘ 𝐿 ) ∈ ( Base ‘ ( Scalar ‘ 𝐴 ) ) ∧ ( 𝐿 ↑ 𝑀 ) ∈ 𝐵 ) → ( ( 𝐿 ↑ 𝑀 ) · ( ( algSc ‘ 𝐴 ) ‘ ( 𝐻 ‘ 𝐿 ) ) ) = ( ( 𝐻 ‘ 𝐿 ) ∗ ( 𝐿 ↑ 𝑀 ) ) )
41 27 17 39 40 syl3anc ⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) ∧ ( 𝐻 ∈ ( 𝐾 ↑m ℕ0 ) ∧ 𝐿 ∈ ℕ0 ) ) → ( ( 𝐿 ↑ 𝑀 ) · ( ( algSc ‘ 𝐴 ) ‘ ( 𝐻 ‘ 𝐿 ) ) ) = ( ( 𝐻 ‘ 𝐿 ) ∗ ( 𝐿 ↑ 𝑀 ) ) )
42 24 41 eqtr2d ⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) ∧ ( 𝐻 ∈ ( 𝐾 ↑m ℕ0 ) ∧ 𝐿 ∈ ℕ0 ) ) → ( ( 𝐻 ‘ 𝐿 ) ∗ ( 𝐿 ↑ 𝑀 ) ) = ( ( 𝐿 ↑ 𝑀 ) · ( ( 𝐻 ‘ 𝐿 ) ∗ 1 ) ) )