# Metamath Proof Explorer

## Theorem cayhamlem3

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

Ref Expression
Hypotheses chcoeffeq.a ${⊢}{A}={N}\mathrm{Mat}{R}$
chcoeffeq.b ${⊢}{B}={\mathrm{Base}}_{{A}}$
chcoeffeq.p ${⊢}{P}={\mathrm{Poly}}_{1}\left({R}\right)$
chcoeffeq.y ${⊢}{Y}={N}\mathrm{Mat}{P}$
chcoeffeq.r
chcoeffeq.s
chcoeffeq.0
chcoeffeq.t ${⊢}{T}={N}\mathrm{matToPolyMat}{R}$
chcoeffeq.c ${⊢}{C}={N}\mathrm{CharPlyMat}{R}$
chcoeffeq.k ${⊢}{K}={C}\left({M}\right)$
chcoeffeq.g
chcoeffeq.w ${⊢}{W}={\mathrm{Base}}_{{Y}}$
chcoeffeq.1
chcoeffeq.m
chcoeffeq.u ${⊢}{U}={N}\mathrm{cPolyMatToMat}{R}$
cayhamlem.e1
cayhamlem.r
Assertion cayhamlem3

### Proof

Step Hyp Ref Expression
1 chcoeffeq.a ${⊢}{A}={N}\mathrm{Mat}{R}$
2 chcoeffeq.b ${⊢}{B}={\mathrm{Base}}_{{A}}$
3 chcoeffeq.p ${⊢}{P}={\mathrm{Poly}}_{1}\left({R}\right)$
4 chcoeffeq.y ${⊢}{Y}={N}\mathrm{Mat}{P}$
5 chcoeffeq.r
6 chcoeffeq.s
7 chcoeffeq.0
8 chcoeffeq.t ${⊢}{T}={N}\mathrm{matToPolyMat}{R}$
9 chcoeffeq.c ${⊢}{C}={N}\mathrm{CharPlyMat}{R}$
10 chcoeffeq.k ${⊢}{K}={C}\left({M}\right)$
11 chcoeffeq.g
12 chcoeffeq.w ${⊢}{W}={\mathrm{Base}}_{{Y}}$
13 chcoeffeq.1
14 chcoeffeq.m
15 chcoeffeq.u ${⊢}{U}={N}\mathrm{cPolyMatToMat}{R}$
16 cayhamlem.e1
17 cayhamlem.r
18 1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 chcoeffeq
19 2fveq3 ${⊢}{n}={l}\to {U}\left({G}\left({n}\right)\right)={U}\left({G}\left({l}\right)\right)$
20 fveq2 ${⊢}{n}={l}\to {\mathrm{coe}}_{1}\left({K}\right)\left({n}\right)={\mathrm{coe}}_{1}\left({K}\right)\left({l}\right)$
21 20 oveq1d
22 19 21 eqeq12d
23 22 cbvralvw
24 2fveq3 ${⊢}{l}={n}\to {U}\left({G}\left({l}\right)\right)={U}\left({G}\left({n}\right)\right)$
25 fveq2 ${⊢}{l}={n}\to {\mathrm{coe}}_{1}\left({K}\right)\left({l}\right)={\mathrm{coe}}_{1}\left({K}\right)\left({n}\right)$
26 25 oveq1d
27 24 26 eqeq12d
28 27 rspccva
29 simprll ${⊢}\left({n}\in {ℕ}_{0}\wedge \left(\left(\left({N}\in \mathrm{Fin}\wedge {R}\in \mathrm{CRing}\wedge {M}\in {B}\right)\wedge {s}\in ℕ\right)\wedge {b}\in \left({{B}}^{\left(0\dots {s}\right)}\right)\right)\right)\to \left({N}\in \mathrm{Fin}\wedge {R}\in \mathrm{CRing}\wedge {M}\in {B}\right)$
30 eqid ${⊢}{\mathrm{Base}}_{{P}}={\mathrm{Base}}_{{P}}$
31 9 1 2 3 30 chpmatply1 ${⊢}\left({N}\in \mathrm{Fin}\wedge {R}\in \mathrm{CRing}\wedge {M}\in {B}\right)\to {C}\left({M}\right)\in {\mathrm{Base}}_{{P}}$
32 29 31 syl ${⊢}\left({n}\in {ℕ}_{0}\wedge \left(\left(\left({N}\in \mathrm{Fin}\wedge {R}\in \mathrm{CRing}\wedge {M}\in {B}\right)\wedge {s}\in ℕ\right)\wedge {b}\in \left({{B}}^{\left(0\dots {s}\right)}\right)\right)\right)\to {C}\left({M}\right)\in {\mathrm{Base}}_{{P}}$
33 10 32 eqeltrid ${⊢}\left({n}\in {ℕ}_{0}\wedge \left(\left(\left({N}\in \mathrm{Fin}\wedge {R}\in \mathrm{CRing}\wedge {M}\in {B}\right)\wedge {s}\in ℕ\right)\wedge {b}\in \left({{B}}^{\left(0\dots {s}\right)}\right)\right)\right)\to {K}\in {\mathrm{Base}}_{{P}}$
34 eqid ${⊢}{\mathrm{coe}}_{1}\left({K}\right)={\mathrm{coe}}_{1}\left({K}\right)$
35 eqid ${⊢}{\mathrm{Base}}_{{R}}={\mathrm{Base}}_{{R}}$
36 34 30 3 35 coe1f ${⊢}{K}\in {\mathrm{Base}}_{{P}}\to {\mathrm{coe}}_{1}\left({K}\right):{ℕ}_{0}⟶{\mathrm{Base}}_{{R}}$
37 33 36 syl ${⊢}\left({n}\in {ℕ}_{0}\wedge \left(\left(\left({N}\in \mathrm{Fin}\wedge {R}\in \mathrm{CRing}\wedge {M}\in {B}\right)\wedge {s}\in ℕ\right)\wedge {b}\in \left({{B}}^{\left(0\dots {s}\right)}\right)\right)\right)\to {\mathrm{coe}}_{1}\left({K}\right):{ℕ}_{0}⟶{\mathrm{Base}}_{{R}}$
38 fvex ${⊢}{\mathrm{Base}}_{{R}}\in \mathrm{V}$
39 nn0ex ${⊢}{ℕ}_{0}\in \mathrm{V}$
40 38 39 pm3.2i ${⊢}\left({\mathrm{Base}}_{{R}}\in \mathrm{V}\wedge {ℕ}_{0}\in \mathrm{V}\right)$
41 elmapg ${⊢}\left({\mathrm{Base}}_{{R}}\in \mathrm{V}\wedge {ℕ}_{0}\in \mathrm{V}\right)\to \left({\mathrm{coe}}_{1}\left({K}\right)\in \left({{\mathrm{Base}}_{{R}}}^{{ℕ}_{0}}\right)↔{\mathrm{coe}}_{1}\left({K}\right):{ℕ}_{0}⟶{\mathrm{Base}}_{{R}}\right)$
42 40 41 mp1i ${⊢}\left({n}\in {ℕ}_{0}\wedge \left(\left(\left({N}\in \mathrm{Fin}\wedge {R}\in \mathrm{CRing}\wedge {M}\in {B}\right)\wedge {s}\in ℕ\right)\wedge {b}\in \left({{B}}^{\left(0\dots {s}\right)}\right)\right)\right)\to \left({\mathrm{coe}}_{1}\left({K}\right)\in \left({{\mathrm{Base}}_{{R}}}^{{ℕ}_{0}}\right)↔{\mathrm{coe}}_{1}\left({K}\right):{ℕ}_{0}⟶{\mathrm{Base}}_{{R}}\right)$
43 37 42 mpbird ${⊢}\left({n}\in {ℕ}_{0}\wedge \left(\left(\left({N}\in \mathrm{Fin}\wedge {R}\in \mathrm{CRing}\wedge {M}\in {B}\right)\wedge {s}\in ℕ\right)\wedge {b}\in \left({{B}}^{\left(0\dots {s}\right)}\right)\right)\right)\to {\mathrm{coe}}_{1}\left({K}\right)\in \left({{\mathrm{Base}}_{{R}}}^{{ℕ}_{0}}\right)$
44 simpl ${⊢}\left({n}\in {ℕ}_{0}\wedge \left(\left(\left({N}\in \mathrm{Fin}\wedge {R}\in \mathrm{CRing}\wedge {M}\in {B}\right)\wedge {s}\in ℕ\right)\wedge {b}\in \left({{B}}^{\left(0\dots {s}\right)}\right)\right)\right)\to {n}\in {ℕ}_{0}$
45 35 1 2 13 14 16 17 cayhamlem2
46 29 43 44 45 syl12anc
48 oveq2
50 47 49 eqtr4d
51 50 exp32
52 51 com12