Metamath Proof Explorer

Theorem pwsdiagmhm

Description: Diagonal monoid homomorphism into a structure power. (Contributed by Stefan O'Rear, 12-Mar-2015)

Ref Expression
Hypotheses pwsdiagmhm.y ${⊢}{Y}={R}{↑}_{𝑠}{I}$
pwsdiagmhm.b ${⊢}{B}={\mathrm{Base}}_{{R}}$
pwsdiagmhm.f ${⊢}{F}=\left({x}\in {B}⟼{I}×\left\{{x}\right\}\right)$
Assertion pwsdiagmhm ${⊢}\left({R}\in \mathrm{Mnd}\wedge {I}\in {W}\right)\to {F}\in \left({R}\mathrm{MndHom}{Y}\right)$

Proof

Step Hyp Ref Expression
1 pwsdiagmhm.y ${⊢}{Y}={R}{↑}_{𝑠}{I}$
2 pwsdiagmhm.b ${⊢}{B}={\mathrm{Base}}_{{R}}$
3 pwsdiagmhm.f ${⊢}{F}=\left({x}\in {B}⟼{I}×\left\{{x}\right\}\right)$
4 simpl ${⊢}\left({R}\in \mathrm{Mnd}\wedge {I}\in {W}\right)\to {R}\in \mathrm{Mnd}$
5 1 pwsmnd ${⊢}\left({R}\in \mathrm{Mnd}\wedge {I}\in {W}\right)\to {Y}\in \mathrm{Mnd}$
6 2 fvexi ${⊢}{B}\in \mathrm{V}$
7 3 fdiagfn ${⊢}\left({B}\in \mathrm{V}\wedge {I}\in {W}\right)\to {F}:{B}⟶{{B}}^{{I}}$
8 6 7 mpan ${⊢}{I}\in {W}\to {F}:{B}⟶{{B}}^{{I}}$
9 8 adantl ${⊢}\left({R}\in \mathrm{Mnd}\wedge {I}\in {W}\right)\to {F}:{B}⟶{{B}}^{{I}}$
10 1 2 pwsbas ${⊢}\left({R}\in \mathrm{Mnd}\wedge {I}\in {W}\right)\to {{B}}^{{I}}={\mathrm{Base}}_{{Y}}$
11 10 feq3d ${⊢}\left({R}\in \mathrm{Mnd}\wedge {I}\in {W}\right)\to \left({F}:{B}⟶{{B}}^{{I}}↔{F}:{B}⟶{\mathrm{Base}}_{{Y}}\right)$
12 9 11 mpbid ${⊢}\left({R}\in \mathrm{Mnd}\wedge {I}\in {W}\right)\to {F}:{B}⟶{\mathrm{Base}}_{{Y}}$
13 simplr ${⊢}\left(\left({R}\in \mathrm{Mnd}\wedge {I}\in {W}\right)\wedge \left({a}\in {B}\wedge {b}\in {B}\right)\right)\to {I}\in {W}$
14 eqid ${⊢}{+}_{{R}}={+}_{{R}}$
15 2 14 mndcl ${⊢}\left({R}\in \mathrm{Mnd}\wedge {a}\in {B}\wedge {b}\in {B}\right)\to {a}{+}_{{R}}{b}\in {B}$
16 15 3expb ${⊢}\left({R}\in \mathrm{Mnd}\wedge \left({a}\in {B}\wedge {b}\in {B}\right)\right)\to {a}{+}_{{R}}{b}\in {B}$
17 16 adantlr ${⊢}\left(\left({R}\in \mathrm{Mnd}\wedge {I}\in {W}\right)\wedge \left({a}\in {B}\wedge {b}\in {B}\right)\right)\to {a}{+}_{{R}}{b}\in {B}$
18 3 fvdiagfn ${⊢}\left({I}\in {W}\wedge {a}{+}_{{R}}{b}\in {B}\right)\to {F}\left({a}{+}_{{R}}{b}\right)={I}×\left\{{a}{+}_{{R}}{b}\right\}$
19 13 17 18 syl2anc ${⊢}\left(\left({R}\in \mathrm{Mnd}\wedge {I}\in {W}\right)\wedge \left({a}\in {B}\wedge {b}\in {B}\right)\right)\to {F}\left({a}{+}_{{R}}{b}\right)={I}×\left\{{a}{+}_{{R}}{b}\right\}$
20 3 fvdiagfn ${⊢}\left({I}\in {W}\wedge {a}\in {B}\right)\to {F}\left({a}\right)={I}×\left\{{a}\right\}$
21 3 fvdiagfn ${⊢}\left({I}\in {W}\wedge {b}\in {B}\right)\to {F}\left({b}\right)={I}×\left\{{b}\right\}$
22 20 21 oveqan12d ${⊢}\left(\left({I}\in {W}\wedge {a}\in {B}\right)\wedge \left({I}\in {W}\wedge {b}\in {B}\right)\right)\to {F}\left({a}\right){+}_{{Y}}{F}\left({b}\right)=\left({I}×\left\{{a}\right\}\right){+}_{{Y}}\left({I}×\left\{{b}\right\}\right)$
23 22 anandis ${⊢}\left({I}\in {W}\wedge \left({a}\in {B}\wedge {b}\in {B}\right)\right)\to {F}\left({a}\right){+}_{{Y}}{F}\left({b}\right)=\left({I}×\left\{{a}\right\}\right){+}_{{Y}}\left({I}×\left\{{b}\right\}\right)$
24 23 adantll ${⊢}\left(\left({R}\in \mathrm{Mnd}\wedge {I}\in {W}\right)\wedge \left({a}\in {B}\wedge {b}\in {B}\right)\right)\to {F}\left({a}\right){+}_{{Y}}{F}\left({b}\right)=\left({I}×\left\{{a}\right\}\right){+}_{{Y}}\left({I}×\left\{{b}\right\}\right)$
25 eqid ${⊢}{\mathrm{Base}}_{{Y}}={\mathrm{Base}}_{{Y}}$
26 simpll ${⊢}\left(\left({R}\in \mathrm{Mnd}\wedge {I}\in {W}\right)\wedge \left({a}\in {B}\wedge {b}\in {B}\right)\right)\to {R}\in \mathrm{Mnd}$
27 1 2 25 pwsdiagel ${⊢}\left(\left({R}\in \mathrm{Mnd}\wedge {I}\in {W}\right)\wedge {a}\in {B}\right)\to {I}×\left\{{a}\right\}\in {\mathrm{Base}}_{{Y}}$
28 27 adantrr ${⊢}\left(\left({R}\in \mathrm{Mnd}\wedge {I}\in {W}\right)\wedge \left({a}\in {B}\wedge {b}\in {B}\right)\right)\to {I}×\left\{{a}\right\}\in {\mathrm{Base}}_{{Y}}$
29 1 2 25 pwsdiagel ${⊢}\left(\left({R}\in \mathrm{Mnd}\wedge {I}\in {W}\right)\wedge {b}\in {B}\right)\to {I}×\left\{{b}\right\}\in {\mathrm{Base}}_{{Y}}$
30 29 adantrl ${⊢}\left(\left({R}\in \mathrm{Mnd}\wedge {I}\in {W}\right)\wedge \left({a}\in {B}\wedge {b}\in {B}\right)\right)\to {I}×\left\{{b}\right\}\in {\mathrm{Base}}_{{Y}}$
31 eqid ${⊢}{+}_{{Y}}={+}_{{Y}}$
32 1 25 26 13 28 30 14 31 pwsplusgval ${⊢}\left(\left({R}\in \mathrm{Mnd}\wedge {I}\in {W}\right)\wedge \left({a}\in {B}\wedge {b}\in {B}\right)\right)\to \left({I}×\left\{{a}\right\}\right){+}_{{Y}}\left({I}×\left\{{b}\right\}\right)=\left({I}×\left\{{a}\right\}\right){{+}_{{R}}}_{f}\left({I}×\left\{{b}\right\}\right)$
33 id ${⊢}{I}\in {W}\to {I}\in {W}$
34 vex ${⊢}{a}\in \mathrm{V}$
35 34 a1i ${⊢}{I}\in {W}\to {a}\in \mathrm{V}$
36 vex ${⊢}{b}\in \mathrm{V}$
37 36 a1i ${⊢}{I}\in {W}\to {b}\in \mathrm{V}$
38 33 35 37 ofc12 ${⊢}{I}\in {W}\to \left({I}×\left\{{a}\right\}\right){{+}_{{R}}}_{f}\left({I}×\left\{{b}\right\}\right)={I}×\left\{{a}{+}_{{R}}{b}\right\}$
39 38 ad2antlr ${⊢}\left(\left({R}\in \mathrm{Mnd}\wedge {I}\in {W}\right)\wedge \left({a}\in {B}\wedge {b}\in {B}\right)\right)\to \left({I}×\left\{{a}\right\}\right){{+}_{{R}}}_{f}\left({I}×\left\{{b}\right\}\right)={I}×\left\{{a}{+}_{{R}}{b}\right\}$
40 24 32 39 3eqtrd ${⊢}\left(\left({R}\in \mathrm{Mnd}\wedge {I}\in {W}\right)\wedge \left({a}\in {B}\wedge {b}\in {B}\right)\right)\to {F}\left({a}\right){+}_{{Y}}{F}\left({b}\right)={I}×\left\{{a}{+}_{{R}}{b}\right\}$
41 19 40 eqtr4d ${⊢}\left(\left({R}\in \mathrm{Mnd}\wedge {I}\in {W}\right)\wedge \left({a}\in {B}\wedge {b}\in {B}\right)\right)\to {F}\left({a}{+}_{{R}}{b}\right)={F}\left({a}\right){+}_{{Y}}{F}\left({b}\right)$
42 41 ralrimivva ${⊢}\left({R}\in \mathrm{Mnd}\wedge {I}\in {W}\right)\to \forall {a}\in {B}\phantom{\rule{.4em}{0ex}}\forall {b}\in {B}\phantom{\rule{.4em}{0ex}}{F}\left({a}{+}_{{R}}{b}\right)={F}\left({a}\right){+}_{{Y}}{F}\left({b}\right)$
43 simpr ${⊢}\left({R}\in \mathrm{Mnd}\wedge {I}\in {W}\right)\to {I}\in {W}$
44 eqid ${⊢}{0}_{{R}}={0}_{{R}}$
45 2 44 mndidcl ${⊢}{R}\in \mathrm{Mnd}\to {0}_{{R}}\in {B}$
46 45 adantr ${⊢}\left({R}\in \mathrm{Mnd}\wedge {I}\in {W}\right)\to {0}_{{R}}\in {B}$
47 3 fvdiagfn ${⊢}\left({I}\in {W}\wedge {0}_{{R}}\in {B}\right)\to {F}\left({0}_{{R}}\right)={I}×\left\{{0}_{{R}}\right\}$
48 43 46 47 syl2anc ${⊢}\left({R}\in \mathrm{Mnd}\wedge {I}\in {W}\right)\to {F}\left({0}_{{R}}\right)={I}×\left\{{0}_{{R}}\right\}$
49 1 44 pws0g ${⊢}\left({R}\in \mathrm{Mnd}\wedge {I}\in {W}\right)\to {I}×\left\{{0}_{{R}}\right\}={0}_{{Y}}$
50 48 49 eqtrd ${⊢}\left({R}\in \mathrm{Mnd}\wedge {I}\in {W}\right)\to {F}\left({0}_{{R}}\right)={0}_{{Y}}$
51 12 42 50 3jca ${⊢}\left({R}\in \mathrm{Mnd}\wedge {I}\in {W}\right)\to \left({F}:{B}⟶{\mathrm{Base}}_{{Y}}\wedge \forall {a}\in {B}\phantom{\rule{.4em}{0ex}}\forall {b}\in {B}\phantom{\rule{.4em}{0ex}}{F}\left({a}{+}_{{R}}{b}\right)={F}\left({a}\right){+}_{{Y}}{F}\left({b}\right)\wedge {F}\left({0}_{{R}}\right)={0}_{{Y}}\right)$
52 eqid ${⊢}{0}_{{Y}}={0}_{{Y}}$
53 2 25 14 31 44 52 ismhm ${⊢}{F}\in \left({R}\mathrm{MndHom}{Y}\right)↔\left(\left({R}\in \mathrm{Mnd}\wedge {Y}\in \mathrm{Mnd}\right)\wedge \left({F}:{B}⟶{\mathrm{Base}}_{{Y}}\wedge \forall {a}\in {B}\phantom{\rule{.4em}{0ex}}\forall {b}\in {B}\phantom{\rule{.4em}{0ex}}{F}\left({a}{+}_{{R}}{b}\right)={F}\left({a}\right){+}_{{Y}}{F}\left({b}\right)\wedge {F}\left({0}_{{R}}\right)={0}_{{Y}}\right)\right)$
54 4 5 51 53 syl21anbrc ${⊢}\left({R}\in \mathrm{Mnd}\wedge {I}\in {W}\right)\to {F}\in \left({R}\mathrm{MndHom}{Y}\right)$