imasmnd

Description: The image structure of a monoid is a monoid. (Contributed by Mario Carneiro, 24-Feb-2015)

	Ref	Expression
Hypotheses	imasmnd.u	⊢ ( 𝜑 → 𝑈 = ( 𝐹 “_s 𝑅 ) )
	imasmnd.v	⊢ ( 𝜑 → 𝑉 = ( Base ‘ 𝑅 ) )
	imasmnd.p	⊢ + = ( +_g ‘ 𝑅 )
	imasmnd.f	⊢ ( 𝜑 → 𝐹 : 𝑉 –onto→ 𝐵 )
	imasmnd.e	⊢ ( ( 𝜑 ∧ ( 𝑎 ∈ 𝑉 ∧ 𝑏 ∈ 𝑉 ) ∧ ( 𝑝 ∈ 𝑉 ∧ 𝑞 ∈ 𝑉 ) ) → ( ( ( 𝐹 ‘ 𝑎 ) = ( 𝐹 ‘ 𝑝 ) ∧ ( 𝐹 ‘ 𝑏 ) = ( 𝐹 ‘ 𝑞 ) ) → ( 𝐹 ‘ ( 𝑎 + 𝑏 ) ) = ( 𝐹 ‘ ( 𝑝 + 𝑞 ) ) ) )
	imasmnd.r	⊢ ( 𝜑 → 𝑅 ∈ Mnd )
	imasmnd.z	⊢ 0 = ( 0_g ‘ 𝑅 )
Assertion	imasmnd	⊢ ( 𝜑 → ( 𝑈 ∈ Mnd ∧ ( 𝐹 ‘ 0 ) = ( 0_g ‘ 𝑈 ) ) )

Proof

Step	Hyp	Ref	Expression
1		imasmnd.u	⊢ ( 𝜑 → 𝑈 = ( 𝐹 “_s 𝑅 ) )
2		imasmnd.v	⊢ ( 𝜑 → 𝑉 = ( Base ‘ 𝑅 ) )
3		imasmnd.p	⊢ + = ( +_g ‘ 𝑅 )
4		imasmnd.f	⊢ ( 𝜑 → 𝐹 : 𝑉 –onto→ 𝐵 )
5		imasmnd.e	⊢ ( ( 𝜑 ∧ ( 𝑎 ∈ 𝑉 ∧ 𝑏 ∈ 𝑉 ) ∧ ( 𝑝 ∈ 𝑉 ∧ 𝑞 ∈ 𝑉 ) ) → ( ( ( 𝐹 ‘ 𝑎 ) = ( 𝐹 ‘ 𝑝 ) ∧ ( 𝐹 ‘ 𝑏 ) = ( 𝐹 ‘ 𝑞 ) ) → ( 𝐹 ‘ ( 𝑎 + 𝑏 ) ) = ( 𝐹 ‘ ( 𝑝 + 𝑞 ) ) ) )
6		imasmnd.r	⊢ ( 𝜑 → 𝑅 ∈ Mnd )
7		imasmnd.z	⊢ 0 = ( 0_g ‘ 𝑅 )
8	6	3ad2ant1	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑉 ∧ 𝑦 ∈ 𝑉 ) → 𝑅 ∈ Mnd )
9		simp2	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑉 ∧ 𝑦 ∈ 𝑉 ) → 𝑥 ∈ 𝑉 )
10	2	3ad2ant1	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑉 ∧ 𝑦 ∈ 𝑉 ) → 𝑉 = ( Base ‘ 𝑅 ) )
11	9 10	eleqtrd	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑉 ∧ 𝑦 ∈ 𝑉 ) → 𝑥 ∈ ( Base ‘ 𝑅 ) )
12		simp3	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑉 ∧ 𝑦 ∈ 𝑉 ) → 𝑦 ∈ 𝑉 )
13	12 10	eleqtrd	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑉 ∧ 𝑦 ∈ 𝑉 ) → 𝑦 ∈ ( Base ‘ 𝑅 ) )
14		eqid	⊢ ( Base ‘ 𝑅 ) = ( Base ‘ 𝑅 )
15	14 3	mndcl	⊢ ( ( 𝑅 ∈ Mnd ∧ 𝑥 ∈ ( Base ‘ 𝑅 ) ∧ 𝑦 ∈ ( Base ‘ 𝑅 ) ) → ( 𝑥 + 𝑦 ) ∈ ( Base ‘ 𝑅 ) )
16	8 11 13 15	syl3anc	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑉 ∧ 𝑦 ∈ 𝑉 ) → ( 𝑥 + 𝑦 ) ∈ ( Base ‘ 𝑅 ) )
17	16 10	eleqtrrd	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑉 ∧ 𝑦 ∈ 𝑉 ) → ( 𝑥 + 𝑦 ) ∈ 𝑉 )
18	6	adantr	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝑉 ∧ 𝑦 ∈ 𝑉 ∧ 𝑧 ∈ 𝑉 ) ) → 𝑅 ∈ Mnd )
19	11	3adant3r3	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝑉 ∧ 𝑦 ∈ 𝑉 ∧ 𝑧 ∈ 𝑉 ) ) → 𝑥 ∈ ( Base ‘ 𝑅 ) )
20	13	3adant3r3	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝑉 ∧ 𝑦 ∈ 𝑉 ∧ 𝑧 ∈ 𝑉 ) ) → 𝑦 ∈ ( Base ‘ 𝑅 ) )
21		simpr3	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝑉 ∧ 𝑦 ∈ 𝑉 ∧ 𝑧 ∈ 𝑉 ) ) → 𝑧 ∈ 𝑉 )
22	2	adantr	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝑉 ∧ 𝑦 ∈ 𝑉 ∧ 𝑧 ∈ 𝑉 ) ) → 𝑉 = ( Base ‘ 𝑅 ) )
23	21 22	eleqtrd	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝑉 ∧ 𝑦 ∈ 𝑉 ∧ 𝑧 ∈ 𝑉 ) ) → 𝑧 ∈ ( Base ‘ 𝑅 ) )
24	14 3	mndass	⊢ ( ( 𝑅 ∈ Mnd ∧ ( 𝑥 ∈ ( Base ‘ 𝑅 ) ∧ 𝑦 ∈ ( Base ‘ 𝑅 ) ∧ 𝑧 ∈ ( Base ‘ 𝑅 ) ) ) → ( ( 𝑥 + 𝑦 ) + 𝑧 ) = ( 𝑥 + ( 𝑦 + 𝑧 ) ) )
25	18 19 20 23 24	syl13anc	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝑉 ∧ 𝑦 ∈ 𝑉 ∧ 𝑧 ∈ 𝑉 ) ) → ( ( 𝑥 + 𝑦 ) + 𝑧 ) = ( 𝑥 + ( 𝑦 + 𝑧 ) ) )
26	25	fveq2d	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝑉 ∧ 𝑦 ∈ 𝑉 ∧ 𝑧 ∈ 𝑉 ) ) → ( 𝐹 ‘ ( ( 𝑥 + 𝑦 ) + 𝑧 ) ) = ( 𝐹 ‘ ( 𝑥 + ( 𝑦 + 𝑧 ) ) ) )
27	14 7	mndidcl	⊢ ( 𝑅 ∈ Mnd → 0 ∈ ( Base ‘ 𝑅 ) )
28	6 27	syl	⊢ ( 𝜑 → 0 ∈ ( Base ‘ 𝑅 ) )
29	28 2	eleqtrrd	⊢ ( 𝜑 → 0 ∈ 𝑉 )
30	2	eleq2d	⊢ ( 𝜑 → ( 𝑥 ∈ 𝑉 ↔ 𝑥 ∈ ( Base ‘ 𝑅 ) ) )
31	30	biimpa	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑉 ) → 𝑥 ∈ ( Base ‘ 𝑅 ) )
32	14 3 7	mndlid	⊢ ( ( 𝑅 ∈ Mnd ∧ 𝑥 ∈ ( Base ‘ 𝑅 ) ) → ( 0 + 𝑥 ) = 𝑥 )
33	6 31 32	syl2an2r	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑉 ) → ( 0 + 𝑥 ) = 𝑥 )
34	33	fveq2d	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑉 ) → ( 𝐹 ‘ ( 0 + 𝑥 ) ) = ( 𝐹 ‘ 𝑥 ) )
35	14 3 7	mndrid	⊢ ( ( 𝑅 ∈ Mnd ∧ 𝑥 ∈ ( Base ‘ 𝑅 ) ) → ( 𝑥 + 0 ) = 𝑥 )
36	6 31 35	syl2an2r	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑉 ) → ( 𝑥 + 0 ) = 𝑥 )
37	36	fveq2d	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑉 ) → ( 𝐹 ‘ ( 𝑥 + 0 ) ) = ( 𝐹 ‘ 𝑥 ) )
38	1 2 3 4 5 6 17 26 29 34 37	imasmnd2	⊢ ( 𝜑 → ( 𝑈 ∈ Mnd ∧ ( 𝐹 ‘ 0 ) = ( 0_g ‘ 𝑈 ) ) )

Metamath Proof Explorer

Theorem imasmnd

Proof