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