cayhamlem2

	Ref	Expression
Hypotheses	cayhamlem2.k	$⊢ K = {Base}_{R}$
	cayhamlem2.a	$⊢ A = N Mat R$
	cayhamlem2.b	$⊢ B = {Base}_{A}$
	cayhamlem2.1	$⊢ \underset{˙}{1} = 1_{A}$
	cayhamlem2.m	$⊢ \underset{˙}{*} = \cdot_{A}$
	cayhamlem2.e	$⊢ \underset{˙}{\times} = \cdot_{{mulGrp}_{A}}$
	cayhamlem2.r	$⊢ \underset{˙}{\cdot} = \cdot_{A}$
Assertion	cayhamlem2	$⊢ ((N \in Fin \land R \in CRing \land M \in B) \land (H \in (K^{ℕ_{0}}) \land L \in ℕ_{0})) \to H (L) \underset{˙}{} (L \underset{˙}{\times} M) = (L \underset{˙}{\times} M) \underset{˙}{\cdot} (H (L) \underset{˙}{} \underset{˙}{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	$⊢ \underset{˙}{1} = 1_{A}$
5		cayhamlem2.m	$⊢ \underset{˙}{*} = \cdot_{A}$
6		cayhamlem2.e	$⊢ \underset{˙}{\times} = \cdot_{{mulGrp}_{A}}$
7		cayhamlem2.r	$⊢ \underset{˙}{\cdot} = \cdot_{A}$
8		elmapi	$⊢ H \in (K^{ℕ_{0}}) \to H : ℕ_{0} ⟶ K$
9	8	ffvelrnda	$⊢ (H \in (K^{ℕ_{0}}) \land L \in ℕ_{0}) \to H (L) \in K$
10	9	adantl	$⊢ ((N \in Fin \land R \in CRing \land M \in B) \land (H \in (K^{ℕ_{0}}) \land L \in ℕ_{0})) \to H (L) \in K$
11	2	matsca2	$⊢ (N \in Fin \land R \in CRing) \to R = Scalar (A)$
12	11	3adant3	$⊢ (N \in Fin \land R \in CRing \land M \in B) \to R = Scalar (A)$
13	12	fveq2d	$⊢ (N \in Fin \land R \in CRing \land M \in B) \to {Base}_{R} = {Base}_{Scalar (A)}$
14	1 13	eqtr2id	$⊢ (N \in Fin \land R \in CRing \land M \in B) \to {Base}_{Scalar (A)} = K$
15	14	eleq2d	$⊢ (N \in Fin \land R \in CRing \land M \in B) \to (H (L) \in {Base}_{Scalar (A)} \leftrightarrow H (L) \in K)$
16	15	adantr	$⊢ ((N \in Fin \land R \in CRing \land M \in B) \land (H \in (K^{ℕ_{0}}) \land L \in ℕ_{0})) \to (H (L) \in {Base}_{Scalar (A)} \leftrightarrow H (L) \in K)$
17	10 16	mpbird	$⊢ ((N \in Fin \land R \in CRing \land M \in B) \land (H \in (K^{ℕ_{0}}) \land L \in ℕ_{0})) \to H (L) \in {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) \in {Base}_{Scalar (A)} \to algSc (A) (H (L)) = H (L) \underset{˙}{*} \underset{˙}{1}$
22	17 21	syl	$⊢ ((N \in Fin \land R \in CRing \land M \in B) \land (H \in (K^{ℕ_{0}}) \land L \in ℕ_{0})) \to algSc (A) (H (L)) = H (L) \underset{˙}{*} \underset{˙}{1}$
23	22	eqcomd	$⊢ ((N \in Fin \land R \in CRing \land M \in B) \land (H \in (K^{ℕ_{0}}) \land L \in ℕ_{0})) \to H (L) \underset{˙}{*} \underset{˙}{1} = algSc (A) (H (L))$
24	23	oveq2d	$⊢ ((N \in Fin \land R \in CRing \land M \in B) \land (H \in (K^{ℕ_{0}}) \land L \in ℕ_{0})) \to (L \underset{˙}{\times} M) \underset{˙}{\cdot} (H (L) \underset{˙}{*} \underset{˙}{1}) = (L \underset{˙}{\times} M) \underset{˙}{\cdot} algSc (A) (H (L))$
25	2	matassa	$⊢ (N \in Fin \land R \in CRing) \to A \in AssAlg$
26	25	3adant3	$⊢ (N \in Fin \land R \in CRing \land M \in B) \to A \in AssAlg$
27	26	adantr	$⊢ ((N \in Fin \land R \in CRing \land M \in B) \land (H \in (K^{ℕ_{0}}) \land L \in ℕ_{0})) \to A \in AssAlg$
28		crngring	$⊢ R \in CRing \to R \in Ring$
29	28	anim2i	$⊢ (N \in Fin \land R \in CRing) \to (N \in Fin \land R \in Ring)$
30	29	3adant3	$⊢ (N \in Fin \land R \in CRing \land M \in B) \to (N \in Fin \land R \in Ring)$
31	2	matring	$⊢ (N \in Fin \land R \in Ring) \to A \in Ring$
32		eqid	$⊢ {mulGrp}_{A} = {mulGrp}_{A}$
33	32	ringmgp	$⊢ A \in Ring \to {mulGrp}_{A} \in Mnd$
34	30 31 33	3syl	$⊢ (N \in Fin \land R \in CRing \land M \in B) \to {mulGrp}_{A} \in Mnd$
35	34	adantr	$⊢ ((N \in Fin \land R \in CRing \land M \in B) \land (H \in (K^{ℕ_{0}}) \land L \in ℕ_{0})) \to {mulGrp}_{A} \in Mnd$
36		simprr	$⊢ ((N \in Fin \land R \in CRing \land M \in B) \land (H \in (K^{ℕ_{0}}) \land L \in ℕ_{0})) \to L \in ℕ_{0}$
37		simpl3	$⊢ ((N \in Fin \land R \in CRing \land M \in B) \land (H \in (K^{ℕ_{0}}) \land L \in ℕ_{0})) \to M \in B$
38	32 3	mgpbas	$⊢ B = {Base}_{{mulGrp}_{A}}$
39	38 6	mulgnn0cl	$⊢ ({mulGrp}_{A} \in Mnd \land L \in ℕ_{0} \land M \in B) \to L \underset{˙}{\times} M \in B$
40	35 36 37 39	syl3anc	$⊢ ((N \in Fin \land R \in CRing \land M \in B) \land (H \in (K^{ℕ_{0}}) \land L \in ℕ_{0})) \to L \underset{˙}{\times} M \in B$
41	18 19 20 3 7 5	asclmul2	$⊢ (A \in AssAlg \land H (L) \in {Base}_{Scalar (A)} \land L \underset{˙}{\times} M \in B) \to (L \underset{˙}{\times} M) \underset{˙}{\cdot} algSc (A) (H (L)) = H (L) \underset{˙}{*} (L \underset{˙}{\times} M)$
42	27 17 40 41	syl3anc	$⊢ ((N \in Fin \land R \in CRing \land M \in B) \land (H \in (K^{ℕ_{0}}) \land L \in ℕ_{0})) \to (L \underset{˙}{\times} M) \underset{˙}{\cdot} algSc (A) (H (L)) = H (L) \underset{˙}{*} (L \underset{˙}{\times} M)$
43	24 42	eqtr2d	$⊢ ((N \in Fin \land R \in CRing \land M \in B) \land (H \in (K^{ℕ_{0}}) \land L \in ℕ_{0})) \to H (L) \underset{˙}{} (L \underset{˙}{\times} M) = (L \underset{˙}{\times} M) \underset{˙}{\cdot} (H (L) \underset{˙}{} \underset{˙}{1})$

Metamath Proof Explorer

Theorem cayhamlem2

Proof