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 2 43 fexd ( 𝜑𝐺 ∈ V )
45 eqid ran 𝐺 = ran 𝐺
46 45 isgrpo ( 𝐺 ∈ V → ( 𝐺 ∈ GrpOp ↔ ( 𝐺 : ( ran 𝐺 × ran 𝐺 ) ⟶ ran 𝐺 ∧ ∀ 𝑥 ∈ ran 𝐺𝑦 ∈ ran 𝐺𝑧 ∈ ran 𝐺 ( ( 𝑥 𝐺 𝑦 ) 𝐺 𝑧 ) = ( 𝑥 𝐺 ( 𝑦 𝐺 𝑧 ) ) ∧ ∃ 𝑢 ∈ ran 𝐺𝑥 ∈ ran 𝐺 ( ( 𝑢 𝐺 𝑥 ) = 𝑥 ∧ ∃ 𝑦 ∈ ran 𝐺 ( 𝑦 𝐺 𝑥 ) = 𝑢 ) ) ) )
47 44 46 syl ( 𝜑 → ( 𝐺 ∈ GrpOp ↔ ( 𝐺 : ( ran 𝐺 × ran 𝐺 ) ⟶ ran 𝐺 ∧ ∀ 𝑥 ∈ ran 𝐺𝑦 ∈ ran 𝐺𝑧 ∈ ran 𝐺 ( ( 𝑥 𝐺 𝑦 ) 𝐺 𝑧 ) = ( 𝑥 𝐺 ( 𝑦 𝐺 𝑧 ) ) ∧ ∃ 𝑢 ∈ ran 𝐺𝑥 ∈ ran 𝐺 ( ( 𝑢 𝐺 𝑥 ) = 𝑥 ∧ ∃ 𝑦 ∈ ran 𝐺 ( 𝑦 𝐺 𝑥 ) = 𝑢 ) ) ) )
48 42 47 mpbird ( 𝜑𝐺 ∈ GrpOp )