Metamath Proof Explorer

Theorem ismndo2

Description: The predicate "is a monoid". (Contributed by FL, 2-Nov-2009) (Revised by Mario Carneiro, 22-Dec-2013) (New usage is discouraged.)

Ref Expression
Hypothesis ismndo2.1 ⊢ 𝑋 = ran 𝐺
Assertion ismndo2 ( 𝐺 ∈ 𝐴 → ( 𝐺 ∈ MndOp ↔ ( 𝐺 : ( 𝑋 × 𝑋 ) ⟶ 𝑋 ∧ ∀ 𝑥 ∈ 𝑋 ∀ 𝑦 ∈ 𝑋 ∀ 𝑧 ∈ 𝑋 ( ( 𝑥 𝐺 𝑦 ) 𝐺 𝑧 ) = ( 𝑥 𝐺 ( 𝑦 𝐺 𝑧 ) ) ∧ ∃ 𝑥 ∈ 𝑋 ∀ 𝑦 ∈ 𝑋 ( ( 𝑥 𝐺 𝑦 ) = 𝑦 ∧ ( 𝑦 𝐺 𝑥 ) = 𝑦 ) ) ) )

Proof

Step Hyp Ref Expression
1 ismndo2.1 ⊢ 𝑋 = ran 𝐺
2 mndomgmid ⊢ ( 𝐺 ∈ MndOp → 𝐺 ∈ ( Magma ∩ ExId ) )
3 rngopidOLD ⊢ ( 𝐺 ∈ ( Magma ∩ ExId ) → ran 𝐺 = dom dom 𝐺 )
4 2 3 syl ⊢ ( 𝐺 ∈ MndOp → ran 𝐺 = dom dom 𝐺 )
5 1 4 syl5eq ⊢ ( 𝐺 ∈ MndOp → 𝑋 = dom dom 𝐺 )
6 5 a1i ⊢ ( 𝐺 ∈ 𝐴 → ( 𝐺 ∈ MndOp → 𝑋 = dom dom 𝐺 ) )
7 fdm ⊢ ( 𝐺 : ( 𝑋 × 𝑋 ) ⟶ 𝑋 → dom 𝐺 = ( 𝑋 × 𝑋 ) )
8 7 dmeqd ⊢ ( 𝐺 : ( 𝑋 × 𝑋 ) ⟶ 𝑋 → dom dom 𝐺 = dom ( 𝑋 × 𝑋 ) )
9 dmxpid ⊢ dom ( 𝑋 × 𝑋 ) = 𝑋
10 8 9 eqtr2di ⊢ ( 𝐺 : ( 𝑋 × 𝑋 ) ⟶ 𝑋 → 𝑋 = dom dom 𝐺 )
11 10 3ad2ant1 ⊢ ( ( 𝐺 : ( 𝑋 × 𝑋 ) ⟶ 𝑋 ∧ ∀ 𝑥 ∈ 𝑋 ∀ 𝑦 ∈ 𝑋 ∀ 𝑧 ∈ 𝑋 ( ( 𝑥 𝐺 𝑦 ) 𝐺 𝑧 ) = ( 𝑥 𝐺 ( 𝑦 𝐺 𝑧 ) ) ∧ ∃ 𝑥 ∈ 𝑋 ∀ 𝑦 ∈ 𝑋 ( ( 𝑥 𝐺 𝑦 ) = 𝑦 ∧ ( 𝑦 𝐺 𝑥 ) = 𝑦 ) ) → 𝑋 = dom dom 𝐺 )
12 11 a1i ⊢ ( 𝐺 ∈ 𝐴 → ( ( 𝐺 : ( 𝑋 × 𝑋 ) ⟶ 𝑋 ∧ ∀ 𝑥 ∈ 𝑋 ∀ 𝑦 ∈ 𝑋 ∀ 𝑧 ∈ 𝑋 ( ( 𝑥 𝐺 𝑦 ) 𝐺 𝑧 ) = ( 𝑥 𝐺 ( 𝑦 𝐺 𝑧 ) ) ∧ ∃ 𝑥 ∈ 𝑋 ∀ 𝑦 ∈ 𝑋 ( ( 𝑥 𝐺 𝑦 ) = 𝑦 ∧ ( 𝑦 𝐺 𝑥 ) = 𝑦 ) ) → 𝑋 = dom dom 𝐺 ) )
13 eqid ⊢ dom dom 𝐺 = dom dom 𝐺
14 13 ismndo1 ⊢ ( 𝐺 ∈ 𝐴 → ( 𝐺 ∈ MndOp ↔ ( 𝐺 : ( dom dom 𝐺 × dom dom 𝐺 ) ⟶ dom dom 𝐺 ∧ ∀ 𝑥 ∈ dom dom 𝐺 ∀ 𝑦 ∈ dom dom 𝐺 ∀ 𝑧 ∈ dom dom 𝐺 ( ( 𝑥 𝐺 𝑦 ) 𝐺 𝑧 ) = ( 𝑥 𝐺 ( 𝑦 𝐺 𝑧 ) ) ∧ ∃ 𝑥 ∈ dom dom 𝐺 ∀ 𝑦 ∈ dom dom 𝐺 ( ( 𝑥 𝐺 𝑦 ) = 𝑦 ∧ ( 𝑦 𝐺 𝑥 ) = 𝑦 ) ) ) )
15 xpid11 ⊢ ( ( 𝑋 × 𝑋 ) = ( dom dom 𝐺 × dom dom 𝐺 ) ↔ 𝑋 = dom dom 𝐺 )
16 15 biimpri ⊢ ( 𝑋 = dom dom 𝐺 → ( 𝑋 × 𝑋 ) = ( dom dom 𝐺 × dom dom 𝐺 ) )
17 feq23 ⊢ ( ( ( 𝑋 × 𝑋 ) = ( dom dom 𝐺 × dom dom 𝐺 ) ∧ 𝑋 = dom dom 𝐺 ) → ( 𝐺 : ( 𝑋 × 𝑋 ) ⟶ 𝑋 ↔ 𝐺 : ( dom dom 𝐺 × dom dom 𝐺 ) ⟶ dom dom 𝐺 ) )
18 16 17 mpancom ⊢ ( 𝑋 = dom dom 𝐺 → ( 𝐺 : ( 𝑋 × 𝑋 ) ⟶ 𝑋 ↔ 𝐺 : ( dom dom 𝐺 × dom dom 𝐺 ) ⟶ dom dom 𝐺 ) )
19 raleq ⊢ ( 𝑋 = dom dom 𝐺 → ( ∀ 𝑧 ∈ 𝑋 ( ( 𝑥 𝐺 𝑦 ) 𝐺 𝑧 ) = ( 𝑥 𝐺 ( 𝑦 𝐺 𝑧 ) ) ↔ ∀ 𝑧 ∈ dom dom 𝐺 ( ( 𝑥 𝐺 𝑦 ) 𝐺 𝑧 ) = ( 𝑥 𝐺 ( 𝑦 𝐺 𝑧 ) ) ) )
20 19 raleqbi1dv ⊢ ( 𝑋 = dom dom 𝐺 → ( ∀ 𝑦 ∈ 𝑋 ∀ 𝑧 ∈ 𝑋 ( ( 𝑥 𝐺 𝑦 ) 𝐺 𝑧 ) = ( 𝑥 𝐺 ( 𝑦 𝐺 𝑧 ) ) ↔ ∀ 𝑦 ∈ dom dom 𝐺 ∀ 𝑧 ∈ dom dom 𝐺 ( ( 𝑥 𝐺 𝑦 ) 𝐺 𝑧 ) = ( 𝑥 𝐺 ( 𝑦 𝐺 𝑧 ) ) ) )
21 20 raleqbi1dv ⊢ ( 𝑋 = dom dom 𝐺 → ( ∀ 𝑥 ∈ 𝑋 ∀ 𝑦 ∈ 𝑋 ∀ 𝑧 ∈ 𝑋 ( ( 𝑥 𝐺 𝑦 ) 𝐺 𝑧 ) = ( 𝑥 𝐺 ( 𝑦 𝐺 𝑧 ) ) ↔ ∀ 𝑥 ∈ dom dom 𝐺 ∀ 𝑦 ∈ dom dom 𝐺 ∀ 𝑧 ∈ dom dom 𝐺 ( ( 𝑥 𝐺 𝑦 ) 𝐺 𝑧 ) = ( 𝑥 𝐺 ( 𝑦 𝐺 𝑧 ) ) ) )
22 raleq ⊢ ( 𝑋 = dom dom 𝐺 → ( ∀ 𝑦 ∈ 𝑋 ( ( 𝑥 𝐺 𝑦 ) = 𝑦 ∧ ( 𝑦 𝐺 𝑥 ) = 𝑦 ) ↔ ∀ 𝑦 ∈ dom dom 𝐺 ( ( 𝑥 𝐺 𝑦 ) = 𝑦 ∧ ( 𝑦 𝐺 𝑥 ) = 𝑦 ) ) )
23 22 rexeqbi1dv ⊢ ( 𝑋 = dom dom 𝐺 → ( ∃ 𝑥 ∈ 𝑋 ∀ 𝑦 ∈ 𝑋 ( ( 𝑥 𝐺 𝑦 ) = 𝑦 ∧ ( 𝑦 𝐺 𝑥 ) = 𝑦 ) ↔ ∃ 𝑥 ∈ dom dom 𝐺 ∀ 𝑦 ∈ dom dom 𝐺 ( ( 𝑥 𝐺 𝑦 ) = 𝑦 ∧ ( 𝑦 𝐺 𝑥 ) = 𝑦 ) ) )
24 18 21 23 3anbi123d ⊢ ( 𝑋 = dom dom 𝐺 → ( ( 𝐺 : ( 𝑋 × 𝑋 ) ⟶ 𝑋 ∧ ∀ 𝑥 ∈ 𝑋 ∀ 𝑦 ∈ 𝑋 ∀ 𝑧 ∈ 𝑋 ( ( 𝑥 𝐺 𝑦 ) 𝐺 𝑧 ) = ( 𝑥 𝐺 ( 𝑦 𝐺 𝑧 ) ) ∧ ∃ 𝑥 ∈ 𝑋 ∀ 𝑦 ∈ 𝑋 ( ( 𝑥 𝐺 𝑦 ) = 𝑦 ∧ ( 𝑦 𝐺 𝑥 ) = 𝑦 ) ) ↔ ( 𝐺 : ( dom dom 𝐺 × dom dom 𝐺 ) ⟶ dom dom 𝐺 ∧ ∀ 𝑥 ∈ dom dom 𝐺 ∀ 𝑦 ∈ dom dom 𝐺 ∀ 𝑧 ∈ dom dom 𝐺 ( ( 𝑥 𝐺 𝑦 ) 𝐺 𝑧 ) = ( 𝑥 𝐺 ( 𝑦 𝐺 𝑧 ) ) ∧ ∃ 𝑥 ∈ dom dom 𝐺 ∀ 𝑦 ∈ dom dom 𝐺 ( ( 𝑥 𝐺 𝑦 ) = 𝑦 ∧ ( 𝑦 𝐺 𝑥 ) = 𝑦 ) ) ) )
25 24 bibi2d ⊢ ( 𝑋 = dom dom 𝐺 → ( ( 𝐺 ∈ MndOp ↔ ( 𝐺 : ( 𝑋 × 𝑋 ) ⟶ 𝑋 ∧ ∀ 𝑥 ∈ 𝑋 ∀ 𝑦 ∈ 𝑋 ∀ 𝑧 ∈ 𝑋 ( ( 𝑥 𝐺 𝑦 ) 𝐺 𝑧 ) = ( 𝑥 𝐺 ( 𝑦 𝐺 𝑧 ) ) ∧ ∃ 𝑥 ∈ 𝑋 ∀ 𝑦 ∈ 𝑋 ( ( 𝑥 𝐺 𝑦 ) = 𝑦 ∧ ( 𝑦 𝐺 𝑥 ) = 𝑦 ) ) ) ↔ ( 𝐺 ∈ MndOp ↔ ( 𝐺 : ( dom dom 𝐺 × dom dom 𝐺 ) ⟶ dom dom 𝐺 ∧ ∀ 𝑥 ∈ dom dom 𝐺 ∀ 𝑦 ∈ dom dom 𝐺 ∀ 𝑧 ∈ dom dom 𝐺 ( ( 𝑥 𝐺 𝑦 ) 𝐺 𝑧 ) = ( 𝑥 𝐺 ( 𝑦 𝐺 𝑧 ) ) ∧ ∃ 𝑥 ∈ dom dom 𝐺 ∀ 𝑦 ∈ dom dom 𝐺 ( ( 𝑥 𝐺 𝑦 ) = 𝑦 ∧ ( 𝑦 𝐺 𝑥 ) = 𝑦 ) ) ) ) )
26 14 25 syl5ibrcom ⊢ ( 𝐺 ∈ 𝐴 → ( 𝑋 = dom dom 𝐺 → ( 𝐺 ∈ MndOp ↔ ( 𝐺 : ( 𝑋 × 𝑋 ) ⟶ 𝑋 ∧ ∀ 𝑥 ∈ 𝑋 ∀ 𝑦 ∈ 𝑋 ∀ 𝑧 ∈ 𝑋 ( ( 𝑥 𝐺 𝑦 ) 𝐺 𝑧 ) = ( 𝑥 𝐺 ( 𝑦 𝐺 𝑧 ) ) ∧ ∃ 𝑥 ∈ 𝑋 ∀ 𝑦 ∈ 𝑋 ( ( 𝑥 𝐺 𝑦 ) = 𝑦 ∧ ( 𝑦 𝐺 𝑥 ) = 𝑦 ) ) ) ) )
27 6 12 26 pm5.21ndd ⊢ ( 𝐺 ∈ 𝐴 → ( 𝐺 ∈ MndOp ↔ ( 𝐺 : ( 𝑋 × 𝑋 ) ⟶ 𝑋 ∧ ∀ 𝑥 ∈ 𝑋 ∀ 𝑦 ∈ 𝑋 ∀ 𝑧 ∈ 𝑋 ( ( 𝑥 𝐺 𝑦 ) 𝐺 𝑧 ) = ( 𝑥 𝐺 ( 𝑦 𝐺 𝑧 ) ) ∧ ∃ 𝑥 ∈ 𝑋 ∀ 𝑦 ∈ 𝑋 ( ( 𝑥 𝐺 𝑦 ) = 𝑦 ∧ ( 𝑦 𝐺 𝑥 ) = 𝑦 ) ) ) )