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 syl6req ( 𝐺 : ( 𝑋 × 𝑋 ) ⟶ 𝑋𝑋 = 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 ↔ ( 𝐺 : ( 𝑋 × 𝑋 ) ⟶ 𝑋 ∧ ∀ 𝑥𝑋𝑦𝑋𝑧𝑋 ( ( 𝑥 𝐺 𝑦 ) 𝐺 𝑧 ) = ( 𝑥 𝐺 ( 𝑦 𝐺 𝑧 ) ) ∧ ∃ 𝑥𝑋𝑦𝑋 ( ( 𝑥 𝐺 𝑦 ) = 𝑦 ∧ ( 𝑦 𝐺 𝑥 ) = 𝑦 ) ) ) )