cayhamlem3

Description: Lemma for cayhamlem4 . (Contributed by AV, 24-Nov-2019) (Revised by AV, 15-Dec-2019)

	Ref	Expression
Hypotheses	chcoeffeq.a	$⊢ A = N Mat R$
	chcoeffeq.b	$⊢ B = {Base}_{A}$
	chcoeffeq.p	$⊢ P = {Poly}_{1} (R)$
	chcoeffeq.y	$⊢ Y = N Mat P$
	chcoeffeq.r	$⊢ \underset{˙}{\times} = \cdot_{Y}$
	chcoeffeq.s	$⊢ \underset{˙}{-} = -_{Y}$
	chcoeffeq.0	$⊢ \underset{˙}{0} = 0_{Y}$
	chcoeffeq.t	$⊢ T = N matToPolyMat R$
	chcoeffeq.c	$⊢ C = N CharPlyMat R$
	chcoeffeq.k	$⊢ K = C (M)$
	chcoeffeq.g	$⊢ G = (n \in ℕ_{0} ⟼ if (n = 0, \underset{˙}{0} \underset{˙}{-} (T (M) \underset{˙}{\times} T (b (0))), if (n = s + 1, T (b (s)), if (s + 1 < n, \underset{˙}{0}, T (b (n - 1)) \underset{˙}{-} (T (M) \underset{˙}{\times} T (b (n)))))))$
	chcoeffeq.w	$⊢ W = {Base}_{Y}$
	chcoeffeq.1	$⊢ \underset{˙}{1} = 1_{A}$
	chcoeffeq.m	$⊢ \underset{˙}{*} = \cdot_{A}$
	chcoeffeq.u	$⊢ U = N cPolyMatToMat R$
	cayhamlem.e1	$⊢ \underset{˙}{\times} = \cdot_{{mulGrp}_{A}}$
	cayhamlem.r	$⊢ \underset{˙}{\cdot} = \cdot_{A}$
Assertion	cayhamlem3	$⊢ (N \in Fin \land R \in CRing \land M \in B) \to \exists s \in ℕ \exists b \in (B^{(0 \dots s)}) \underset{n \in ℕ_{0}}{\sum_{A}} ({coe}_{1} (K) (n) \underset{˙}{*} (n \underset{˙}{\times} M)) = \underset{n \in ℕ_{0}}{\sum_{A}} ((n \underset{˙}{\times} M) \underset{˙}{\cdot} U (G (n)))$

Proof

Step	Hyp	Ref	Expression
1		chcoeffeq.a	$⊢ A = N Mat R$
2		chcoeffeq.b	$⊢ B = {Base}_{A}$
3		chcoeffeq.p	$⊢ P = {Poly}_{1} (R)$
4		chcoeffeq.y	$⊢ Y = N Mat P$
5		chcoeffeq.r	$⊢ \underset{˙}{\times} = \cdot_{Y}$
6		chcoeffeq.s	$⊢ \underset{˙}{-} = -_{Y}$
7		chcoeffeq.0	$⊢ \underset{˙}{0} = 0_{Y}$
8		chcoeffeq.t	$⊢ T = N matToPolyMat R$
9		chcoeffeq.c	$⊢ C = N CharPlyMat R$
10		chcoeffeq.k	$⊢ K = C (M)$
11		chcoeffeq.g	$⊢ G = (n \in ℕ_{0} ⟼ if (n = 0, \underset{˙}{0} \underset{˙}{-} (T (M) \underset{˙}{\times} T (b (0))), if (n = s + 1, T (b (s)), if (s + 1 < n, \underset{˙}{0}, T (b (n - 1)) \underset{˙}{-} (T (M) \underset{˙}{\times} T (b (n)))))))$
12		chcoeffeq.w	$⊢ W = {Base}_{Y}$
13		chcoeffeq.1	$⊢ \underset{˙}{1} = 1_{A}$
14		chcoeffeq.m	$⊢ \underset{˙}{*} = \cdot_{A}$
15		chcoeffeq.u	$⊢ U = N cPolyMatToMat R$
16		cayhamlem.e1	$⊢ \underset{˙}{\times} = \cdot_{{mulGrp}_{A}}$
17		cayhamlem.r	$⊢ \underset{˙}{\cdot} = \cdot_{A}$
18	1 2 3 4 5 6 7 8 9 10 11 12 13 14 15	chcoeffeq	$⊢ (N \in Fin \land R \in CRing \land M \in B) \to \exists s \in ℕ \exists b \in (B^{(0 \dots s)}) \forall n \in ℕ_{0} U (G (n)) = {coe}_{1} (K) (n) \underset{˙}{*} \underset{˙}{1}$
19		2fveq3	$⊢ n = l \to U (G (n)) = U (G (l))$
20		fveq2	$⊢ n = l \to {coe}_{1} (K) (n) = {coe}_{1} (K) (l)$
21	20	oveq1d	$⊢ n = l \to {coe}_{1} (K) (n) \underset{˙}{} \underset{˙}{1} = {coe}_{1} (K) (l) \underset{˙}{} \underset{˙}{1}$
22	19 21	eqeq12d	$⊢ n = l \to (U (G (n)) = {coe}_{1} (K) (n) \underset{˙}{} \underset{˙}{1} \leftrightarrow U (G (l)) = {coe}_{1} (K) (l) \underset{˙}{} \underset{˙}{1})$
23	22	cbvralvw	$⊢ \forall n \in ℕ_{0} U (G (n)) = {coe}_{1} (K) (n) \underset{˙}{} \underset{˙}{1} \leftrightarrow \forall l \in ℕ_{0} U (G (l)) = {coe}_{1} (K) (l) \underset{˙}{} \underset{˙}{1}$
24		2fveq3	$⊢ l = n \to U (G (l)) = U (G (n))$
25		fveq2	$⊢ l = n \to {coe}_{1} (K) (l) = {coe}_{1} (K) (n)$
26	25	oveq1d	$⊢ l = n \to {coe}_{1} (K) (l) \underset{˙}{} \underset{˙}{1} = {coe}_{1} (K) (n) \underset{˙}{} \underset{˙}{1}$
27	24 26	eqeq12d	$⊢ l = n \to (U (G (l)) = {coe}_{1} (K) (l) \underset{˙}{} \underset{˙}{1} \leftrightarrow U (G (n)) = {coe}_{1} (K) (n) \underset{˙}{} \underset{˙}{1})$
28	27	rspccva	$⊢ (\forall l \in ℕ_{0} U (G (l)) = {coe}_{1} (K) (l) \underset{˙}{} \underset{˙}{1} \land n \in ℕ_{0}) \to U (G (n)) = {coe}_{1} (K) (n) \underset{˙}{} \underset{˙}{1}$
29		simprll	$⊢ (n \in ℕ_{0} \land (((N \in Fin \land R \in CRing \land M \in B) \land s \in ℕ) \land b \in (B^{(0 \dots s)}))) \to (N \in Fin \land R \in CRing \land M \in B)$
30		eqid	$⊢ {Base}_{P} = {Base}_{P}$
31	9 1 2 3 30	chpmatply1	$⊢ (N \in Fin \land R \in CRing \land M \in B) \to C (M) \in {Base}_{P}$
32	29 31	syl	$⊢ (n \in ℕ_{0} \land (((N \in Fin \land R \in CRing \land M \in B) \land s \in ℕ) \land b \in (B^{(0 \dots s)}))) \to C (M) \in {Base}_{P}$
33	10 32	eqeltrid	$⊢ (n \in ℕ_{0} \land (((N \in Fin \land R \in CRing \land M \in B) \land s \in ℕ) \land b \in (B^{(0 \dots s)}))) \to K \in {Base}_{P}$
34		eqid	$⊢ {coe}_{1} (K) = {coe}_{1} (K)$
35		eqid	$⊢ {Base}_{R} = {Base}_{R}$
36	34 30 3 35	coe1f	$⊢ K \in {Base}_{P} \to {coe}_{1} (K) : ℕ_{0} ⟶ {Base}_{R}$
37	33 36	syl	$⊢ (n \in ℕ_{0} \land (((N \in Fin \land R \in CRing \land M \in B) \land s \in ℕ) \land b \in (B^{(0 \dots s)}))) \to {coe}_{1} (K) : ℕ_{0} ⟶ {Base}_{R}$
38		fvex	$⊢ {Base}_{R} \in V$
39		nn0ex	$⊢ ℕ_{0} \in V$
40	38 39	pm3.2i	$⊢ ({Base}_{R} \in V \land ℕ_{0} \in V)$
41		elmapg	$⊢ ({Base}_{R} \in V \land ℕ_{0} \in V) \to ({coe}_{1} (K) \in ({Base}_{R}^{ℕ_{0}}) \leftrightarrow {coe}_{1} (K) : ℕ_{0} ⟶ {Base}_{R})$
42	40 41	mp1i	$⊢ (n \in ℕ_{0} \land (((N \in Fin \land R \in CRing \land M \in B) \land s \in ℕ) \land b \in (B^{(0 \dots s)}))) \to ({coe}_{1} (K) \in ({Base}_{R}^{ℕ_{0}}) \leftrightarrow {coe}_{1} (K) : ℕ_{0} ⟶ {Base}_{R})$
43	37 42	mpbird	$⊢ (n \in ℕ_{0} \land (((N \in Fin \land R \in CRing \land M \in B) \land s \in ℕ) \land b \in (B^{(0 \dots s)}))) \to {coe}_{1} (K) \in ({Base}_{R}^{ℕ_{0}})$
44		simpl	$⊢ (n \in ℕ_{0} \land (((N \in Fin \land R \in CRing \land M \in B) \land s \in ℕ) \land b \in (B^{(0 \dots s)}))) \to n \in ℕ_{0}$
45	35 1 2 13 14 16 17	cayhamlem2	$⊢ ((N \in Fin \land R \in CRing \land M \in B) \land ({coe}_{1} (K) \in ({Base}_{R}^{ℕ_{0}}) \land n \in ℕ_{0})) \to {coe}_{1} (K) (n) \underset{˙}{} (n \underset{˙}{\times} M) = (n \underset{˙}{\times} M) \underset{˙}{\cdot} ({coe}_{1} (K) (n) \underset{˙}{} \underset{˙}{1})$
46	29 43 44 45	syl12anc	$⊢ (n \in ℕ_{0} \land (((N \in Fin \land R \in CRing \land M \in B) \land s \in ℕ) \land b \in (B^{(0 \dots s)}))) \to {coe}_{1} (K) (n) \underset{˙}{} (n \underset{˙}{\times} M) = (n \underset{˙}{\times} M) \underset{˙}{\cdot} ({coe}_{1} (K) (n) \underset{˙}{} \underset{˙}{1})$
47	46	adantl	$⊢ (U (G (n)) = {coe}_{1} (K) (n) \underset{˙}{} \underset{˙}{1} \land (n \in ℕ_{0} \land (((N \in Fin \land R \in CRing \land M \in B) \land s \in ℕ) \land b \in (B^{(0 \dots s)})))) \to {coe}_{1} (K) (n) \underset{˙}{} (n \underset{˙}{\times} M) = (n \underset{˙}{\times} M) \underset{˙}{\cdot} ({coe}_{1} (K) (n) \underset{˙}{*} \underset{˙}{1})$
48		oveq2	$⊢ U (G (n)) = {coe}_{1} (K) (n) \underset{˙}{} \underset{˙}{1} \to (n \underset{˙}{\times} M) \underset{˙}{\cdot} U (G (n)) = (n \underset{˙}{\times} M) \underset{˙}{\cdot} ({coe}_{1} (K) (n) \underset{˙}{} \underset{˙}{1})$
49	48	adantr	$⊢ (U (G (n)) = {coe}_{1} (K) (n) \underset{˙}{} \underset{˙}{1} \land (n \in ℕ_{0} \land (((N \in Fin \land R \in CRing \land M \in B) \land s \in ℕ) \land b \in (B^{(0 \dots s)})))) \to (n \underset{˙}{\times} M) \underset{˙}{\cdot} U (G (n)) = (n \underset{˙}{\times} M) \underset{˙}{\cdot} ({coe}_{1} (K) (n) \underset{˙}{} \underset{˙}{1})$
50	47 49	eqtr4d	$⊢ (U (G (n)) = {coe}_{1} (K) (n) \underset{˙}{} \underset{˙}{1} \land (n \in ℕ_{0} \land (((N \in Fin \land R \in CRing \land M \in B) \land s \in ℕ) \land b \in (B^{(0 \dots s)})))) \to {coe}_{1} (K) (n) \underset{˙}{} (n \underset{˙}{\times} M) = (n \underset{˙}{\times} M) \underset{˙}{\cdot} U (G (n))$
51	50	exp32	$⊢ U (G (n)) = {coe}_{1} (K) (n) \underset{˙}{} \underset{˙}{1} \to (n \in ℕ_{0} \to ((((N \in Fin \land R \in CRing \land M \in B) \land s \in ℕ) \land b \in (B^{(0 \dots s)})) \to {coe}_{1} (K) (n) \underset{˙}{} (n \underset{˙}{\times} M) = (n \underset{˙}{\times} M) \underset{˙}{\cdot} U (G (n))))$
52	51	com12	$⊢ n \in ℕ_{0} \to (U (G (n)) = {coe}_{1} (K) (n) \underset{˙}{} \underset{˙}{1} \to ((((N \in Fin \land R \in CRing \land M \in B) \land s \in ℕ) \land b \in (B^{(0 \dots s)})) \to {coe}_{1} (K) (n) \underset{˙}{} (n \underset{˙}{\times} M) = (n \underset{˙}{\times} M) \underset{˙}{\cdot} U (G (n))))$
53	52	adantl	$⊢ (\forall l \in ℕ_{0} U (G (l)) = {coe}_{1} (K) (l) \underset{˙}{} \underset{˙}{1} \land n \in ℕ_{0}) \to (U (G (n)) = {coe}_{1} (K) (n) \underset{˙}{} \underset{˙}{1} \to ((((N \in Fin \land R \in CRing \land M \in B) \land s \in ℕ) \land b \in (B^{(0 \dots s)})) \to {coe}_{1} (K) (n) \underset{˙}{*} (n \underset{˙}{\times} M) = (n \underset{˙}{\times} M) \underset{˙}{\cdot} U (G (n))))$
54	28 53	mpd	$⊢ (\forall l \in ℕ_{0} U (G (l)) = {coe}_{1} (K) (l) \underset{˙}{} \underset{˙}{1} \land n \in ℕ_{0}) \to ((((N \in Fin \land R \in CRing \land M \in B) \land s \in ℕ) \land b \in (B^{(0 \dots s)})) \to {coe}_{1} (K) (n) \underset{˙}{} (n \underset{˙}{\times} M) = (n \underset{˙}{\times} M) \underset{˙}{\cdot} U (G (n)))$
55	54	com12	$⊢ (((N \in Fin \land R \in CRing \land M \in B) \land s \in ℕ) \land b \in (B^{(0 \dots s)})) \to ((\forall l \in ℕ_{0} U (G (l)) = {coe}_{1} (K) (l) \underset{˙}{} \underset{˙}{1} \land n \in ℕ_{0}) \to {coe}_{1} (K) (n) \underset{˙}{} (n \underset{˙}{\times} M) = (n \underset{˙}{\times} M) \underset{˙}{\cdot} U (G (n)))$
56	55	impl	$⊢ (((((N \in Fin \land R \in CRing \land M \in B) \land s \in ℕ) \land b \in (B^{(0 \dots s)})) \land \forall l \in ℕ_{0} U (G (l)) = {coe}_{1} (K) (l) \underset{˙}{} \underset{˙}{1}) \land n \in ℕ_{0}) \to {coe}_{1} (K) (n) \underset{˙}{} (n \underset{˙}{\times} M) = (n \underset{˙}{\times} M) \underset{˙}{\cdot} U (G (n))$
57	56	mpteq2dva	$⊢ ((((N \in Fin \land R \in CRing \land M \in B) \land s \in ℕ) \land b \in (B^{(0 \dots s)})) \land \forall l \in ℕ_{0} U (G (l)) = {coe}_{1} (K) (l) \underset{˙}{} \underset{˙}{1}) \to (n \in ℕ_{0} ⟼ {coe}_{1} (K) (n) \underset{˙}{} (n \underset{˙}{\times} M)) = (n \in ℕ_{0} ⟼ (n \underset{˙}{\times} M) \underset{˙}{\cdot} U (G (n)))$
58	57	oveq2d	$⊢ ((((N \in Fin \land R \in CRing \land M \in B) \land s \in ℕ) \land b \in (B^{(0 \dots s)})) \land \forall l \in ℕ_{0} U (G (l)) = {coe}_{1} (K) (l) \underset{˙}{} \underset{˙}{1}) \to \underset{n \in ℕ_{0}}{\sum_{A}} ({coe}_{1} (K) (n) \underset{˙}{} (n \underset{˙}{\times} M)) = \underset{n \in ℕ_{0}}{\sum_{A}} ((n \underset{˙}{\times} M) \underset{˙}{\cdot} U (G (n)))$
59	58	ex	$⊢ (((N \in Fin \land R \in CRing \land M \in B) \land s \in ℕ) \land b \in (B^{(0 \dots s)})) \to (\forall l \in ℕ_{0} U (G (l)) = {coe}_{1} (K) (l) \underset{˙}{} \underset{˙}{1} \to \underset{n \in ℕ_{0}}{\sum_{A}} ({coe}_{1} (K) (n) \underset{˙}{} (n \underset{˙}{\times} M)) = \underset{n \in ℕ_{0}}{\sum_{A}} ((n \underset{˙}{\times} M) \underset{˙}{\cdot} U (G (n))))$
60	23 59	syl5bi	$⊢ (((N \in Fin \land R \in CRing \land M \in B) \land s \in ℕ) \land b \in (B^{(0 \dots s)})) \to (\forall n \in ℕ_{0} U (G (n)) = {coe}_{1} (K) (n) \underset{˙}{} \underset{˙}{1} \to \underset{n \in ℕ_{0}}{\sum_{A}} ({coe}_{1} (K) (n) \underset{˙}{} (n \underset{˙}{\times} M)) = \underset{n \in ℕ_{0}}{\sum_{A}} ((n \underset{˙}{\times} M) \underset{˙}{\cdot} U (G (n))))$
61	60	reximdva	$⊢ ((N \in Fin \land R \in CRing \land M \in B) \land s \in ℕ) \to (\exists b \in (B^{(0 \dots s)}) \forall n \in ℕ_{0} U (G (n)) = {coe}_{1} (K) (n) \underset{˙}{} \underset{˙}{1} \to \exists b \in (B^{(0 \dots s)}) \underset{n \in ℕ_{0}}{\sum_{A}} ({coe}_{1} (K) (n) \underset{˙}{} (n \underset{˙}{\times} M)) = \underset{n \in ℕ_{0}}{\sum_{A}} ((n \underset{˙}{\times} M) \underset{˙}{\cdot} U (G (n))))$
62	61	reximdva	$⊢ (N \in Fin \land R \in CRing \land M \in B) \to (\exists s \in ℕ \exists b \in (B^{(0 \dots s)}) \forall n \in ℕ_{0} U (G (n)) = {coe}_{1} (K) (n) \underset{˙}{} \underset{˙}{1} \to \exists s \in ℕ \exists b \in (B^{(0 \dots s)}) \underset{n \in ℕ_{0}}{\sum_{A}} ({coe}_{1} (K) (n) \underset{˙}{} (n \underset{˙}{\times} M)) = \underset{n \in ℕ_{0}}{\sum_{A}} ((n \underset{˙}{\times} M) \underset{˙}{\cdot} U (G (n))))$
63	18 62	mpd	$⊢ (N \in Fin \land R \in CRing \land M \in B) \to \exists s \in ℕ \exists b \in (B^{(0 \dots s)}) \underset{n \in ℕ_{0}}{\sum_{A}} ({coe}_{1} (K) (n) \underset{˙}{*} (n \underset{˙}{\times} M)) = \underset{n \in ℕ_{0}}{\sum_{A}} ((n \underset{˙}{\times} M) \underset{˙}{\cdot} U (G (n)))$

Metamath Proof Explorer

Theorem cayhamlem3

Proof