Metamath Proof Explorer

Theorem grpoidinv2

Description: A group's properties using the explicit identity element. (Contributed by NM, 5-Feb-2010) (Revised by Mario Carneiro, 15-Dec-2013) (New usage is discouraged.)

Ref Expression
Hypotheses grpoidval.1 ⊢ 𝑋 = ran 𝐺
grpoidval.2 ⊢ 𝑈 = ( GId ‘ 𝐺 )
Assertion grpoidinv2 ( ( 𝐺 ∈ GrpOp ∧ 𝐴 ∈ 𝑋 ) → ( ( ( 𝑈 𝐺 𝐴 ) = 𝐴 ∧ ( 𝐴 𝐺 𝑈 ) = 𝐴 ) ∧ ∃ 𝑦 ∈ 𝑋 ( ( 𝑦 𝐺 𝐴 ) = 𝑈 ∧ ( 𝐴 𝐺 𝑦 ) = 𝑈 ) ) )

Proof

Step Hyp Ref Expression
1 grpoidval.1 ⊢ 𝑋 = ran 𝐺
2 grpoidval.2 ⊢ 𝑈 = ( GId ‘ 𝐺 )
3 1 2 grpoidval ⊢ ( 𝐺 ∈ GrpOp → 𝑈 = ( ℩ 𝑢 ∈ 𝑋 ∀ 𝑥 ∈ 𝑋 ( 𝑢 𝐺 𝑥 ) = 𝑥 ) )
4 1 grpoideu ⊢ ( 𝐺 ∈ GrpOp → ∃! 𝑢 ∈ 𝑋 ∀ 𝑥 ∈ 𝑋 ( 𝑢 𝐺 𝑥 ) = 𝑥 )
5 riotacl2 ⊢ ( ∃! 𝑢 ∈ 𝑋 ∀ 𝑥 ∈ 𝑋 ( 𝑢 𝐺 𝑥 ) = 𝑥 → ( ℩ 𝑢 ∈ 𝑋 ∀ 𝑥 ∈ 𝑋 ( 𝑢 𝐺 𝑥 ) = 𝑥 ) ∈ { 𝑢 ∈ 𝑋 ∣ ∀ 𝑥 ∈ 𝑋 ( 𝑢 𝐺 𝑥 ) = 𝑥 } )
6 4 5 syl ⊢ ( 𝐺 ∈ GrpOp → ( ℩ 𝑢 ∈ 𝑋 ∀ 𝑥 ∈ 𝑋 ( 𝑢 𝐺 𝑥 ) = 𝑥 ) ∈ { 𝑢 ∈ 𝑋 ∣ ∀ 𝑥 ∈ 𝑋 ( 𝑢 𝐺 𝑥 ) = 𝑥 } )
7 3 6 eqeltrd ⊢ ( 𝐺 ∈ GrpOp → 𝑈 ∈ { 𝑢 ∈ 𝑋 ∣ ∀ 𝑥 ∈ 𝑋 ( 𝑢 𝐺 𝑥 ) = 𝑥 } )
8 simpll ⊢ ( ( ( ( 𝑢 𝐺 𝑥 ) = 𝑥 ∧ ( 𝑥 𝐺 𝑢 ) = 𝑥 ) ∧ ∃ 𝑦 ∈ 𝑋 ( ( 𝑦 𝐺 𝑥 ) = 𝑢 ∧ ( 𝑥 𝐺 𝑦 ) = 𝑢 ) ) → ( 𝑢 𝐺 𝑥 ) = 𝑥 )
9 8 ralimi ⊢ ( ∀ 𝑥 ∈ 𝑋 ( ( ( 𝑢 𝐺 𝑥 ) = 𝑥 ∧ ( 𝑥 𝐺 𝑢 ) = 𝑥 ) ∧ ∃ 𝑦 ∈ 𝑋 ( ( 𝑦 𝐺 𝑥 ) = 𝑢 ∧ ( 𝑥 𝐺 𝑦 ) = 𝑢 ) ) → ∀ 𝑥 ∈ 𝑋 ( 𝑢 𝐺 𝑥 ) = 𝑥 )
10 9 rgenw ⊢ ∀ 𝑢 ∈ 𝑋 ( ∀ 𝑥 ∈ 𝑋 ( ( ( 𝑢 𝐺 𝑥 ) = 𝑥 ∧ ( 𝑥 𝐺 𝑢 ) = 𝑥 ) ∧ ∃ 𝑦 ∈ 𝑋 ( ( 𝑦 𝐺 𝑥 ) = 𝑢 ∧ ( 𝑥 𝐺 𝑦 ) = 𝑢 ) ) → ∀ 𝑥 ∈ 𝑋 ( 𝑢 𝐺 𝑥 ) = 𝑥 )
11 10 a1i ⊢ ( 𝐺 ∈ GrpOp → ∀ 𝑢 ∈ 𝑋 ( ∀ 𝑥 ∈ 𝑋 ( ( ( 𝑢 𝐺 𝑥 ) = 𝑥 ∧ ( 𝑥 𝐺 𝑢 ) = 𝑥 ) ∧ ∃ 𝑦 ∈ 𝑋 ( ( 𝑦 𝐺 𝑥 ) = 𝑢 ∧ ( 𝑥 𝐺 𝑦 ) = 𝑢 ) ) → ∀ 𝑥 ∈ 𝑋 ( 𝑢 𝐺 𝑥 ) = 𝑥 ) )
12 1 grpoidinv ⊢ ( 𝐺 ∈ GrpOp → ∃ 𝑢 ∈ 𝑋 ∀ 𝑥 ∈ 𝑋 ( ( ( 𝑢 𝐺 𝑥 ) = 𝑥 ∧ ( 𝑥 𝐺 𝑢 ) = 𝑥 ) ∧ ∃ 𝑦 ∈ 𝑋 ( ( 𝑦 𝐺 𝑥 ) = 𝑢 ∧ ( 𝑥 𝐺 𝑦 ) = 𝑢 ) ) )
13 11 12 4 3jca ⊢ ( 𝐺 ∈ GrpOp → ( ∀ 𝑢 ∈ 𝑋 ( ∀ 𝑥 ∈ 𝑋 ( ( ( 𝑢 𝐺 𝑥 ) = 𝑥 ∧ ( 𝑥 𝐺 𝑢 ) = 𝑥 ) ∧ ∃ 𝑦 ∈ 𝑋 ( ( 𝑦 𝐺 𝑥 ) = 𝑢 ∧ ( 𝑥 𝐺 𝑦 ) = 𝑢 ) ) → ∀ 𝑥 ∈ 𝑋 ( 𝑢 𝐺 𝑥 ) = 𝑥 ) ∧ ∃ 𝑢 ∈ 𝑋 ∀ 𝑥 ∈ 𝑋 ( ( ( 𝑢 𝐺 𝑥 ) = 𝑥 ∧ ( 𝑥 𝐺 𝑢 ) = 𝑥 ) ∧ ∃ 𝑦 ∈ 𝑋 ( ( 𝑦 𝐺 𝑥 ) = 𝑢 ∧ ( 𝑥 𝐺 𝑦 ) = 𝑢 ) ) ∧ ∃! 𝑢 ∈ 𝑋 ∀ 𝑥 ∈ 𝑋 ( 𝑢 𝐺 𝑥 ) = 𝑥 ) )
14 reupick2 ⊢ ( ( ( ∀ 𝑢 ∈ 𝑋 ( ∀ 𝑥 ∈ 𝑋 ( ( ( 𝑢 𝐺 𝑥 ) = 𝑥 ∧ ( 𝑥 𝐺 𝑢 ) = 𝑥 ) ∧ ∃ 𝑦 ∈ 𝑋 ( ( 𝑦 𝐺 𝑥 ) = 𝑢 ∧ ( 𝑥 𝐺 𝑦 ) = 𝑢 ) ) → ∀ 𝑥 ∈ 𝑋 ( 𝑢 𝐺 𝑥 ) = 𝑥 ) ∧ ∃ 𝑢 ∈ 𝑋 ∀ 𝑥 ∈ 𝑋 ( ( ( 𝑢 𝐺 𝑥 ) = 𝑥 ∧ ( 𝑥 𝐺 𝑢 ) = 𝑥 ) ∧ ∃ 𝑦 ∈ 𝑋 ( ( 𝑦 𝐺 𝑥 ) = 𝑢 ∧ ( 𝑥 𝐺 𝑦 ) = 𝑢 ) ) ∧ ∃! 𝑢 ∈ 𝑋 ∀ 𝑥 ∈ 𝑋 ( 𝑢 𝐺 𝑥 ) = 𝑥 ) ∧ 𝑢 ∈ 𝑋 ) → ( ∀ 𝑥 ∈ 𝑋 ( 𝑢 𝐺 𝑥 ) = 𝑥 ↔ ∀ 𝑥 ∈ 𝑋 ( ( ( 𝑢 𝐺 𝑥 ) = 𝑥 ∧ ( 𝑥 𝐺 𝑢 ) = 𝑥 ) ∧ ∃ 𝑦 ∈ 𝑋 ( ( 𝑦 𝐺 𝑥 ) = 𝑢 ∧ ( 𝑥 𝐺 𝑦 ) = 𝑢 ) ) ) )
15 13 14 sylan ⊢ ( ( 𝐺 ∈ GrpOp ∧ 𝑢 ∈ 𝑋 ) → ( ∀ 𝑥 ∈ 𝑋 ( 𝑢 𝐺 𝑥 ) = 𝑥 ↔ ∀ 𝑥 ∈ 𝑋 ( ( ( 𝑢 𝐺 𝑥 ) = 𝑥 ∧ ( 𝑥 𝐺 𝑢 ) = 𝑥 ) ∧ ∃ 𝑦 ∈ 𝑋 ( ( 𝑦 𝐺 𝑥 ) = 𝑢 ∧ ( 𝑥 𝐺 𝑦 ) = 𝑢 ) ) ) )
16 15 rabbidva ⊢ ( 𝐺 ∈ GrpOp → { 𝑢 ∈ 𝑋 ∣ ∀ 𝑥 ∈ 𝑋 ( 𝑢 𝐺 𝑥 ) = 𝑥 } = { 𝑢 ∈ 𝑋 ∣ ∀ 𝑥 ∈ 𝑋 ( ( ( 𝑢 𝐺 𝑥 ) = 𝑥 ∧ ( 𝑥 𝐺 𝑢 ) = 𝑥 ) ∧ ∃ 𝑦 ∈ 𝑋 ( ( 𝑦 𝐺 𝑥 ) = 𝑢 ∧ ( 𝑥 𝐺 𝑦 ) = 𝑢 ) ) } )
17 7 16 eleqtrd ⊢ ( 𝐺 ∈ GrpOp → 𝑈 ∈ { 𝑢 ∈ 𝑋 ∣ ∀ 𝑥 ∈ 𝑋 ( ( ( 𝑢 𝐺 𝑥 ) = 𝑥 ∧ ( 𝑥 𝐺 𝑢 ) = 𝑥 ) ∧ ∃ 𝑦 ∈ 𝑋 ( ( 𝑦 𝐺 𝑥 ) = 𝑢 ∧ ( 𝑥 𝐺 𝑦 ) = 𝑢 ) ) } )
18 oveq1 ⊢ ( 𝑢 = 𝑈 → ( 𝑢 𝐺 𝑥 ) = ( 𝑈 𝐺 𝑥 ) )
19 18 eqeq1d ⊢ ( 𝑢 = 𝑈 → ( ( 𝑢 𝐺 𝑥 ) = 𝑥 ↔ ( 𝑈 𝐺 𝑥 ) = 𝑥 ) )
20 oveq2 ⊢ ( 𝑢 = 𝑈 → ( 𝑥 𝐺 𝑢 ) = ( 𝑥 𝐺 𝑈 ) )
21 20 eqeq1d ⊢ ( 𝑢 = 𝑈 → ( ( 𝑥 𝐺 𝑢 ) = 𝑥 ↔ ( 𝑥 𝐺 𝑈 ) = 𝑥 ) )
22 19 21 anbi12d ⊢ ( 𝑢 = 𝑈 → ( ( ( 𝑢 𝐺 𝑥 ) = 𝑥 ∧ ( 𝑥 𝐺 𝑢 ) = 𝑥 ) ↔ ( ( 𝑈 𝐺 𝑥 ) = 𝑥 ∧ ( 𝑥 𝐺 𝑈 ) = 𝑥 ) ) )
23 eqeq2 ⊢ ( 𝑢 = 𝑈 → ( ( 𝑦 𝐺 𝑥 ) = 𝑢 ↔ ( 𝑦 𝐺 𝑥 ) = 𝑈 ) )
24 eqeq2 ⊢ ( 𝑢 = 𝑈 → ( ( 𝑥 𝐺 𝑦 ) = 𝑢 ↔ ( 𝑥 𝐺 𝑦 ) = 𝑈 ) )
25 23 24 anbi12d ⊢ ( 𝑢 = 𝑈 → ( ( ( 𝑦 𝐺 𝑥 ) = 𝑢 ∧ ( 𝑥 𝐺 𝑦 ) = 𝑢 ) ↔ ( ( 𝑦 𝐺 𝑥 ) = 𝑈 ∧ ( 𝑥 𝐺 𝑦 ) = 𝑈 ) ) )
26 25 rexbidv ⊢ ( 𝑢 = 𝑈 → ( ∃ 𝑦 ∈ 𝑋 ( ( 𝑦 𝐺 𝑥 ) = 𝑢 ∧ ( 𝑥 𝐺 𝑦 ) = 𝑢 ) ↔ ∃ 𝑦 ∈ 𝑋 ( ( 𝑦 𝐺 𝑥 ) = 𝑈 ∧ ( 𝑥 𝐺 𝑦 ) = 𝑈 ) ) )
27 22 26 anbi12d ⊢ ( 𝑢 = 𝑈 → ( ( ( ( 𝑢 𝐺 𝑥 ) = 𝑥 ∧ ( 𝑥 𝐺 𝑢 ) = 𝑥 ) ∧ ∃ 𝑦 ∈ 𝑋 ( ( 𝑦 𝐺 𝑥 ) = 𝑢 ∧ ( 𝑥 𝐺 𝑦 ) = 𝑢 ) ) ↔ ( ( ( 𝑈 𝐺 𝑥 ) = 𝑥 ∧ ( 𝑥 𝐺 𝑈 ) = 𝑥 ) ∧ ∃ 𝑦 ∈ 𝑋 ( ( 𝑦 𝐺 𝑥 ) = 𝑈 ∧ ( 𝑥 𝐺 𝑦 ) = 𝑈 ) ) ) )
28 27 ralbidv ⊢ ( 𝑢 = 𝑈 → ( ∀ 𝑥 ∈ 𝑋 ( ( ( 𝑢 𝐺 𝑥 ) = 𝑥 ∧ ( 𝑥 𝐺 𝑢 ) = 𝑥 ) ∧ ∃ 𝑦 ∈ 𝑋 ( ( 𝑦 𝐺 𝑥 ) = 𝑢 ∧ ( 𝑥 𝐺 𝑦 ) = 𝑢 ) ) ↔ ∀ 𝑥 ∈ 𝑋 ( ( ( 𝑈 𝐺 𝑥 ) = 𝑥 ∧ ( 𝑥 𝐺 𝑈 ) = 𝑥 ) ∧ ∃ 𝑦 ∈ 𝑋 ( ( 𝑦 𝐺 𝑥 ) = 𝑈 ∧ ( 𝑥 𝐺 𝑦 ) = 𝑈 ) ) ) )
29 28 elrab ⊢ ( 𝑈 ∈ { 𝑢 ∈ 𝑋 ∣ ∀ 𝑥 ∈ 𝑋 ( ( ( 𝑢 𝐺 𝑥 ) = 𝑥 ∧ ( 𝑥 𝐺 𝑢 ) = 𝑥 ) ∧ ∃ 𝑦 ∈ 𝑋 ( ( 𝑦 𝐺 𝑥 ) = 𝑢 ∧ ( 𝑥 𝐺 𝑦 ) = 𝑢 ) ) } ↔ ( 𝑈 ∈ 𝑋 ∧ ∀ 𝑥 ∈ 𝑋 ( ( ( 𝑈 𝐺 𝑥 ) = 𝑥 ∧ ( 𝑥 𝐺 𝑈 ) = 𝑥 ) ∧ ∃ 𝑦 ∈ 𝑋 ( ( 𝑦 𝐺 𝑥 ) = 𝑈 ∧ ( 𝑥 𝐺 𝑦 ) = 𝑈 ) ) ) )
30 17 29 sylib ⊢ ( 𝐺 ∈ GrpOp → ( 𝑈 ∈ 𝑋 ∧ ∀ 𝑥 ∈ 𝑋 ( ( ( 𝑈 𝐺 𝑥 ) = 𝑥 ∧ ( 𝑥 𝐺 𝑈 ) = 𝑥 ) ∧ ∃ 𝑦 ∈ 𝑋 ( ( 𝑦 𝐺 𝑥 ) = 𝑈 ∧ ( 𝑥 𝐺 𝑦 ) = 𝑈 ) ) ) )
31 30 simprd ⊢ ( 𝐺 ∈ GrpOp → ∀ 𝑥 ∈ 𝑋 ( ( ( 𝑈 𝐺 𝑥 ) = 𝑥 ∧ ( 𝑥 𝐺 𝑈 ) = 𝑥 ) ∧ ∃ 𝑦 ∈ 𝑋 ( ( 𝑦 𝐺 𝑥 ) = 𝑈 ∧ ( 𝑥 𝐺 𝑦 ) = 𝑈 ) ) )
32 oveq2 ⊢ ( 𝑥 = 𝐴 → ( 𝑈 𝐺 𝑥 ) = ( 𝑈 𝐺 𝐴 ) )
33 id ⊢ ( 𝑥 = 𝐴 → 𝑥 = 𝐴 )
34 32 33 eqeq12d ⊢ ( 𝑥 = 𝐴 → ( ( 𝑈 𝐺 𝑥 ) = 𝑥 ↔ ( 𝑈 𝐺 𝐴 ) = 𝐴 ) )
35 oveq1 ⊢ ( 𝑥 = 𝐴 → ( 𝑥 𝐺 𝑈 ) = ( 𝐴 𝐺 𝑈 ) )
36 35 33 eqeq12d ⊢ ( 𝑥 = 𝐴 → ( ( 𝑥 𝐺 𝑈 ) = 𝑥 ↔ ( 𝐴 𝐺 𝑈 ) = 𝐴 ) )
37 34 36 anbi12d ⊢ ( 𝑥 = 𝐴 → ( ( ( 𝑈 𝐺 𝑥 ) = 𝑥 ∧ ( 𝑥 𝐺 𝑈 ) = 𝑥 ) ↔ ( ( 𝑈 𝐺 𝐴 ) = 𝐴 ∧ ( 𝐴 𝐺 𝑈 ) = 𝐴 ) ) )
38 oveq2 ⊢ ( 𝑥 = 𝐴 → ( 𝑦 𝐺 𝑥 ) = ( 𝑦 𝐺 𝐴 ) )
39 38 eqeq1d ⊢ ( 𝑥 = 𝐴 → ( ( 𝑦 𝐺 𝑥 ) = 𝑈 ↔ ( 𝑦 𝐺 𝐴 ) = 𝑈 ) )
40 oveq1 ⊢ ( 𝑥 = 𝐴 → ( 𝑥 𝐺 𝑦 ) = ( 𝐴 𝐺 𝑦 ) )
41 40 eqeq1d ⊢ ( 𝑥 = 𝐴 → ( ( 𝑥 𝐺 𝑦 ) = 𝑈 ↔ ( 𝐴 𝐺 𝑦 ) = 𝑈 ) )
42 39 41 anbi12d ⊢ ( 𝑥 = 𝐴 → ( ( ( 𝑦 𝐺 𝑥 ) = 𝑈 ∧ ( 𝑥 𝐺 𝑦 ) = 𝑈 ) ↔ ( ( 𝑦 𝐺 𝐴 ) = 𝑈 ∧ ( 𝐴 𝐺 𝑦 ) = 𝑈 ) ) )
43 42 rexbidv ⊢ ( 𝑥 = 𝐴 → ( ∃ 𝑦 ∈ 𝑋 ( ( 𝑦 𝐺 𝑥 ) = 𝑈 ∧ ( 𝑥 𝐺 𝑦 ) = 𝑈 ) ↔ ∃ 𝑦 ∈ 𝑋 ( ( 𝑦 𝐺 𝐴 ) = 𝑈 ∧ ( 𝐴 𝐺 𝑦 ) = 𝑈 ) ) )
44 37 43 anbi12d ⊢ ( 𝑥 = 𝐴 → ( ( ( ( 𝑈 𝐺 𝑥 ) = 𝑥 ∧ ( 𝑥 𝐺 𝑈 ) = 𝑥 ) ∧ ∃ 𝑦 ∈ 𝑋 ( ( 𝑦 𝐺 𝑥 ) = 𝑈 ∧ ( 𝑥 𝐺 𝑦 ) = 𝑈 ) ) ↔ ( ( ( 𝑈 𝐺 𝐴 ) = 𝐴 ∧ ( 𝐴 𝐺 𝑈 ) = 𝐴 ) ∧ ∃ 𝑦 ∈ 𝑋 ( ( 𝑦 𝐺 𝐴 ) = 𝑈 ∧ ( 𝐴 𝐺 𝑦 ) = 𝑈 ) ) ) )
45 44 rspccva ⊢ ( ( ∀ 𝑥 ∈ 𝑋 ( ( ( 𝑈 𝐺 𝑥 ) = 𝑥 ∧ ( 𝑥 𝐺 𝑈 ) = 𝑥 ) ∧ ∃ 𝑦 ∈ 𝑋 ( ( 𝑦 𝐺 𝑥 ) = 𝑈 ∧ ( 𝑥 𝐺 𝑦 ) = 𝑈 ) ) ∧ 𝐴 ∈ 𝑋 ) → ( ( ( 𝑈 𝐺 𝐴 ) = 𝐴 ∧ ( 𝐴 𝐺 𝑈 ) = 𝐴 ) ∧ ∃ 𝑦 ∈ 𝑋 ( ( 𝑦 𝐺 𝐴 ) = 𝑈 ∧ ( 𝐴 𝐺 𝑦 ) = 𝑈 ) ) )
46 31 45 sylan ⊢ ( ( 𝐺 ∈ GrpOp ∧ 𝐴 ∈ 𝑋 ) → ( ( ( 𝑈 𝐺 𝐴 ) = 𝐴 ∧ ( 𝐴 𝐺 𝑈 ) = 𝐴 ) ∧ ∃ 𝑦 ∈ 𝑋 ( ( 𝑦 𝐺 𝐴 ) = 𝑈 ∧ ( 𝐴 𝐺 𝑦 ) = 𝑈 ) ) )