Theorem frmdplusg

Description: The monoid operation of a free monoid. (Contributed by Mario Carneiro, 27-Sep-2015) (Revised by Mario Carneiro, 27-Feb-2016)

	Ref	Expression
Hypotheses	frmdbas.m	⊢ 𝑀 = ( freeMnd ‘ 𝐼 )
	frmdbas.b	⊢ 𝐵 = ( Base ‘ 𝑀 )
	frmdplusg.p	⊢ + = ( +g ‘ 𝑀 )
Assertion	frmdplusg	⊢ + = ( ++ ↾ ( 𝐵 × 𝐵 ) )

Proof

Step	Hyp	Ref	Expression
1		frmdbas.m	⊢ 𝑀 = ( freeMnd ‘ 𝐼 )
2		frmdbas.b	⊢ 𝐵 = ( Base ‘ 𝑀 )
3		frmdplusg.p	⊢ + = ( +g ‘ 𝑀 )
4	1 2	frmdbas	⊢ ( 𝐼 ∈ V → 𝐵 = Word 𝐼 )
5		eqid	⊢ ( ++ ↾ ( 𝐵 × 𝐵 ) ) = ( ++ ↾ ( 𝐵 × 𝐵 ) )
6	1 4 5	frmdval	⊢ ( 𝐼 ∈ V → 𝑀 = { ⟨ ( Base ‘ ndx ) , 𝐵 ⟩ , ⟨ ( +g ‘ ndx ) , ( ++ ↾ ( 𝐵 × 𝐵 ) ) ⟩ } )
7	6	fveq2d	⊢ ( 𝐼 ∈ V → ( +g ‘ 𝑀 ) = ( +g ‘ { ⟨ ( Base ‘ ndx ) , 𝐵 ⟩ , ⟨ ( +g ‘ ndx ) , ( ++ ↾ ( 𝐵 × 𝐵 ) ) ⟩ } ) )
8	3 7	syl5eq	⊢ ( 𝐼 ∈ V → + = ( +g ‘ { ⟨ ( Base ‘ ndx ) , 𝐵 ⟩ , ⟨ ( +g ‘ ndx ) , ( ++ ↾ ( 𝐵 × 𝐵 ) ) ⟩ } ) )
9		wrdexg	⊢ ( 𝐼 ∈ V → Word 𝐼 ∈ V )
10		ccatfn	⊢ ++ Fn ( V × V )
11		xpss	⊢ ( 𝐵 × 𝐵 ) ⊆ ( V × V )
12		fnssres	⊢ ( ( ++ Fn ( V × V ) ∧ ( 𝐵 × 𝐵 ) ⊆ ( V × V ) ) → ( ++ ↾ ( 𝐵 × 𝐵 ) ) Fn ( 𝐵 × 𝐵 ) )
13	10 11 12	mp2an	⊢ ( ++ ↾ ( 𝐵 × 𝐵 ) ) Fn ( 𝐵 × 𝐵 )
14		ovres	⊢ ( ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) → ( 𝑥 ( ++ ↾ ( 𝐵 × 𝐵 ) ) 𝑦 ) = ( 𝑥 ++ 𝑦 ) )
15	1 2	frmdelbas	⊢ ( 𝑥 ∈ 𝐵 → 𝑥 ∈ Word 𝐼 )
16	1 2	frmdelbas	⊢ ( 𝑦 ∈ 𝐵 → 𝑦 ∈ Word 𝐼 )
17		ccatcl	⊢ ( ( 𝑥 ∈ Word 𝐼 ∧ 𝑦 ∈ Word 𝐼 ) → ( 𝑥 ++ 𝑦 ) ∈ Word 𝐼 )
18	15 16 17	syl2an	⊢ ( ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) → ( 𝑥 ++ 𝑦 ) ∈ Word 𝐼 )
19	14 18	eqeltrd	⊢ ( ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) → ( 𝑥 ( ++ ↾ ( 𝐵 × 𝐵 ) ) 𝑦 ) ∈ Word 𝐼 )
20	19	rgen2	⊢ ∀ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ( 𝑥 ( ++ ↾ ( 𝐵 × 𝐵 ) ) 𝑦 ) ∈ Word 𝐼
21		ffnov	⊢ ( ( ++ ↾ ( 𝐵 × 𝐵 ) ) : ( 𝐵 × 𝐵 ) ⟶ Word 𝐼 ↔ ( ( ++ ↾ ( 𝐵 × 𝐵 ) ) Fn ( 𝐵 × 𝐵 ) ∧ ∀ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ( 𝑥 ( ++ ↾ ( 𝐵 × 𝐵 ) ) 𝑦 ) ∈ Word 𝐼 ) )
22	13 20 21	mpbir2an	⊢ ( ++ ↾ ( 𝐵 × 𝐵 ) ) : ( 𝐵 × 𝐵 ) ⟶ Word 𝐼
23	2	fvexi	⊢ 𝐵 ∈ V
24	23 23	xpex	⊢ ( 𝐵 × 𝐵 ) ∈ V
25		fex2	⊢ ( ( ( ++ ↾ ( 𝐵 × 𝐵 ) ) : ( 𝐵 × 𝐵 ) ⟶ Word 𝐼 ∧ ( 𝐵 × 𝐵 ) ∈ V ∧ Word 𝐼 ∈ V ) → ( ++ ↾ ( 𝐵 × 𝐵 ) ) ∈ V )
26	22 24 25	mp3an12	⊢ ( Word 𝐼 ∈ V → ( ++ ↾ ( 𝐵 × 𝐵 ) ) ∈ V )
27		eqid	⊢ { ⟨ ( Base ‘ ndx ) , 𝐵 ⟩ , ⟨ ( +g ‘ ndx ) , ( ++ ↾ ( 𝐵 × 𝐵 ) ) ⟩ } = { ⟨ ( Base ‘ ndx ) , 𝐵 ⟩ , ⟨ ( +g ‘ ndx ) , ( ++ ↾ ( 𝐵 × 𝐵 ) ) ⟩ }
28	27	grpplusg	⊢ ( ( ++ ↾ ( 𝐵 × 𝐵 ) ) ∈ V → ( ++ ↾ ( 𝐵 × 𝐵 ) ) = ( +g ‘ { ⟨ ( Base ‘ ndx ) , 𝐵 ⟩ , ⟨ ( +g ‘ ndx ) , ( ++ ↾ ( 𝐵 × 𝐵 ) ) ⟩ } ) )
29	9 26 28	3syl	⊢ ( 𝐼 ∈ V → ( ++ ↾ ( 𝐵 × 𝐵 ) ) = ( +g ‘ { ⟨ ( Base ‘ ndx ) , 𝐵 ⟩ , ⟨ ( +g ‘ ndx ) , ( ++ ↾ ( 𝐵 × 𝐵 ) ) ⟩ } ) )
30	8 29	eqtr4d	⊢ ( 𝐼 ∈ V → + = ( ++ ↾ ( 𝐵 × 𝐵 ) ) )
31		fvprc	⊢ ( ¬ 𝐼 ∈ V → ( freeMnd ‘ 𝐼 ) = ∅ )
32	1 31	syl5eq	⊢ ( ¬ 𝐼 ∈ V → 𝑀 = ∅ )
33	32	fveq2d	⊢ ( ¬ 𝐼 ∈ V → ( +g ‘ 𝑀 ) = ( +g ‘ ∅ ) )
34	3 33	syl5eq	⊢ ( ¬ 𝐼 ∈ V → + = ( +g ‘ ∅ ) )
35		res0	⊢ ( ++ ↾ ∅ ) = ∅
36		df-plusg	⊢ +g = Slot 2
37	36	str0	⊢ ∅ = ( +g ‘ ∅ )
38	35 37	eqtr2i	⊢ ( +g ‘ ∅ ) = ( ++ ↾ ∅ )
39	34 38	eqtrdi	⊢ ( ¬ 𝐼 ∈ V → + = ( ++ ↾ ∅ ) )
40	32	fveq2d	⊢ ( ¬ 𝐼 ∈ V → ( Base ‘ 𝑀 ) = ( Base ‘ ∅ ) )
41		base0	⊢ ∅ = ( Base ‘ ∅ )
42	40 2 41	3eqtr4g	⊢ ( ¬ 𝐼 ∈ V → 𝐵 = ∅ )
43	42	xpeq2d	⊢ ( ¬ 𝐼 ∈ V → ( 𝐵 × 𝐵 ) = ( 𝐵 × ∅ ) )
44		xp0	⊢ ( 𝐵 × ∅ ) = ∅
45	43 44	eqtrdi	⊢ ( ¬ 𝐼 ∈ V → ( 𝐵 × 𝐵 ) = ∅ )
46	45	reseq2d	⊢ ( ¬ 𝐼 ∈ V → ( ++ ↾ ( 𝐵 × 𝐵 ) ) = ( ++ ↾ ∅ ) )
47	39 46	eqtr4d	⊢ ( ¬ 𝐼 ∈ V → + = ( ++ ↾ ( 𝐵 × 𝐵 ) ) )
48	30 47	pm2.61i	⊢ + = ( ++ ↾ ( 𝐵 × 𝐵 ) )