Theorem frmdplusg

Description: The monoid operation of a free monoid. (Contributed by Mario Carneiro, 27-Sep-2015) (Revised by Mario Carneiro, 27-Feb-2016) (Proof shortened by AV, 6-Nov-2024)

	Ref	Expression
Hypotheses	frmdbas.m	$$⊢M=\mathrm{freeMnd}\left(I\right)$$
	frmdbas.b	$$⊢B={\mathrm{Base}}_M$$
	frmdplusg.p	$$⊢\underset{\dot{}}{+}={+}_M$$
Assertion	frmdplusg	$$⊢\underset{\dot{}}{+}={\mathrm{++}\upharpoonright }_{\left(B\times B\right)}$$

Proof

Step	Hyp	Ref	Expression
1		frmdbas.m	$$⊢M=\mathrm{freeMnd}\left(I\right)$$
2		frmdbas.b	$$⊢B={\mathrm{Base}}_M$$
3		frmdplusg.p	$$⊢\underset{\dot{}}{+}={+}_M$$
4	1 2	frmdbas	$$⊢I\in \mathrm{V}\to B=\mathrm{Word}I$$
5		eqid	$$⊢{\mathrm{++}\upharpoonright }_{\left(B\times B\right)}={\mathrm{++}\upharpoonright }_{\left(B\times B\right)}$$
6	1 4 5	frmdval	$$⊢I\in \mathrm{V}\to M=\left\{⟨{\mathrm{Base}}_{\mathrm{ndx}},B⟩,⟨{+}_{\mathrm{ndx}},{\mathrm{++}\upharpoonright }_{\left(B\times B\right)}⟩\right\}$$
7	6	fveq2d	$$⊢I\in \mathrm{V}\to {+}_M={+}_{\left\{⟨{\mathrm{Base}}_{\mathrm{ndx}},B⟩,⟨{+}_{\mathrm{ndx}},{\mathrm{++}\upharpoonright }_{\left(B\times B\right)}⟩\right\}}$$
8	3 7	eqtrid	$$⊢I\in \mathrm{V}\to \underset{\dot{}}{+}={+}_{\left\{⟨{\mathrm{Base}}_{\mathrm{ndx}},B⟩,⟨{+}_{\mathrm{ndx}},{\mathrm{++}\upharpoonright }_{\left(B\times B\right)}⟩\right\}}$$
9		wrdexg	$$⊢I\in \mathrm{V}\to \mathrm{Word}I\in \mathrm{V}$$
10		ccatfn	$$⊢\mathrm{++}Fn\left(\mathrm{V}\times \mathrm{V}\right)$$
11		xpss	$$⊢B\times B\subseteq \mathrm{V}\times \mathrm{V}$$
12		fnssres	$$⊢\left(\mathrm{++}Fn\left(\mathrm{V}\times \mathrm{V}\right)\wedge B\times B\subseteq \mathrm{V}\times \mathrm{V}\right)\to \left({\mathrm{++}\upharpoonright }_{\left(B\times B\right)}\right)Fn\left(B\times B\right)$$
13	10 11 12	mp2an	$$⊢\left({\mathrm{++}\upharpoonright }_{\left(B\times B\right)}\right)Fn\left(B\times B\right)$$
14		ovres	$$⊢\left(x\in B\wedge y\in B\right)\to x\left({\mathrm{++}\upharpoonright }_{\left(B\times B\right)}\right)y=x\mathrm{++}y$$
15	1 2	frmdelbas	$$⊢x\in B\to x\in \mathrm{Word}I$$
16	1 2	frmdelbas	$$⊢y\in B\to y\in \mathrm{Word}I$$
17		ccatcl	$$⊢\left(x\in \mathrm{Word}I\wedge y\in \mathrm{Word}I\right)\to x\mathrm{++}y\in \mathrm{Word}I$$
18	15 16 17	syl2an	$$⊢\left(x\in B\wedge y\in B\right)\to x\mathrm{++}y\in \mathrm{Word}I$$
19	14 18	eqeltrd	$$⊢\left(x\in B\wedge y\in B\right)\to x\left({\mathrm{++}\upharpoonright }_{\left(B\times B\right)}\right)y\in \mathrm{Word}I$$
20	19	rgen2	$$⊢\forall x\in B\forall y\in Bx\left({\mathrm{++}\upharpoonright }_{\left(B\times B\right)}\right)y\in \mathrm{Word}I$$
21		ffnov	$$⊢\left({\mathrm{++}\upharpoonright }_{\left(B\times B\right)}\right):B\times B⟶\mathrm{Word}I\leftrightarrow \left(\left({\mathrm{++}\upharpoonright }_{\left(B\times B\right)}\right)Fn\left(B\times B\right)\wedge \forall x\in B\forall y\in Bx\left({\mathrm{++}\upharpoonright }_{\left(B\times B\right)}\right)y\in \mathrm{Word}I\right)$$
22	13 20 21	mpbir2an	$$⊢\left({\mathrm{++}\upharpoonright }_{\left(B\times B\right)}\right):B\times B⟶\mathrm{Word}I$$
23	2	fvexi	$$⊢B\in \mathrm{V}$$
24	23 23	xpex	$$⊢B\times B\in \mathrm{V}$$
25		fex2	$$⊢\left(\left({\mathrm{++}\upharpoonright }_{\left(B\times B\right)}\right):B\times B⟶\mathrm{Word}I\wedge B\times B\in \mathrm{V}\wedge \mathrm{Word}I\in \mathrm{V}\right)\to {\mathrm{++}\upharpoonright }_{\left(B\times B\right)}\in \mathrm{V}$$
26	22 24 25	mp3an12	$$⊢\mathrm{Word}I\in \mathrm{V}\to {\mathrm{++}\upharpoonright }_{\left(B\times B\right)}\in \mathrm{V}$$
27		eqid	$$⊢\left\{⟨{\mathrm{Base}}_{\mathrm{ndx}},B⟩,⟨{+}_{\mathrm{ndx}},{\mathrm{++}\upharpoonright }_{\left(B\times B\right)}⟩\right\}=\left\{⟨{\mathrm{Base}}_{\mathrm{ndx}},B⟩,⟨{+}_{\mathrm{ndx}},{\mathrm{++}\upharpoonright }_{\left(B\times B\right)}⟩\right\}$$
28	27	grpplusg	$$⊢{\mathrm{++}\upharpoonright }_{\left(B\times B\right)}\in \mathrm{V}\to {\mathrm{++}\upharpoonright }_{\left(B\times B\right)}={+}_{\left\{⟨{\mathrm{Base}}_{\mathrm{ndx}},B⟩,⟨{+}_{\mathrm{ndx}},{\mathrm{++}\upharpoonright }_{\left(B\times B\right)}⟩\right\}}$$
29	9 26 28	3syl	$$⊢I\in \mathrm{V}\to {\mathrm{++}\upharpoonright }_{\left(B\times B\right)}={+}_{\left\{⟨{\mathrm{Base}}_{\mathrm{ndx}},B⟩,⟨{+}_{\mathrm{ndx}},{\mathrm{++}\upharpoonright }_{\left(B\times B\right)}⟩\right\}}$$
30	8 29	eqtr4d	$$⊢I\in \mathrm{V}\to \underset{\dot{}}{+}={\mathrm{++}\upharpoonright }_{\left(B\times B\right)}$$
31		fvprc	$$⊢\neg I\in \mathrm{V}\to \mathrm{freeMnd}\left(I\right)=\varnothing$$
32	1 31	eqtrid	$$⊢\neg I\in \mathrm{V}\to M=\varnothing$$
33	32	fveq2d	$$⊢\neg I\in \mathrm{V}\to {+}_M={+}_{\varnothing }$$
34	3 33	eqtrid	$$⊢\neg I\in \mathrm{V}\to \underset{\dot{}}{+}={+}_{\varnothing }$$
35		res0	$$⊢{\mathrm{++}\upharpoonright }_{\varnothing }=\varnothing$$
36		plusgid	$$⊢{+}_{𝑔}=\mathrm{Slot}{+}_{\mathrm{ndx}}$$
37	36	str0	$$⊢\varnothing ={+}_{\varnothing }$$
38	35 37	eqtr2i	$$⊢{+}_{\varnothing }={\mathrm{++}\upharpoonright }_{\varnothing }$$
39	34 38	eqtrdi	$$⊢\neg I\in \mathrm{V}\to \underset{\dot{}}{+}={\mathrm{++}\upharpoonright }_{\varnothing }$$
40	32	fveq2d	$$⊢\neg I\in \mathrm{V}\to {\mathrm{Base}}_M={\mathrm{Base}}_{\varnothing }$$
41		base0	$$⊢\varnothing ={\mathrm{Base}}_{\varnothing }$$
42	40 2 41	3eqtr4g	$$⊢\neg I\in \mathrm{V}\to B=\varnothing$$
43	42	xpeq2d	$$⊢\neg I\in \mathrm{V}\to B\times B=B\times \varnothing$$
44		xp0	$$⊢B\times \varnothing =\varnothing$$
45	43 44	eqtrdi	$$⊢\neg I\in \mathrm{V}\to B\times B=\varnothing$$
46	45	reseq2d	$$⊢\neg I\in \mathrm{V}\to {\mathrm{++}\upharpoonright }_{\left(B\times B\right)}={\mathrm{++}\upharpoonright }_{\varnothing }$$
47	39 46	eqtr4d	$$⊢\neg I\in \mathrm{V}\to \underset{\dot{}}{+}={\mathrm{++}\upharpoonright }_{\left(B\times B\right)}$$
48	30 47	pm2.61i	$$⊢\underset{\dot{}}{+}={\mathrm{++}\upharpoonright }_{\left(B\times B\right)}$$