Metamath Proof Explorer

Theorem cayhamlem2

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

Ref Expression
Hypotheses cayhamlem2.k ⊢ K = Base R
cayhamlem2.a ⊢ A = N Mat R
cayhamlem2.b ⊢ B = Base A
cayhamlem2.1 ⊢ 1 ˙ = 1 A
cayhamlem2.m ⊢ ∗ ˙ = ⋅ A
cayhamlem2.e ⊢ × ˙ = ⋅ mulGrp A
cayhamlem2.r ⊢ · ˙ = ⋅ A
Assertion cayhamlem2 ⊢ N ∈ Fin ∧ R ∈ CRing ∧ M ∈ B ∧ H ∈ K ℕ 0 ∧ L ∈ ℕ 0 → H ⁡ L ∗ ˙ L × ˙ M = L × ˙ M · ˙ H ⁡ L ∗ ˙ 1 ˙

Proof

Step Hyp Ref Expression
1 cayhamlem2.k ⊢ K = Base R
2 cayhamlem2.a ⊢ A = N Mat R
3 cayhamlem2.b ⊢ B = Base A
4 cayhamlem2.1 ⊢ 1 ˙ = 1 A
5 cayhamlem2.m ⊢ ∗ ˙ = ⋅ A
6 cayhamlem2.e ⊢ × ˙ = ⋅ mulGrp A
7 cayhamlem2.r ⊢ · ˙ = ⋅ A
8 elmapi ⊢ H ∈ K ℕ 0 → H : ℕ 0 ⟶ K
9 8 ffvelcdmda ⊢ H ∈ K ℕ 0 ∧ L ∈ ℕ 0 → H ⁡ L ∈ K
10 9 adantl ⊢ N ∈ Fin ∧ R ∈ CRing ∧ M ∈ B ∧ H ∈ K ℕ 0 ∧ L ∈ ℕ 0 → H ⁡ L ∈ K
11 2 matsca2 ⊢ N ∈ Fin ∧ R ∈ CRing → R = Scalar ⁡ A
12 11 3adant3 ⊢ N ∈ Fin ∧ R ∈ CRing ∧ M ∈ B → R = Scalar ⁡ A
13 12 fveq2d ⊢ N ∈ Fin ∧ R ∈ CRing ∧ M ∈ B → Base R = Base Scalar ⁡ A
14 1 13 eqtr2id ⊢ N ∈ Fin ∧ R ∈ CRing ∧ M ∈ B → Base Scalar ⁡ A = K
15 14 eleq2d ⊢ N ∈ Fin ∧ R ∈ CRing ∧ M ∈ B → H ⁡ L ∈ Base Scalar ⁡ A ↔ H ⁡ L ∈ K
16 15 adantr ⊢ N ∈ Fin ∧ R ∈ CRing ∧ M ∈ B ∧ H ∈ K ℕ 0 ∧ L ∈ ℕ 0 → H ⁡ L ∈ Base Scalar ⁡ A ↔ H ⁡ L ∈ K
17 10 16 mpbird ⊢ N ∈ Fin ∧ R ∈ CRing ∧ M ∈ B ∧ H ∈ K ℕ 0 ∧ L ∈ ℕ 0 → H ⁡ L ∈ Base Scalar ⁡ A
18 eqid ⊢ algSc ⁡ A = algSc ⁡ A
19 eqid ⊢ Scalar ⁡ A = Scalar ⁡ A
20 eqid ⊢ Base Scalar ⁡ A = Base Scalar ⁡ A
21 18 19 20 5 4 asclval ⊢ H ⁡ L ∈ Base Scalar ⁡ A → algSc ⁡ A ⁡ H ⁡ L = H ⁡ L ∗ ˙ 1 ˙
22 17 21 syl ⊢ N ∈ Fin ∧ R ∈ CRing ∧ M ∈ B ∧ H ∈ K ℕ 0 ∧ L ∈ ℕ 0 → algSc ⁡ A ⁡ H ⁡ L = H ⁡ L ∗ ˙ 1 ˙
23 22 eqcomd ⊢ N ∈ Fin ∧ R ∈ CRing ∧ M ∈ B ∧ H ∈ K ℕ 0 ∧ L ∈ ℕ 0 → H ⁡ L ∗ ˙ 1 ˙ = algSc ⁡ A ⁡ H ⁡ L
24 23 oveq2d ⊢ N ∈ Fin ∧ R ∈ CRing ∧ M ∈ B ∧ H ∈ K ℕ 0 ∧ L ∈ ℕ 0 → L × ˙ M · ˙ H ⁡ L ∗ ˙ 1 ˙ = L × ˙ M · ˙ algSc ⁡ A ⁡ H ⁡ L
25 2 matassa ⊢ N ∈ Fin ∧ R ∈ CRing → A ∈ AssAlg
26 25 3adant3 ⊢ N ∈ Fin ∧ R ∈ CRing ∧ M ∈ B → A ∈ AssAlg
27 26 adantr ⊢ N ∈ Fin ∧ R ∈ CRing ∧ M ∈ B ∧ H ∈ K ℕ 0 ∧ L ∈ ℕ 0 → A ∈ AssAlg
28 eqid ⊢ mulGrp A = mulGrp A
29 28 3 mgpbas ⊢ B = Base mulGrp A
30 crngring ⊢ R ∈ CRing → R ∈ Ring
31 30 anim2i ⊢ N ∈ Fin ∧ R ∈ CRing → N ∈ Fin ∧ R ∈ Ring
32 31 3adant3 ⊢ N ∈ Fin ∧ R ∈ CRing ∧ M ∈ B → N ∈ Fin ∧ R ∈ Ring
33 2 matring ⊢ N ∈ Fin ∧ R ∈ Ring → A ∈ Ring
34 28 ringmgp ⊢ A ∈ Ring → mulGrp A ∈ Mnd
35 32 33 34 3syl ⊢ N ∈ Fin ∧ R ∈ CRing ∧ M ∈ B → mulGrp A ∈ Mnd
36 35 adantr ⊢ N ∈ Fin ∧ R ∈ CRing ∧ M ∈ B ∧ H ∈ K ℕ 0 ∧ L ∈ ℕ 0 → mulGrp A ∈ Mnd
37 simprr ⊢ N ∈ Fin ∧ R ∈ CRing ∧ M ∈ B ∧ H ∈ K ℕ 0 ∧ L ∈ ℕ 0 → L ∈ ℕ 0
38 simpl3 ⊢ N ∈ Fin ∧ R ∈ CRing ∧ M ∈ B ∧ H ∈ K ℕ 0 ∧ L ∈ ℕ 0 → M ∈ B
39 29 6 36 37 38 mulgnn0cld ⊢ N ∈ Fin ∧ R ∈ CRing ∧ M ∈ B ∧ H ∈ K ℕ 0 ∧ L ∈ ℕ 0 → L × ˙ M ∈ B
40 18 19 20 3 7 5 asclmul2 ⊢ A ∈ AssAlg ∧ H ⁡ L ∈ Base Scalar ⁡ A ∧ L × ˙ M ∈ B → L × ˙ M · ˙ algSc ⁡ A ⁡ H ⁡ L = H ⁡ L ∗ ˙ L × ˙ M
41 27 17 39 40 syl3anc ⊢ N ∈ Fin ∧ R ∈ CRing ∧ M ∈ B ∧ H ∈ K ℕ 0 ∧ L ∈ ℕ 0 → L × ˙ M · ˙ algSc ⁡ A ⁡ H ⁡ L = H ⁡ L ∗ ˙ L × ˙ M
42 24 41 eqtr2d ⊢ N ∈ Fin ∧ R ∈ CRing ∧ M ∈ B ∧ H ∈ K ℕ 0 ∧ L ∈ ℕ 0 → H ⁡ L ∗ ˙ L × ˙ M = L × ˙ M · ˙ H ⁡ L ∗ ˙ 1 ˙