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 ∧ 𝑀𝐵 ) ∧ ( 𝐻 ∈ ( 𝐾m0 ) ∧ 𝐿 ∈ ℕ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 ( 𝐻 ∈ ( 𝐾m0 ) → 𝐻 : ℕ0𝐾 )
9 8 ffvelrnda ( ( 𝐻 ∈ ( 𝐾m0 ) ∧ 𝐿 ∈ ℕ0 ) → ( 𝐻𝐿 ) ∈ 𝐾 )
10 9 adantl ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀𝐵 ) ∧ ( 𝐻 ∈ ( 𝐾m0 ) ∧ 𝐿 ∈ ℕ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 ∧ 𝑀𝐵 ) ∧ ( 𝐻 ∈ ( 𝐾m0 ) ∧ 𝐿 ∈ ℕ0 ) ) → ( ( 𝐻𝐿 ) ∈ ( Base ‘ ( Scalar ‘ 𝐴 ) ) ↔ ( 𝐻𝐿 ) ∈ 𝐾 ) )
17 10 16 mpbird ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀𝐵 ) ∧ ( 𝐻 ∈ ( 𝐾m0 ) ∧ 𝐿 ∈ ℕ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 ∧ 𝑀𝐵 ) ∧ ( 𝐻 ∈ ( 𝐾m0 ) ∧ 𝐿 ∈ ℕ0 ) ) → ( ( algSc ‘ 𝐴 ) ‘ ( 𝐻𝐿 ) ) = ( ( 𝐻𝐿 ) 1 ) )
23 22 eqcomd ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀𝐵 ) ∧ ( 𝐻 ∈ ( 𝐾m0 ) ∧ 𝐿 ∈ ℕ0 ) ) → ( ( 𝐻𝐿 ) 1 ) = ( ( algSc ‘ 𝐴 ) ‘ ( 𝐻𝐿 ) ) )
24 23 oveq2d ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀𝐵 ) ∧ ( 𝐻 ∈ ( 𝐾m0 ) ∧ 𝐿 ∈ ℕ0 ) ) → ( ( 𝐿 𝑀 ) · ( ( 𝐻𝐿 ) 1 ) ) = ( ( 𝐿 𝑀 ) · ( ( algSc ‘ 𝐴 ) ‘ ( 𝐻𝐿 ) ) ) )
25 2 matassa ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ) → 𝐴 ∈ AssAlg )
26 25 3adant3 ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀𝐵 ) → 𝐴 ∈ AssAlg )
27 26 adantr ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀𝐵 ) ∧ ( 𝐻 ∈ ( 𝐾m0 ) ∧ 𝐿 ∈ ℕ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 ∧ 𝑀𝐵 ) ∧ ( 𝐻 ∈ ( 𝐾m0 ) ∧ 𝐿 ∈ ℕ0 ) ) → ( mulGrp ‘ 𝐴 ) ∈ Mnd )
36 simprr ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀𝐵 ) ∧ ( 𝐻 ∈ ( 𝐾m0 ) ∧ 𝐿 ∈ ℕ0 ) ) → 𝐿 ∈ ℕ0 )
37 simpl3 ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀𝐵 ) ∧ ( 𝐻 ∈ ( 𝐾m0 ) ∧ 𝐿 ∈ ℕ0 ) ) → 𝑀𝐵 )
38 32 3 mgpbas 𝐵 = ( Base ‘ ( mulGrp ‘ 𝐴 ) )
39 38 6 mulgnn0cl ( ( ( mulGrp ‘ 𝐴 ) ∈ Mnd ∧ 𝐿 ∈ ℕ0𝑀𝐵 ) → ( 𝐿 𝑀 ) ∈ 𝐵 )
40 35 36 37 39 syl3anc ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀𝐵 ) ∧ ( 𝐻 ∈ ( 𝐾m0 ) ∧ 𝐿 ∈ ℕ0 ) ) → ( 𝐿 𝑀 ) ∈ 𝐵 )
41 18 19 20 3 7 5 asclmul2 ( ( 𝐴 ∈ AssAlg ∧ ( 𝐻𝐿 ) ∈ ( Base ‘ ( Scalar ‘ 𝐴 ) ) ∧ ( 𝐿 𝑀 ) ∈ 𝐵 ) → ( ( 𝐿 𝑀 ) · ( ( algSc ‘ 𝐴 ) ‘ ( 𝐻𝐿 ) ) ) = ( ( 𝐻𝐿 ) ( 𝐿 𝑀 ) ) )
42 27 17 40 41 syl3anc ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀𝐵 ) ∧ ( 𝐻 ∈ ( 𝐾m0 ) ∧ 𝐿 ∈ ℕ0 ) ) → ( ( 𝐿 𝑀 ) · ( ( algSc ‘ 𝐴 ) ‘ ( 𝐻𝐿 ) ) ) = ( ( 𝐻𝐿 ) ( 𝐿 𝑀 ) ) )
43 24 42 eqtr2d ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀𝐵 ) ∧ ( 𝐻 ∈ ( 𝐾m0 ) ∧ 𝐿 ∈ ℕ0 ) ) → ( ( 𝐻𝐿 ) ( 𝐿 𝑀 ) ) = ( ( 𝐿 𝑀 ) · ( ( 𝐻𝐿 ) 1 ) ) )