Theorem ismndd

Description: Deduce a monoid from its properties. (Contributed by Mario Carneiro, 6-Jan-2015)

	Ref	Expression
Hypotheses	ismndd.b	⊢ ( 𝜑 → 𝐵 = ( Base ‘ 𝐺 ) )
	ismndd.p	⊢ ( 𝜑 → + = ( +g ‘ 𝐺 ) )
	ismndd.c	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) → ( 𝑥 + 𝑦 ) ∈ 𝐵 )
	ismndd.a	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵 ) ) → ( ( 𝑥 + 𝑦 ) + 𝑧 ) = ( 𝑥 + ( 𝑦 + 𝑧 ) ) )
	ismndd.z	⊢ ( 𝜑 → 0 ∈ 𝐵 )
	ismndd.i	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐵 ) → ( 0 + 𝑥 ) = 𝑥 )
	ismndd.j	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐵 ) → ( 𝑥 + 0 ) = 𝑥 )
Assertion	ismndd	⊢ ( 𝜑 → 𝐺 ∈ Mnd )

Proof

Step	Hyp	Ref	Expression
1		ismndd.b	⊢ ( 𝜑 → 𝐵 = ( Base ‘ 𝐺 ) )
2		ismndd.p	⊢ ( 𝜑 → + = ( +g ‘ 𝐺 ) )
3		ismndd.c	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) → ( 𝑥 + 𝑦 ) ∈ 𝐵 )
4		ismndd.a	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵 ) ) → ( ( 𝑥 + 𝑦 ) + 𝑧 ) = ( 𝑥 + ( 𝑦 + 𝑧 ) ) )
5		ismndd.z	⊢ ( 𝜑 → 0 ∈ 𝐵 )
6		ismndd.i	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐵 ) → ( 0 + 𝑥 ) = 𝑥 )
7		ismndd.j	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐵 ) → ( 𝑥 + 0 ) = 𝑥 )
8	3	3expb	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ) → ( 𝑥 + 𝑦 ) ∈ 𝐵 )
9		simpll	⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ) ∧ 𝑧 ∈ 𝐵 ) → 𝜑 )
10		simplrl	⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ) ∧ 𝑧 ∈ 𝐵 ) → 𝑥 ∈ 𝐵 )
11		simplrr	⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ) ∧ 𝑧 ∈ 𝐵 ) → 𝑦 ∈ 𝐵 )
12		simpr	⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ) ∧ 𝑧 ∈ 𝐵 ) → 𝑧 ∈ 𝐵 )
13	9 10 11 12 4	syl13anc	⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ) ∧ 𝑧 ∈ 𝐵 ) → ( ( 𝑥 + 𝑦 ) + 𝑧 ) = ( 𝑥 + ( 𝑦 + 𝑧 ) ) )
14	13	ralrimiva	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ) → ∀ 𝑧 ∈ 𝐵 ( ( 𝑥 + 𝑦 ) + 𝑧 ) = ( 𝑥 + ( 𝑦 + 𝑧 ) ) )
15	8 14	jca	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ) → ( ( 𝑥 + 𝑦 ) ∈ 𝐵 ∧ ∀ 𝑧 ∈ 𝐵 ( ( 𝑥 + 𝑦 ) + 𝑧 ) = ( 𝑥 + ( 𝑦 + 𝑧 ) ) ) )
16	15	ralrimivva	⊢ ( 𝜑 → ∀ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ( ( 𝑥 + 𝑦 ) ∈ 𝐵 ∧ ∀ 𝑧 ∈ 𝐵 ( ( 𝑥 + 𝑦 ) + 𝑧 ) = ( 𝑥 + ( 𝑦 + 𝑧 ) ) ) )
17	2	oveqd	⊢ ( 𝜑 → ( 𝑥 + 𝑦 ) = ( 𝑥 ( +g ‘ 𝐺 ) 𝑦 ) )
18	17 1	eleq12d	⊢ ( 𝜑 → ( ( 𝑥 + 𝑦 ) ∈ 𝐵 ↔ ( 𝑥 ( +g ‘ 𝐺 ) 𝑦 ) ∈ ( Base ‘ 𝐺 ) ) )
19		eqidd	⊢ ( 𝜑 → 𝑧 = 𝑧 )
20	2 17 19	oveq123d	⊢ ( 𝜑 → ( ( 𝑥 + 𝑦 ) + 𝑧 ) = ( ( 𝑥 ( +g ‘ 𝐺 ) 𝑦 ) ( +g ‘ 𝐺 ) 𝑧 ) )
21		eqidd	⊢ ( 𝜑 → 𝑥 = 𝑥 )
22	2	oveqd	⊢ ( 𝜑 → ( 𝑦 + 𝑧 ) = ( 𝑦 ( +g ‘ 𝐺 ) 𝑧 ) )
23	2 21 22	oveq123d	⊢ ( 𝜑 → ( 𝑥 + ( 𝑦 + 𝑧 ) ) = ( 𝑥 ( +g ‘ 𝐺 ) ( 𝑦 ( +g ‘ 𝐺 ) 𝑧 ) ) )
24	20 23	eqeq12d	⊢ ( 𝜑 → ( ( ( 𝑥 + 𝑦 ) + 𝑧 ) = ( 𝑥 + ( 𝑦 + 𝑧 ) ) ↔ ( ( 𝑥 ( +g ‘ 𝐺 ) 𝑦 ) ( +g ‘ 𝐺 ) 𝑧 ) = ( 𝑥 ( +g ‘ 𝐺 ) ( 𝑦 ( +g ‘ 𝐺 ) 𝑧 ) ) ) )
25	1 24	raleqbidv	⊢ ( 𝜑 → ( ∀ 𝑧 ∈ 𝐵 ( ( 𝑥 + 𝑦 ) + 𝑧 ) = ( 𝑥 + ( 𝑦 + 𝑧 ) ) ↔ ∀ 𝑧 ∈ ( Base ‘ 𝐺 ) ( ( 𝑥 ( +g ‘ 𝐺 ) 𝑦 ) ( +g ‘ 𝐺 ) 𝑧 ) = ( 𝑥 ( +g ‘ 𝐺 ) ( 𝑦 ( +g ‘ 𝐺 ) 𝑧 ) ) ) )
26	18 25	anbi12d	⊢ ( 𝜑 → ( ( ( 𝑥 + 𝑦 ) ∈ 𝐵 ∧ ∀ 𝑧 ∈ 𝐵 ( ( 𝑥 + 𝑦 ) + 𝑧 ) = ( 𝑥 + ( 𝑦 + 𝑧 ) ) ) ↔ ( ( 𝑥 ( +g ‘ 𝐺 ) 𝑦 ) ∈ ( Base ‘ 𝐺 ) ∧ ∀ 𝑧 ∈ ( Base ‘ 𝐺 ) ( ( 𝑥 ( +g ‘ 𝐺 ) 𝑦 ) ( +g ‘ 𝐺 ) 𝑧 ) = ( 𝑥 ( +g ‘ 𝐺 ) ( 𝑦 ( +g ‘ 𝐺 ) 𝑧 ) ) ) ) )
27	1 26	raleqbidv	⊢ ( 𝜑 → ( ∀ 𝑦 ∈ 𝐵 ( ( 𝑥 + 𝑦 ) ∈ 𝐵 ∧ ∀ 𝑧 ∈ 𝐵 ( ( 𝑥 + 𝑦 ) + 𝑧 ) = ( 𝑥 + ( 𝑦 + 𝑧 ) ) ) ↔ ∀ 𝑦 ∈ ( Base ‘ 𝐺 ) ( ( 𝑥 ( +g ‘ 𝐺 ) 𝑦 ) ∈ ( Base ‘ 𝐺 ) ∧ ∀ 𝑧 ∈ ( Base ‘ 𝐺 ) ( ( 𝑥 ( +g ‘ 𝐺 ) 𝑦 ) ( +g ‘ 𝐺 ) 𝑧 ) = ( 𝑥 ( +g ‘ 𝐺 ) ( 𝑦 ( +g ‘ 𝐺 ) 𝑧 ) ) ) ) )
28	1 27	raleqbidv	⊢ ( 𝜑 → ( ∀ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ( ( 𝑥 + 𝑦 ) ∈ 𝐵 ∧ ∀ 𝑧 ∈ 𝐵 ( ( 𝑥 + 𝑦 ) + 𝑧 ) = ( 𝑥 + ( 𝑦 + 𝑧 ) ) ) ↔ ∀ 𝑥 ∈ ( Base ‘ 𝐺 ) ∀ 𝑦 ∈ ( Base ‘ 𝐺 ) ( ( 𝑥 ( +g ‘ 𝐺 ) 𝑦 ) ∈ ( Base ‘ 𝐺 ) ∧ ∀ 𝑧 ∈ ( Base ‘ 𝐺 ) ( ( 𝑥 ( +g ‘ 𝐺 ) 𝑦 ) ( +g ‘ 𝐺 ) 𝑧 ) = ( 𝑥 ( +g ‘ 𝐺 ) ( 𝑦 ( +g ‘ 𝐺 ) 𝑧 ) ) ) ) )
29	16 28	mpbid	⊢ ( 𝜑 → ∀ 𝑥 ∈ ( Base ‘ 𝐺 ) ∀ 𝑦 ∈ ( Base ‘ 𝐺 ) ( ( 𝑥 ( +g ‘ 𝐺 ) 𝑦 ) ∈ ( Base ‘ 𝐺 ) ∧ ∀ 𝑧 ∈ ( Base ‘ 𝐺 ) ( ( 𝑥 ( +g ‘ 𝐺 ) 𝑦 ) ( +g ‘ 𝐺 ) 𝑧 ) = ( 𝑥 ( +g ‘ 𝐺 ) ( 𝑦 ( +g ‘ 𝐺 ) 𝑧 ) ) ) )
30	5 1	eleqtrd	⊢ ( 𝜑 → 0 ∈ ( Base ‘ 𝐺 ) )
31	1	eleq2d	⊢ ( 𝜑 → ( 𝑥 ∈ 𝐵 ↔ 𝑥 ∈ ( Base ‘ 𝐺 ) ) )
32	31	biimpar	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( Base ‘ 𝐺 ) ) → 𝑥 ∈ 𝐵 )
33	2	adantr	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐵 ) → + = ( +g ‘ 𝐺 ) )
34	33	oveqd	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐵 ) → ( 0 + 𝑥 ) = ( 0 ( +g ‘ 𝐺 ) 𝑥 ) )
35	34 6	eqtr3d	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐵 ) → ( 0 ( +g ‘ 𝐺 ) 𝑥 ) = 𝑥 )
36	33	oveqd	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐵 ) → ( 𝑥 + 0 ) = ( 𝑥 ( +g ‘ 𝐺 ) 0 ) )
37	36 7	eqtr3d	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐵 ) → ( 𝑥 ( +g ‘ 𝐺 ) 0 ) = 𝑥 )
38	35 37	jca	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐵 ) → ( ( 0 ( +g ‘ 𝐺 ) 𝑥 ) = 𝑥 ∧ ( 𝑥 ( +g ‘ 𝐺 ) 0 ) = 𝑥 ) )
39	32 38	syldan	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( Base ‘ 𝐺 ) ) → ( ( 0 ( +g ‘ 𝐺 ) 𝑥 ) = 𝑥 ∧ ( 𝑥 ( +g ‘ 𝐺 ) 0 ) = 𝑥 ) )
40	39	ralrimiva	⊢ ( 𝜑 → ∀ 𝑥 ∈ ( Base ‘ 𝐺 ) ( ( 0 ( +g ‘ 𝐺 ) 𝑥 ) = 𝑥 ∧ ( 𝑥 ( +g ‘ 𝐺 ) 0 ) = 𝑥 ) )
41		oveq1	⊢ ( 𝑢 = 0 → ( 𝑢 ( +g ‘ 𝐺 ) 𝑥 ) = ( 0 ( +g ‘ 𝐺 ) 𝑥 ) )
42	41	eqeq1d	⊢ ( 𝑢 = 0 → ( ( 𝑢 ( +g ‘ 𝐺 ) 𝑥 ) = 𝑥 ↔ ( 0 ( +g ‘ 𝐺 ) 𝑥 ) = 𝑥 ) )
43	42	ovanraleqv	⊢ ( 𝑢 = 0 → ( ∀ 𝑥 ∈ ( Base ‘ 𝐺 ) ( ( 𝑢 ( +g ‘ 𝐺 ) 𝑥 ) = 𝑥 ∧ ( 𝑥 ( +g ‘ 𝐺 ) 𝑢 ) = 𝑥 ) ↔ ∀ 𝑥 ∈ ( Base ‘ 𝐺 ) ( ( 0 ( +g ‘ 𝐺 ) 𝑥 ) = 𝑥 ∧ ( 𝑥 ( +g ‘ 𝐺 ) 0 ) = 𝑥 ) ) )
44	43	rspcev	⊢ ( ( 0 ∈ ( Base ‘ 𝐺 ) ∧ ∀ 𝑥 ∈ ( Base ‘ 𝐺 ) ( ( 0 ( +g ‘ 𝐺 ) 𝑥 ) = 𝑥 ∧ ( 𝑥 ( +g ‘ 𝐺 ) 0 ) = 𝑥 ) ) → ∃ 𝑢 ∈ ( Base ‘ 𝐺 ) ∀ 𝑥 ∈ ( Base ‘ 𝐺 ) ( ( 𝑢 ( +g ‘ 𝐺 ) 𝑥 ) = 𝑥 ∧ ( 𝑥 ( +g ‘ 𝐺 ) 𝑢 ) = 𝑥 ) )
45	30 40 44	syl2anc	⊢ ( 𝜑 → ∃ 𝑢 ∈ ( Base ‘ 𝐺 ) ∀ 𝑥 ∈ ( Base ‘ 𝐺 ) ( ( 𝑢 ( +g ‘ 𝐺 ) 𝑥 ) = 𝑥 ∧ ( 𝑥 ( +g ‘ 𝐺 ) 𝑢 ) = 𝑥 ) )
46		eqid	⊢ ( Base ‘ 𝐺 ) = ( Base ‘ 𝐺 )
47		eqid	⊢ ( +g ‘ 𝐺 ) = ( +g ‘ 𝐺 )
48	46 47	ismnd	⊢ ( 𝐺 ∈ Mnd ↔ ( ∀ 𝑥 ∈ ( Base ‘ 𝐺 ) ∀ 𝑦 ∈ ( Base ‘ 𝐺 ) ( ( 𝑥 ( +g ‘ 𝐺 ) 𝑦 ) ∈ ( Base ‘ 𝐺 ) ∧ ∀ 𝑧 ∈ ( Base ‘ 𝐺 ) ( ( 𝑥 ( +g ‘ 𝐺 ) 𝑦 ) ( +g ‘ 𝐺 ) 𝑧 ) = ( 𝑥 ( +g ‘ 𝐺 ) ( 𝑦 ( +g ‘ 𝐺 ) 𝑧 ) ) ) ∧ ∃ 𝑢 ∈ ( Base ‘ 𝐺 ) ∀ 𝑥 ∈ ( Base ‘ 𝐺 ) ( ( 𝑢 ( +g ‘ 𝐺 ) 𝑥 ) = 𝑥 ∧ ( 𝑥 ( +g ‘ 𝐺 ) 𝑢 ) = 𝑥 ) ) )
49	29 45 48	sylanbrc	⊢ ( 𝜑 → 𝐺 ∈ Mnd )