Metamath Proof Explorer

Theorem isass

Description: The predicate "is an associative operation". (Contributed by FL, 1-Nov-2009) (New usage is discouraged.)

Ref Expression
Hypothesis isass.1 ⊢ 𝑋 = dom dom 𝐺
Assertion isass ( 𝐺 ∈ 𝐴 → ( 𝐺 ∈ Ass ↔ ∀ 𝑥 ∈ 𝑋 ∀ 𝑦 ∈ 𝑋 ∀ 𝑧 ∈ 𝑋 ( ( 𝑥 𝐺 𝑦 ) 𝐺 𝑧 ) = ( 𝑥 𝐺 ( 𝑦 𝐺 𝑧 ) ) ) )

Proof

Step Hyp Ref Expression
1 isass.1 ⊢ 𝑋 = dom dom 𝐺
2 dmeq ⊢ ( 𝑔 = 𝐺 → dom 𝑔 = dom 𝐺 )
3 2 dmeqd ⊢ ( 𝑔 = 𝐺 → dom dom 𝑔 = dom dom 𝐺 )
4 3 eleq2d ⊢ ( 𝑔 = 𝐺 → ( 𝑥 ∈ dom dom 𝑔 ↔ 𝑥 ∈ dom dom 𝐺 ) )
5 3 eleq2d ⊢ ( 𝑔 = 𝐺 → ( 𝑦 ∈ dom dom 𝑔 ↔ 𝑦 ∈ dom dom 𝐺 ) )
6 3 eleq2d ⊢ ( 𝑔 = 𝐺 → ( 𝑧 ∈ dom dom 𝑔 ↔ 𝑧 ∈ dom dom 𝐺 ) )
7 4 5 6 3anbi123d ⊢ ( 𝑔 = 𝐺 → ( ( 𝑥 ∈ dom dom 𝑔 ∧ 𝑦 ∈ dom dom 𝑔 ∧ 𝑧 ∈ dom dom 𝑔 ) ↔ ( 𝑥 ∈ dom dom 𝐺 ∧ 𝑦 ∈ dom dom 𝐺 ∧ 𝑧 ∈ dom dom 𝐺 ) ) )
8 oveq ⊢ ( 𝑔 = 𝐺 → ( 𝑥 𝑔 𝑦 ) = ( 𝑥 𝐺 𝑦 ) )
9 8 oveq1d ⊢ ( 𝑔 = 𝐺 → ( ( 𝑥 𝑔 𝑦 ) 𝑔 𝑧 ) = ( ( 𝑥 𝐺 𝑦 ) 𝑔 𝑧 ) )
10 oveq ⊢ ( 𝑔 = 𝐺 → ( ( 𝑥 𝐺 𝑦 ) 𝑔 𝑧 ) = ( ( 𝑥 𝐺 𝑦 ) 𝐺 𝑧 ) )
11 9 10 eqtrd ⊢ ( 𝑔 = 𝐺 → ( ( 𝑥 𝑔 𝑦 ) 𝑔 𝑧 ) = ( ( 𝑥 𝐺 𝑦 ) 𝐺 𝑧 ) )
12 oveq ⊢ ( 𝑔 = 𝐺 → ( 𝑦 𝑔 𝑧 ) = ( 𝑦 𝐺 𝑧 ) )
13 12 oveq2d ⊢ ( 𝑔 = 𝐺 → ( 𝑥 𝑔 ( 𝑦 𝑔 𝑧 ) ) = ( 𝑥 𝑔 ( 𝑦 𝐺 𝑧 ) ) )
14 oveq ⊢ ( 𝑔 = 𝐺 → ( 𝑥 𝑔 ( 𝑦 𝐺 𝑧 ) ) = ( 𝑥 𝐺 ( 𝑦 𝐺 𝑧 ) ) )
15 13 14 eqtrd ⊢ ( 𝑔 = 𝐺 → ( 𝑥 𝑔 ( 𝑦 𝑔 𝑧 ) ) = ( 𝑥 𝐺 ( 𝑦 𝐺 𝑧 ) ) )
16 11 15 eqeq12d ⊢ ( 𝑔 = 𝐺 → ( ( ( 𝑥 𝑔 𝑦 ) 𝑔 𝑧 ) = ( 𝑥 𝑔 ( 𝑦 𝑔 𝑧 ) ) ↔ ( ( 𝑥 𝐺 𝑦 ) 𝐺 𝑧 ) = ( 𝑥 𝐺 ( 𝑦 𝐺 𝑧 ) ) ) )
17 7 16 imbi12d ⊢ ( 𝑔 = 𝐺 → ( ( ( 𝑥 ∈ dom dom 𝑔 ∧ 𝑦 ∈ dom dom 𝑔 ∧ 𝑧 ∈ dom dom 𝑔 ) → ( ( 𝑥 𝑔 𝑦 ) 𝑔 𝑧 ) = ( 𝑥 𝑔 ( 𝑦 𝑔 𝑧 ) ) ) ↔ ( ( 𝑥 ∈ dom dom 𝐺 ∧ 𝑦 ∈ dom dom 𝐺 ∧ 𝑧 ∈ dom dom 𝐺 ) → ( ( 𝑥 𝐺 𝑦 ) 𝐺 𝑧 ) = ( 𝑥 𝐺 ( 𝑦 𝐺 𝑧 ) ) ) ) )
18 17 albidv ⊢ ( 𝑔 = 𝐺 → ( ∀ 𝑧 ( ( 𝑥 ∈ dom dom 𝑔 ∧ 𝑦 ∈ dom dom 𝑔 ∧ 𝑧 ∈ dom dom 𝑔 ) → ( ( 𝑥 𝑔 𝑦 ) 𝑔 𝑧 ) = ( 𝑥 𝑔 ( 𝑦 𝑔 𝑧 ) ) ) ↔ ∀ 𝑧 ( ( 𝑥 ∈ dom dom 𝐺 ∧ 𝑦 ∈ dom dom 𝐺 ∧ 𝑧 ∈ dom dom 𝐺 ) → ( ( 𝑥 𝐺 𝑦 ) 𝐺 𝑧 ) = ( 𝑥 𝐺 ( 𝑦 𝐺 𝑧 ) ) ) ) )
19 18 2albidv ⊢ ( 𝑔 = 𝐺 → ( ∀ 𝑥 ∀ 𝑦 ∀ 𝑧 ( ( 𝑥 ∈ dom dom 𝑔 ∧ 𝑦 ∈ dom dom 𝑔 ∧ 𝑧 ∈ dom dom 𝑔 ) → ( ( 𝑥 𝑔 𝑦 ) 𝑔 𝑧 ) = ( 𝑥 𝑔 ( 𝑦 𝑔 𝑧 ) ) ) ↔ ∀ 𝑥 ∀ 𝑦 ∀ 𝑧 ( ( 𝑥 ∈ dom dom 𝐺 ∧ 𝑦 ∈ dom dom 𝐺 ∧ 𝑧 ∈ dom dom 𝐺 ) → ( ( 𝑥 𝐺 𝑦 ) 𝐺 𝑧 ) = ( 𝑥 𝐺 ( 𝑦 𝐺 𝑧 ) ) ) ) )
20 r3al ⊢ ( ∀ 𝑥 ∈ dom dom 𝑔 ∀ 𝑦 ∈ dom dom 𝑔 ∀ 𝑧 ∈ dom dom 𝑔 ( ( 𝑥 𝑔 𝑦 ) 𝑔 𝑧 ) = ( 𝑥 𝑔 ( 𝑦 𝑔 𝑧 ) ) ↔ ∀ 𝑥 ∀ 𝑦 ∀ 𝑧 ( ( 𝑥 ∈ dom dom 𝑔 ∧ 𝑦 ∈ dom dom 𝑔 ∧ 𝑧 ∈ dom dom 𝑔 ) → ( ( 𝑥 𝑔 𝑦 ) 𝑔 𝑧 ) = ( 𝑥 𝑔 ( 𝑦 𝑔 𝑧 ) ) ) )
21 r3al ⊢ ( ∀ 𝑥 ∈ dom dom 𝐺 ∀ 𝑦 ∈ dom dom 𝐺 ∀ 𝑧 ∈ dom dom 𝐺 ( ( 𝑥 𝐺 𝑦 ) 𝐺 𝑧 ) = ( 𝑥 𝐺 ( 𝑦 𝐺 𝑧 ) ) ↔ ∀ 𝑥 ∀ 𝑦 ∀ 𝑧 ( ( 𝑥 ∈ dom dom 𝐺 ∧ 𝑦 ∈ dom dom 𝐺 ∧ 𝑧 ∈ dom dom 𝐺 ) → ( ( 𝑥 𝐺 𝑦 ) 𝐺 𝑧 ) = ( 𝑥 𝐺 ( 𝑦 𝐺 𝑧 ) ) ) )
22 19 20 21 3bitr4g ⊢ ( 𝑔 = 𝐺 → ( ∀ 𝑥 ∈ dom dom 𝑔 ∀ 𝑦 ∈ dom dom 𝑔 ∀ 𝑧 ∈ dom dom 𝑔 ( ( 𝑥 𝑔 𝑦 ) 𝑔 𝑧 ) = ( 𝑥 𝑔 ( 𝑦 𝑔 𝑧 ) ) ↔ ∀ 𝑥 ∈ dom dom 𝐺 ∀ 𝑦 ∈ dom dom 𝐺 ∀ 𝑧 ∈ dom dom 𝐺 ( ( 𝑥 𝐺 𝑦 ) 𝐺 𝑧 ) = ( 𝑥 𝐺 ( 𝑦 𝐺 𝑧 ) ) ) )
23 1 eqcomi ⊢ dom dom 𝐺 = 𝑋
24 23 a1i ⊢ ( 𝑔 = 𝐺 → dom dom 𝐺 = 𝑋 )
25 24 raleqdv ⊢ ( 𝑔 = 𝐺 → ( ∀ 𝑦 ∈ dom dom 𝐺 ∀ 𝑧 ∈ dom dom 𝐺 ( ( 𝑥 𝐺 𝑦 ) 𝐺 𝑧 ) = ( 𝑥 𝐺 ( 𝑦 𝐺 𝑧 ) ) ↔ ∀ 𝑦 ∈ 𝑋 ∀ 𝑧 ∈ dom dom 𝐺 ( ( 𝑥 𝐺 𝑦 ) 𝐺 𝑧 ) = ( 𝑥 𝐺 ( 𝑦 𝐺 𝑧 ) ) ) )
26 24 25 raleqbidv ⊢ ( 𝑔 = 𝐺 → ( ∀ 𝑥 ∈ dom dom 𝐺 ∀ 𝑦 ∈ dom dom 𝐺 ∀ 𝑧 ∈ dom dom 𝐺 ( ( 𝑥 𝐺 𝑦 ) 𝐺 𝑧 ) = ( 𝑥 𝐺 ( 𝑦 𝐺 𝑧 ) ) ↔ ∀ 𝑥 ∈ 𝑋 ∀ 𝑦 ∈ 𝑋 ∀ 𝑧 ∈ dom dom 𝐺 ( ( 𝑥 𝐺 𝑦 ) 𝐺 𝑧 ) = ( 𝑥 𝐺 ( 𝑦 𝐺 𝑧 ) ) ) )
27 24 raleqdv ⊢ ( 𝑔 = 𝐺 → ( ∀ 𝑧 ∈ dom dom 𝐺 ( ( 𝑥 𝐺 𝑦 ) 𝐺 𝑧 ) = ( 𝑥 𝐺 ( 𝑦 𝐺 𝑧 ) ) ↔ ∀ 𝑧 ∈ 𝑋 ( ( 𝑥 𝐺 𝑦 ) 𝐺 𝑧 ) = ( 𝑥 𝐺 ( 𝑦 𝐺 𝑧 ) ) ) )
28 27 2ralbidv ⊢ ( 𝑔 = 𝐺 → ( ∀ 𝑥 ∈ 𝑋 ∀ 𝑦 ∈ 𝑋 ∀ 𝑧 ∈ dom dom 𝐺 ( ( 𝑥 𝐺 𝑦 ) 𝐺 𝑧 ) = ( 𝑥 𝐺 ( 𝑦 𝐺 𝑧 ) ) ↔ ∀ 𝑥 ∈ 𝑋 ∀ 𝑦 ∈ 𝑋 ∀ 𝑧 ∈ 𝑋 ( ( 𝑥 𝐺 𝑦 ) 𝐺 𝑧 ) = ( 𝑥 𝐺 ( 𝑦 𝐺 𝑧 ) ) ) )
29 22 26 28 3bitrd ⊢ ( 𝑔 = 𝐺 → ( ∀ 𝑥 ∈ dom dom 𝑔 ∀ 𝑦 ∈ dom dom 𝑔 ∀ 𝑧 ∈ dom dom 𝑔 ( ( 𝑥 𝑔 𝑦 ) 𝑔 𝑧 ) = ( 𝑥 𝑔 ( 𝑦 𝑔 𝑧 ) ) ↔ ∀ 𝑥 ∈ 𝑋 ∀ 𝑦 ∈ 𝑋 ∀ 𝑧 ∈ 𝑋 ( ( 𝑥 𝐺 𝑦 ) 𝐺 𝑧 ) = ( 𝑥 𝐺 ( 𝑦 𝐺 𝑧 ) ) ) )
30 df-ass ⊢ Ass = { 𝑔 ∣ ∀ 𝑥 ∈ dom dom 𝑔 ∀ 𝑦 ∈ dom dom 𝑔 ∀ 𝑧 ∈ dom dom 𝑔 ( ( 𝑥 𝑔 𝑦 ) 𝑔 𝑧 ) = ( 𝑥 𝑔 ( 𝑦 𝑔 𝑧 ) ) }
31 29 30 elab2g ⊢ ( 𝐺 ∈ 𝐴 → ( 𝐺 ∈ Ass ↔ ∀ 𝑥 ∈ 𝑋 ∀ 𝑦 ∈ 𝑋 ∀ 𝑧 ∈ 𝑋 ( ( 𝑥 𝐺 𝑦 ) 𝐺 𝑧 ) = ( 𝑥 𝐺 ( 𝑦 𝐺 𝑧 ) ) ) )