This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 )