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 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 ) ) )