Metamath Proof Explorer

Theorem isgrpda

Description: Properties that determine a group operation. (Contributed by Jeff Madsen, 1-Dec-2009) (New usage is discouraged.)

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

Proof

Step Hyp Ref Expression
1 isgrpda.1 ⊢ ( 𝜑 → 𝑋 ∈ V )
2 isgrpda.2 ⊢ ( 𝜑 → 𝐺 : ( 𝑋 × 𝑋 ) ⟶ 𝑋 )
3 isgrpda.3 ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ∧ 𝑧 ∈ 𝑋 ) ) → ( ( 𝑥 𝐺 𝑦 ) 𝐺 𝑧 ) = ( 𝑥 𝐺 ( 𝑦 𝐺 𝑧 ) ) )
4 isgrpda.4 ⊢ ( 𝜑 → 𝑈 ∈ 𝑋 )
5 isgrpda.5 ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑋 ) → ( 𝑈 𝐺 𝑥 ) = 𝑥 )
6 isgrpda.6 ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑋 ) → ∃ 𝑛 ∈ 𝑋 ( 𝑛 𝐺 𝑥 ) = 𝑈 )
7 3 ralrimivvva ⊢ ( 𝜑 → ∀ 𝑥 ∈ 𝑋 ∀ 𝑦 ∈ 𝑋 ∀ 𝑧 ∈ 𝑋 ( ( 𝑥 𝐺 𝑦 ) 𝐺 𝑧 ) = ( 𝑥 𝐺 ( 𝑦 𝐺 𝑧 ) ) )
8 oveq1 ⊢ ( 𝑦 = 𝑛 → ( 𝑦 𝐺 𝑥 ) = ( 𝑛 𝐺 𝑥 ) )
9 8 eqeq1d ⊢ ( 𝑦 = 𝑛 → ( ( 𝑦 𝐺 𝑥 ) = 𝑈 ↔ ( 𝑛 𝐺 𝑥 ) = 𝑈 ) )
10 9 cbvrexvw ⊢ ( ∃ 𝑦 ∈ 𝑋 ( 𝑦 𝐺 𝑥 ) = 𝑈 ↔ ∃ 𝑛 ∈ 𝑋 ( 𝑛 𝐺 𝑥 ) = 𝑈 )
11 6 10 sylibr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑋 ) → ∃ 𝑦 ∈ 𝑋 ( 𝑦 𝐺 𝑥 ) = 𝑈 )
12 5 11 jca ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑋 ) → ( ( 𝑈 𝐺 𝑥 ) = 𝑥 ∧ ∃ 𝑦 ∈ 𝑋 ( 𝑦 𝐺 𝑥 ) = 𝑈 ) )
13 12 ralrimiva ⊢ ( 𝜑 → ∀ 𝑥 ∈ 𝑋 ( ( 𝑈 𝐺 𝑥 ) = 𝑥 ∧ ∃ 𝑦 ∈ 𝑋 ( 𝑦 𝐺 𝑥 ) = 𝑈 ) )
14 oveq1 ⊢ ( 𝑢 = 𝑈 → ( 𝑢 𝐺 𝑥 ) = ( 𝑈 𝐺 𝑥 ) )
15 14 eqeq1d ⊢ ( 𝑢 = 𝑈 → ( ( 𝑢 𝐺 𝑥 ) = 𝑥 ↔ ( 𝑈 𝐺 𝑥 ) = 𝑥 ) )
16 eqeq2 ⊢ ( 𝑢 = 𝑈 → ( ( 𝑦 𝐺 𝑥 ) = 𝑢 ↔ ( 𝑦 𝐺 𝑥 ) = 𝑈 ) )
17 16 rexbidv ⊢ ( 𝑢 = 𝑈 → ( ∃ 𝑦 ∈ 𝑋 ( 𝑦 𝐺 𝑥 ) = 𝑢 ↔ ∃ 𝑦 ∈ 𝑋 ( 𝑦 𝐺 𝑥 ) = 𝑈 ) )
18 15 17 anbi12d ⊢ ( 𝑢 = 𝑈 → ( ( ( 𝑢 𝐺 𝑥 ) = 𝑥 ∧ ∃ 𝑦 ∈ 𝑋 ( 𝑦 𝐺 𝑥 ) = 𝑢 ) ↔ ( ( 𝑈 𝐺 𝑥 ) = 𝑥 ∧ ∃ 𝑦 ∈ 𝑋 ( 𝑦 𝐺 𝑥 ) = 𝑈 ) ) )
19 18 ralbidv ⊢ ( 𝑢 = 𝑈 → ( ∀ 𝑥 ∈ 𝑋 ( ( 𝑢 𝐺 𝑥 ) = 𝑥 ∧ ∃ 𝑦 ∈ 𝑋 ( 𝑦 𝐺 𝑥 ) = 𝑢 ) ↔ ∀ 𝑥 ∈ 𝑋 ( ( 𝑈 𝐺 𝑥 ) = 𝑥 ∧ ∃ 𝑦 ∈ 𝑋 ( 𝑦 𝐺 𝑥 ) = 𝑈 ) ) )
20 19 rspcev ⊢ ( ( 𝑈 ∈ 𝑋 ∧ ∀ 𝑥 ∈ 𝑋 ( ( 𝑈 𝐺 𝑥 ) = 𝑥 ∧ ∃ 𝑦 ∈ 𝑋 ( 𝑦 𝐺 𝑥 ) = 𝑈 ) ) → ∃ 𝑢 ∈ 𝑋 ∀ 𝑥 ∈ 𝑋 ( ( 𝑢 𝐺 𝑥 ) = 𝑥 ∧ ∃ 𝑦 ∈ 𝑋 ( 𝑦 𝐺 𝑥 ) = 𝑢 ) )
21 4 13 20 syl2anc ⊢ ( 𝜑 → ∃ 𝑢 ∈ 𝑋 ∀ 𝑥 ∈ 𝑋 ( ( 𝑢 𝐺 𝑥 ) = 𝑥 ∧ ∃ 𝑦 ∈ 𝑋 ( 𝑦 𝐺 𝑥 ) = 𝑢 ) )
22 4 adantr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑋 ) → 𝑈 ∈ 𝑋 )
23 simpr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑋 ) → 𝑥 ∈ 𝑋 )
24 5 eqcomd ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑋 ) → 𝑥 = ( 𝑈 𝐺 𝑥 ) )
25 rspceov ⊢ ( ( 𝑈 ∈ 𝑋 ∧ 𝑥 ∈ 𝑋 ∧ 𝑥 = ( 𝑈 𝐺 𝑥 ) ) → ∃ 𝑦 ∈ 𝑋 ∃ 𝑧 ∈ 𝑋 𝑥 = ( 𝑦 𝐺 𝑧 ) )
26 22 23 24 25 syl3anc ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑋 ) → ∃ 𝑦 ∈ 𝑋 ∃ 𝑧 ∈ 𝑋 𝑥 = ( 𝑦 𝐺 𝑧 ) )
27 26 ralrimiva ⊢ ( 𝜑 → ∀ 𝑥 ∈ 𝑋 ∃ 𝑦 ∈ 𝑋 ∃ 𝑧 ∈ 𝑋 𝑥 = ( 𝑦 𝐺 𝑧 ) )
28 foov ⊢ ( 𝐺 : ( 𝑋 × 𝑋 ) –onto→ 𝑋 ↔ ( 𝐺 : ( 𝑋 × 𝑋 ) ⟶ 𝑋 ∧ ∀ 𝑥 ∈ 𝑋 ∃ 𝑦 ∈ 𝑋 ∃ 𝑧 ∈ 𝑋 𝑥 = ( 𝑦 𝐺 𝑧 ) ) )
29 2 27 28 sylanbrc ⊢ ( 𝜑 → 𝐺 : ( 𝑋 × 𝑋 ) –onto→ 𝑋 )
30 forn ⊢ ( 𝐺 : ( 𝑋 × 𝑋 ) –onto→ 𝑋 → ran 𝐺 = 𝑋 )
31 29 30 syl ⊢ ( 𝜑 → ran 𝐺 = 𝑋 )
32 31 sqxpeqd ⊢ ( 𝜑 → ( ran 𝐺 × ran 𝐺 ) = ( 𝑋 × 𝑋 ) )
33 32 31 feq23d ⊢ ( 𝜑 → ( 𝐺 : ( ran 𝐺 × ran 𝐺 ) ⟶ ran 𝐺 ↔ 𝐺 : ( 𝑋 × 𝑋 ) ⟶ 𝑋 ) )
34 31 raleqdv ⊢ ( 𝜑 → ( ∀ 𝑧 ∈ ran 𝐺 ( ( 𝑥 𝐺 𝑦 ) 𝐺 𝑧 ) = ( 𝑥 𝐺 ( 𝑦 𝐺 𝑧 ) ) ↔ ∀ 𝑧 ∈ 𝑋 ( ( 𝑥 𝐺 𝑦 ) 𝐺 𝑧 ) = ( 𝑥 𝐺 ( 𝑦 𝐺 𝑧 ) ) ) )
35 31 34 raleqbidv ⊢ ( 𝜑 → ( ∀ 𝑦 ∈ ran 𝐺 ∀ 𝑧 ∈ ran 𝐺 ( ( 𝑥 𝐺 𝑦 ) 𝐺 𝑧 ) = ( 𝑥 𝐺 ( 𝑦 𝐺 𝑧 ) ) ↔ ∀ 𝑦 ∈ 𝑋 ∀ 𝑧 ∈ 𝑋 ( ( 𝑥 𝐺 𝑦 ) 𝐺 𝑧 ) = ( 𝑥 𝐺 ( 𝑦 𝐺 𝑧 ) ) ) )
36 31 35 raleqbidv ⊢ ( 𝜑 → ( ∀ 𝑥 ∈ ran 𝐺 ∀ 𝑦 ∈ ran 𝐺 ∀ 𝑧 ∈ ran 𝐺 ( ( 𝑥 𝐺 𝑦 ) 𝐺 𝑧 ) = ( 𝑥 𝐺 ( 𝑦 𝐺 𝑧 ) ) ↔ ∀ 𝑥 ∈ 𝑋 ∀ 𝑦 ∈ 𝑋 ∀ 𝑧 ∈ 𝑋 ( ( 𝑥 𝐺 𝑦 ) 𝐺 𝑧 ) = ( 𝑥 𝐺 ( 𝑦 𝐺 𝑧 ) ) ) )
37 31 rexeqdv ⊢ ( 𝜑 → ( ∃ 𝑦 ∈ ran 𝐺 ( 𝑦 𝐺 𝑥 ) = 𝑢 ↔ ∃ 𝑦 ∈ 𝑋 ( 𝑦 𝐺 𝑥 ) = 𝑢 ) )
38 37 anbi2d ⊢ ( 𝜑 → ( ( ( 𝑢 𝐺 𝑥 ) = 𝑥 ∧ ∃ 𝑦 ∈ ran 𝐺 ( 𝑦 𝐺 𝑥 ) = 𝑢 ) ↔ ( ( 𝑢 𝐺 𝑥 ) = 𝑥 ∧ ∃ 𝑦 ∈ 𝑋 ( 𝑦 𝐺 𝑥 ) = 𝑢 ) ) )
39 31 38 raleqbidv ⊢ ( 𝜑 → ( ∀ 𝑥 ∈ ran 𝐺 ( ( 𝑢 𝐺 𝑥 ) = 𝑥 ∧ ∃ 𝑦 ∈ ran 𝐺 ( 𝑦 𝐺 𝑥 ) = 𝑢 ) ↔ ∀ 𝑥 ∈ 𝑋 ( ( 𝑢 𝐺 𝑥 ) = 𝑥 ∧ ∃ 𝑦 ∈ 𝑋 ( 𝑦 𝐺 𝑥 ) = 𝑢 ) ) )
40 31 39 rexeqbidv ⊢ ( 𝜑 → ( ∃ 𝑢 ∈ ran 𝐺 ∀ 𝑥 ∈ ran 𝐺 ( ( 𝑢 𝐺 𝑥 ) = 𝑥 ∧ ∃ 𝑦 ∈ ran 𝐺 ( 𝑦 𝐺 𝑥 ) = 𝑢 ) ↔ ∃ 𝑢 ∈ 𝑋 ∀ 𝑥 ∈ 𝑋 ( ( 𝑢 𝐺 𝑥 ) = 𝑥 ∧ ∃ 𝑦 ∈ 𝑋 ( 𝑦 𝐺 𝑥 ) = 𝑢 ) ) )
41 33 36 40 3anbi123d ⊢ ( 𝜑 → ( ( 𝐺 : ( ran 𝐺 × ran 𝐺 ) ⟶ ran 𝐺 ∧ ∀ 𝑥 ∈ ran 𝐺 ∀ 𝑦 ∈ ran 𝐺 ∀ 𝑧 ∈ ran 𝐺 ( ( 𝑥 𝐺 𝑦 ) 𝐺 𝑧 ) = ( 𝑥 𝐺 ( 𝑦 𝐺 𝑧 ) ) ∧ ∃ 𝑢 ∈ ran 𝐺 ∀ 𝑥 ∈ ran 𝐺 ( ( 𝑢 𝐺 𝑥 ) = 𝑥 ∧ ∃ 𝑦 ∈ ran 𝐺 ( 𝑦 𝐺 𝑥 ) = 𝑢 ) ) ↔ ( 𝐺 : ( 𝑋 × 𝑋 ) ⟶ 𝑋 ∧ ∀ 𝑥 ∈ 𝑋 ∀ 𝑦 ∈ 𝑋 ∀ 𝑧 ∈ 𝑋 ( ( 𝑥 𝐺 𝑦 ) 𝐺 𝑧 ) = ( 𝑥 𝐺 ( 𝑦 𝐺 𝑧 ) ) ∧ ∃ 𝑢 ∈ 𝑋 ∀ 𝑥 ∈ 𝑋 ( ( 𝑢 𝐺 𝑥 ) = 𝑥 ∧ ∃ 𝑦 ∈ 𝑋 ( 𝑦 𝐺 𝑥 ) = 𝑢 ) ) ) )
42 2 7 21 41 mpbir3and ⊢ ( 𝜑 → ( 𝐺 : ( ran 𝐺 × ran 𝐺 ) ⟶ ran 𝐺 ∧ ∀ 𝑥 ∈ ran 𝐺 ∀ 𝑦 ∈ ran 𝐺 ∀ 𝑧 ∈ ran 𝐺 ( ( 𝑥 𝐺 𝑦 ) 𝐺 𝑧 ) = ( 𝑥 𝐺 ( 𝑦 𝐺 𝑧 ) ) ∧ ∃ 𝑢 ∈ ran 𝐺 ∀ 𝑥 ∈ ran 𝐺 ( ( 𝑢 𝐺 𝑥 ) = 𝑥 ∧ ∃ 𝑦 ∈ ran 𝐺 ( 𝑦 𝐺 𝑥 ) = 𝑢 ) ) )
43 1 1 xpexd ⊢ ( 𝜑 → ( 𝑋 × 𝑋 ) ∈ V )
44 fex ⊢ ( ( 𝐺 : ( 𝑋 × 𝑋 ) ⟶ 𝑋 ∧ ( 𝑋 × 𝑋 ) ∈ V ) → 𝐺 ∈ V )
45 2 43 44 syl2anc ⊢ ( 𝜑 → 𝐺 ∈ V )
46 eqid ⊢ ran 𝐺 = ran 𝐺
47 46 isgrpo ⊢ ( 𝐺 ∈ V → ( 𝐺 ∈ GrpOp ↔ ( 𝐺 : ( ran 𝐺 × ran 𝐺 ) ⟶ ran 𝐺 ∧ ∀ 𝑥 ∈ ran 𝐺 ∀ 𝑦 ∈ ran 𝐺 ∀ 𝑧 ∈ ran 𝐺 ( ( 𝑥 𝐺 𝑦 ) 𝐺 𝑧 ) = ( 𝑥 𝐺 ( 𝑦 𝐺 𝑧 ) ) ∧ ∃ 𝑢 ∈ ran 𝐺 ∀ 𝑥 ∈ ran 𝐺 ( ( 𝑢 𝐺 𝑥 ) = 𝑥 ∧ ∃ 𝑦 ∈ ran 𝐺 ( 𝑦 𝐺 𝑥 ) = 𝑢 ) ) ) )
48 45 47 syl ⊢ ( 𝜑 → ( 𝐺 ∈ GrpOp ↔ ( 𝐺 : ( ran 𝐺 × ran 𝐺 ) ⟶ ran 𝐺 ∧ ∀ 𝑥 ∈ ran 𝐺 ∀ 𝑦 ∈ ran 𝐺 ∀ 𝑧 ∈ ran 𝐺 ( ( 𝑥 𝐺 𝑦 ) 𝐺 𝑧 ) = ( 𝑥 𝐺 ( 𝑦 𝐺 𝑧 ) ) ∧ ∃ 𝑢 ∈ ran 𝐺 ∀ 𝑥 ∈ ran 𝐺 ( ( 𝑢 𝐺 𝑥 ) = 𝑥 ∧ ∃ 𝑦 ∈ ran 𝐺 ( 𝑦 𝐺 𝑥 ) = 𝑢 ) ) ) )
49 42 48 mpbird ⊢ ( 𝜑 → 𝐺 ∈ GrpOp )