Metamath Proof Explorer

Theorem isgrpoi

Description: Properties that determine a group operation. Read N as N ( x ) . (Contributed by NM, 4-Nov-2006) (New usage is discouraged.)

Ref Expression
Hypotheses isgrpoi.1 ⊢ 𝑋 ∈ V
isgrpoi.2 ⊢ 𝐺 : ( 𝑋 × 𝑋 ) ⟶ 𝑋
isgrpoi.3 ⊢ ( ( 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ∧ 𝑧 ∈ 𝑋 ) → ( ( 𝑥 𝐺 𝑦 ) 𝐺 𝑧 ) = ( 𝑥 𝐺 ( 𝑦 𝐺 𝑧 ) ) )
isgrpoi.4 ⊢ 𝑈 ∈ 𝑋
isgrpoi.5 ⊢ ( 𝑥 ∈ 𝑋 → ( 𝑈 𝐺 𝑥 ) = 𝑥 )
isgrpoi.6 ⊢ ( 𝑥 ∈ 𝑋 → 𝑁 ∈ 𝑋 )
isgrpoi.7 ⊢ ( 𝑥 ∈ 𝑋 → ( 𝑁 𝐺 𝑥 ) = 𝑈 )
Assertion isgrpoi 𝐺 ∈ GrpOp

Proof

Step Hyp Ref Expression
1 isgrpoi.1 ⊢ 𝑋 ∈ V
2 isgrpoi.2 ⊢ 𝐺 : ( 𝑋 × 𝑋 ) ⟶ 𝑋
3 isgrpoi.3 ⊢ ( ( 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ∧ 𝑧 ∈ 𝑋 ) → ( ( 𝑥 𝐺 𝑦 ) 𝐺 𝑧 ) = ( 𝑥 𝐺 ( 𝑦 𝐺 𝑧 ) ) )
4 isgrpoi.4 ⊢ 𝑈 ∈ 𝑋
5 isgrpoi.5 ⊢ ( 𝑥 ∈ 𝑋 → ( 𝑈 𝐺 𝑥 ) = 𝑥 )
6 isgrpoi.6 ⊢ ( 𝑥 ∈ 𝑋 → 𝑁 ∈ 𝑋 )
7 isgrpoi.7 ⊢ ( 𝑥 ∈ 𝑋 → ( 𝑁 𝐺 𝑥 ) = 𝑈 )
8 3 rgen3 ⊢ ∀ 𝑥 ∈ 𝑋 ∀ 𝑦 ∈ 𝑋 ∀ 𝑧 ∈ 𝑋 ( ( 𝑥 𝐺 𝑦 ) 𝐺 𝑧 ) = ( 𝑥 𝐺 ( 𝑦 𝐺 𝑧 ) )
9 oveq1 ⊢ ( 𝑦 = 𝑁 → ( 𝑦 𝐺 𝑥 ) = ( 𝑁 𝐺 𝑥 ) )
10 9 eqeq1d ⊢ ( 𝑦 = 𝑁 → ( ( 𝑦 𝐺 𝑥 ) = 𝑈 ↔ ( 𝑁 𝐺 𝑥 ) = 𝑈 ) )
11 10 rspcev ⊢ ( ( 𝑁 ∈ 𝑋 ∧ ( 𝑁 𝐺 𝑥 ) = 𝑈 ) → ∃ 𝑦 ∈ 𝑋 ( 𝑦 𝐺 𝑥 ) = 𝑈 )
12 6 7 11 syl2anc ⊢ ( 𝑥 ∈ 𝑋 → ∃ 𝑦 ∈ 𝑋 ( 𝑦 𝐺 𝑥 ) = 𝑈 )
13 5 12 jca ⊢ ( 𝑥 ∈ 𝑋 → ( ( 𝑈 𝐺 𝑥 ) = 𝑥 ∧ ∃ 𝑦 ∈ 𝑋 ( 𝑦 𝐺 𝑥 ) = 𝑈 ) )
14 13 rgen ⊢ ∀ 𝑥 ∈ 𝑋 ( ( 𝑈 𝐺 𝑥 ) = 𝑥 ∧ ∃ 𝑦 ∈ 𝑋 ( 𝑦 𝐺 𝑥 ) = 𝑈 )
15 oveq1 ⊢ ( 𝑢 = 𝑈 → ( 𝑢 𝐺 𝑥 ) = ( 𝑈 𝐺 𝑥 ) )
16 15 eqeq1d ⊢ ( 𝑢 = 𝑈 → ( ( 𝑢 𝐺 𝑥 ) = 𝑥 ↔ ( 𝑈 𝐺 𝑥 ) = 𝑥 ) )
17 eqeq2 ⊢ ( 𝑢 = 𝑈 → ( ( 𝑦 𝐺 𝑥 ) = 𝑢 ↔ ( 𝑦 𝐺 𝑥 ) = 𝑈 ) )
18 17 rexbidv ⊢ ( 𝑢 = 𝑈 → ( ∃ 𝑦 ∈ 𝑋 ( 𝑦 𝐺 𝑥 ) = 𝑢 ↔ ∃ 𝑦 ∈ 𝑋 ( 𝑦 𝐺 𝑥 ) = 𝑈 ) )
19 16 18 anbi12d ⊢ ( 𝑢 = 𝑈 → ( ( ( 𝑢 𝐺 𝑥 ) = 𝑥 ∧ ∃ 𝑦 ∈ 𝑋 ( 𝑦 𝐺 𝑥 ) = 𝑢 ) ↔ ( ( 𝑈 𝐺 𝑥 ) = 𝑥 ∧ ∃ 𝑦 ∈ 𝑋 ( 𝑦 𝐺 𝑥 ) = 𝑈 ) ) )
20 19 ralbidv ⊢ ( 𝑢 = 𝑈 → ( ∀ 𝑥 ∈ 𝑋 ( ( 𝑢 𝐺 𝑥 ) = 𝑥 ∧ ∃ 𝑦 ∈ 𝑋 ( 𝑦 𝐺 𝑥 ) = 𝑢 ) ↔ ∀ 𝑥 ∈ 𝑋 ( ( 𝑈 𝐺 𝑥 ) = 𝑥 ∧ ∃ 𝑦 ∈ 𝑋 ( 𝑦 𝐺 𝑥 ) = 𝑈 ) ) )
21 20 rspcev ⊢ ( ( 𝑈 ∈ 𝑋 ∧ ∀ 𝑥 ∈ 𝑋 ( ( 𝑈 𝐺 𝑥 ) = 𝑥 ∧ ∃ 𝑦 ∈ 𝑋 ( 𝑦 𝐺 𝑥 ) = 𝑈 ) ) → ∃ 𝑢 ∈ 𝑋 ∀ 𝑥 ∈ 𝑋 ( ( 𝑢 𝐺 𝑥 ) = 𝑥 ∧ ∃ 𝑦 ∈ 𝑋 ( 𝑦 𝐺 𝑥 ) = 𝑢 ) )
22 4 14 21 mp2an ⊢ ∃ 𝑢 ∈ 𝑋 ∀ 𝑥 ∈ 𝑋 ( ( 𝑢 𝐺 𝑥 ) = 𝑥 ∧ ∃ 𝑦 ∈ 𝑋 ( 𝑦 𝐺 𝑥 ) = 𝑢 )
23 1 1 xpex ⊢ ( 𝑋 × 𝑋 ) ∈ V
24 fex ⊢ ( ( 𝐺 : ( 𝑋 × 𝑋 ) ⟶ 𝑋 ∧ ( 𝑋 × 𝑋 ) ∈ V ) → 𝐺 ∈ V )
25 2 23 24 mp2an ⊢ 𝐺 ∈ V
26 5 eqcomd ⊢ ( 𝑥 ∈ 𝑋 → 𝑥 = ( 𝑈 𝐺 𝑥 ) )
27 rspceov ⊢ ( ( 𝑈 ∈ 𝑋 ∧ 𝑥 ∈ 𝑋 ∧ 𝑥 = ( 𝑈 𝐺 𝑥 ) ) → ∃ 𝑦 ∈ 𝑋 ∃ 𝑧 ∈ 𝑋 𝑥 = ( 𝑦 𝐺 𝑧 ) )
28 4 27 mp3an1 ⊢ ( ( 𝑥 ∈ 𝑋 ∧ 𝑥 = ( 𝑈 𝐺 𝑥 ) ) → ∃ 𝑦 ∈ 𝑋 ∃ 𝑧 ∈ 𝑋 𝑥 = ( 𝑦 𝐺 𝑧 ) )
29 26 28 mpdan ⊢ ( 𝑥 ∈ 𝑋 → ∃ 𝑦 ∈ 𝑋 ∃ 𝑧 ∈ 𝑋 𝑥 = ( 𝑦 𝐺 𝑧 ) )
30 29 rgen ⊢ ∀ 𝑥 ∈ 𝑋 ∃ 𝑦 ∈ 𝑋 ∃ 𝑧 ∈ 𝑋 𝑥 = ( 𝑦 𝐺 𝑧 )
31 foov ⊢ ( 𝐺 : ( 𝑋 × 𝑋 ) –onto→ 𝑋 ↔ ( 𝐺 : ( 𝑋 × 𝑋 ) ⟶ 𝑋 ∧ ∀ 𝑥 ∈ 𝑋 ∃ 𝑦 ∈ 𝑋 ∃ 𝑧 ∈ 𝑋 𝑥 = ( 𝑦 𝐺 𝑧 ) ) )
32 2 30 31 mpbir2an ⊢ 𝐺 : ( 𝑋 × 𝑋 ) –onto→ 𝑋
33 forn ⊢ ( 𝐺 : ( 𝑋 × 𝑋 ) –onto→ 𝑋 → ran 𝐺 = 𝑋 )
34 32 33 ax-mp ⊢ ran 𝐺 = 𝑋
35 34 eqcomi ⊢ 𝑋 = ran 𝐺
36 35 isgrpo ⊢ ( 𝐺 ∈ V → ( 𝐺 ∈ GrpOp ↔ ( 𝐺 : ( 𝑋 × 𝑋 ) ⟶ 𝑋 ∧ ∀ 𝑥 ∈ 𝑋 ∀ 𝑦 ∈ 𝑋 ∀ 𝑧 ∈ 𝑋 ( ( 𝑥 𝐺 𝑦 ) 𝐺 𝑧 ) = ( 𝑥 𝐺 ( 𝑦 𝐺 𝑧 ) ) ∧ ∃ 𝑢 ∈ 𝑋 ∀ 𝑥 ∈ 𝑋 ( ( 𝑢 𝐺 𝑥 ) = 𝑥 ∧ ∃ 𝑦 ∈ 𝑋 ( 𝑦 𝐺 𝑥 ) = 𝑢 ) ) ) )
37 25 36 ax-mp ⊢ ( 𝐺 ∈ GrpOp ↔ ( 𝐺 : ( 𝑋 × 𝑋 ) ⟶ 𝑋 ∧ ∀ 𝑥 ∈ 𝑋 ∀ 𝑦 ∈ 𝑋 ∀ 𝑧 ∈ 𝑋 ( ( 𝑥 𝐺 𝑦 ) 𝐺 𝑧 ) = ( 𝑥 𝐺 ( 𝑦 𝐺 𝑧 ) ) ∧ ∃ 𝑢 ∈ 𝑋 ∀ 𝑥 ∈ 𝑋 ( ( 𝑢 𝐺 𝑥 ) = 𝑥 ∧ ∃ 𝑦 ∈ 𝑋 ( 𝑦 𝐺 𝑥 ) = 𝑢 ) ) )
38 2 8 22 37 mpbir3an ⊢ 𝐺 ∈ GrpOp