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 ⊢ φ → X ∈ V
isgrpda.2 ⊢ φ → G : X × X ⟶ X
isgrpda.3 ⊢ φ ∧ x ∈ X ∧ y ∈ X ∧ z ∈ X → x G y G z = x G y G z
isgrpda.4 ⊢ φ → U ∈ X
isgrpda.5 ⊢ φ ∧ x ∈ X → U G x = x
isgrpda.6 ⊢ φ ∧ x ∈ X → ∃ n ∈ X n G x = U
Assertion isgrpda ⊢ φ → G ∈ GrpOp

Proof

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