Metamath Proof Explorer

Theorem grpoinv

Description: The properties of a group element's inverse. (Contributed by NM, 27-Oct-2006) (Revised by Mario Carneiro, 15-Dec-2013) (New usage is discouraged.)

Ref Expression
Hypotheses grpinv.1 ⊢ 𝑋 = ran 𝐺
grpinv.2 ⊢ 𝑈 = ( GId ‘ 𝐺 )
grpinv.3 ⊢ 𝑁 = ( inv ‘ 𝐺 )
Assertion grpoinv ( ( 𝐺 ∈ GrpOp ∧ 𝐴 ∈ 𝑋 ) → ( ( ( 𝑁 ‘ 𝐴 ) 𝐺 𝐴 ) = 𝑈 ∧ ( 𝐴 𝐺 ( 𝑁 ‘ 𝐴 ) ) = 𝑈 ) )

Proof

Step Hyp Ref Expression
1 grpinv.1 ⊢ 𝑋 = ran 𝐺
2 grpinv.2 ⊢ 𝑈 = ( GId ‘ 𝐺 )
3 grpinv.3 ⊢ 𝑁 = ( inv ‘ 𝐺 )
4 1 2 3 grpoinvval ⊢ ( ( 𝐺 ∈ GrpOp ∧ 𝐴 ∈ 𝑋 ) → ( 𝑁 ‘ 𝐴 ) = ( ℩ 𝑦 ∈ 𝑋 ( 𝑦 𝐺 𝐴 ) = 𝑈 ) )
5 1 2 grpoinveu ⊢ ( ( 𝐺 ∈ GrpOp ∧ 𝐴 ∈ 𝑋 ) → ∃! 𝑦 ∈ 𝑋 ( 𝑦 𝐺 𝐴 ) = 𝑈 )
6 riotacl2 ⊢ ( ∃! 𝑦 ∈ 𝑋 ( 𝑦 𝐺 𝐴 ) = 𝑈 → ( ℩ 𝑦 ∈ 𝑋 ( 𝑦 𝐺 𝐴 ) = 𝑈 ) ∈ { 𝑦 ∈ 𝑋 ∣ ( 𝑦 𝐺 𝐴 ) = 𝑈 } )
7 5 6 syl ⊢ ( ( 𝐺 ∈ GrpOp ∧ 𝐴 ∈ 𝑋 ) → ( ℩ 𝑦 ∈ 𝑋 ( 𝑦 𝐺 𝐴 ) = 𝑈 ) ∈ { 𝑦 ∈ 𝑋 ∣ ( 𝑦 𝐺 𝐴 ) = 𝑈 } )
8 4 7 eqeltrd ⊢ ( ( 𝐺 ∈ GrpOp ∧ 𝐴 ∈ 𝑋 ) → ( 𝑁 ‘ 𝐴 ) ∈ { 𝑦 ∈ 𝑋 ∣ ( 𝑦 𝐺 𝐴 ) = 𝑈 } )
9 simpl ⊢ ( ( ( 𝑦 𝐺 𝐴 ) = 𝑈 ∧ ( 𝐴 𝐺 𝑦 ) = 𝑈 ) → ( 𝑦 𝐺 𝐴 ) = 𝑈 )
10 9 rgenw ⊢ ∀ 𝑦 ∈ 𝑋 ( ( ( 𝑦 𝐺 𝐴 ) = 𝑈 ∧ ( 𝐴 𝐺 𝑦 ) = 𝑈 ) → ( 𝑦 𝐺 𝐴 ) = 𝑈 )
11 10 a1i ⊢ ( ( 𝐺 ∈ GrpOp ∧ 𝐴 ∈ 𝑋 ) → ∀ 𝑦 ∈ 𝑋 ( ( ( 𝑦 𝐺 𝐴 ) = 𝑈 ∧ ( 𝐴 𝐺 𝑦 ) = 𝑈 ) → ( 𝑦 𝐺 𝐴 ) = 𝑈 ) )
12 1 2 grpoidinv2 ⊢ ( ( 𝐺 ∈ GrpOp ∧ 𝐴 ∈ 𝑋 ) → ( ( ( 𝑈 𝐺 𝐴 ) = 𝐴 ∧ ( 𝐴 𝐺 𝑈 ) = 𝐴 ) ∧ ∃ 𝑦 ∈ 𝑋 ( ( 𝑦 𝐺 𝐴 ) = 𝑈 ∧ ( 𝐴 𝐺 𝑦 ) = 𝑈 ) ) )
13 12 simprd ⊢ ( ( 𝐺 ∈ GrpOp ∧ 𝐴 ∈ 𝑋 ) → ∃ 𝑦 ∈ 𝑋 ( ( 𝑦 𝐺 𝐴 ) = 𝑈 ∧ ( 𝐴 𝐺 𝑦 ) = 𝑈 ) )
14 11 13 5 3jca ⊢ ( ( 𝐺 ∈ GrpOp ∧ 𝐴 ∈ 𝑋 ) → ( ∀ 𝑦 ∈ 𝑋 ( ( ( 𝑦 𝐺 𝐴 ) = 𝑈 ∧ ( 𝐴 𝐺 𝑦 ) = 𝑈 ) → ( 𝑦 𝐺 𝐴 ) = 𝑈 ) ∧ ∃ 𝑦 ∈ 𝑋 ( ( 𝑦 𝐺 𝐴 ) = 𝑈 ∧ ( 𝐴 𝐺 𝑦 ) = 𝑈 ) ∧ ∃! 𝑦 ∈ 𝑋 ( 𝑦 𝐺 𝐴 ) = 𝑈 ) )
15 reupick2 ⊢ ( ( ( ∀ 𝑦 ∈ 𝑋 ( ( ( 𝑦 𝐺 𝐴 ) = 𝑈 ∧ ( 𝐴 𝐺 𝑦 ) = 𝑈 ) → ( 𝑦 𝐺 𝐴 ) = 𝑈 ) ∧ ∃ 𝑦 ∈ 𝑋 ( ( 𝑦 𝐺 𝐴 ) = 𝑈 ∧ ( 𝐴 𝐺 𝑦 ) = 𝑈 ) ∧ ∃! 𝑦 ∈ 𝑋 ( 𝑦 𝐺 𝐴 ) = 𝑈 ) ∧ 𝑦 ∈ 𝑋 ) → ( ( 𝑦 𝐺 𝐴 ) = 𝑈 ↔ ( ( 𝑦 𝐺 𝐴 ) = 𝑈 ∧ ( 𝐴 𝐺 𝑦 ) = 𝑈 ) ) )
16 14 15 sylan ⊢ ( ( ( 𝐺 ∈ GrpOp ∧ 𝐴 ∈ 𝑋 ) ∧ 𝑦 ∈ 𝑋 ) → ( ( 𝑦 𝐺 𝐴 ) = 𝑈 ↔ ( ( 𝑦 𝐺 𝐴 ) = 𝑈 ∧ ( 𝐴 𝐺 𝑦 ) = 𝑈 ) ) )
17 16 rabbidva ⊢ ( ( 𝐺 ∈ GrpOp ∧ 𝐴 ∈ 𝑋 ) → { 𝑦 ∈ 𝑋 ∣ ( 𝑦 𝐺 𝐴 ) = 𝑈 } = { 𝑦 ∈ 𝑋 ∣ ( ( 𝑦 𝐺 𝐴 ) = 𝑈 ∧ ( 𝐴 𝐺 𝑦 ) = 𝑈 ) } )
18 8 17 eleqtrd ⊢ ( ( 𝐺 ∈ GrpOp ∧ 𝐴 ∈ 𝑋 ) → ( 𝑁 ‘ 𝐴 ) ∈ { 𝑦 ∈ 𝑋 ∣ ( ( 𝑦 𝐺 𝐴 ) = 𝑈 ∧ ( 𝐴 𝐺 𝑦 ) = 𝑈 ) } )
19 oveq1 ⊢ ( 𝑦 = ( 𝑁 ‘ 𝐴 ) → ( 𝑦 𝐺 𝐴 ) = ( ( 𝑁 ‘ 𝐴 ) 𝐺 𝐴 ) )
20 19 eqeq1d ⊢ ( 𝑦 = ( 𝑁 ‘ 𝐴 ) → ( ( 𝑦 𝐺 𝐴 ) = 𝑈 ↔ ( ( 𝑁 ‘ 𝐴 ) 𝐺 𝐴 ) = 𝑈 ) )
21 oveq2 ⊢ ( 𝑦 = ( 𝑁 ‘ 𝐴 ) → ( 𝐴 𝐺 𝑦 ) = ( 𝐴 𝐺 ( 𝑁 ‘ 𝐴 ) ) )
22 21 eqeq1d ⊢ ( 𝑦 = ( 𝑁 ‘ 𝐴 ) → ( ( 𝐴 𝐺 𝑦 ) = 𝑈 ↔ ( 𝐴 𝐺 ( 𝑁 ‘ 𝐴 ) ) = 𝑈 ) )
23 20 22 anbi12d ⊢ ( 𝑦 = ( 𝑁 ‘ 𝐴 ) → ( ( ( 𝑦 𝐺 𝐴 ) = 𝑈 ∧ ( 𝐴 𝐺 𝑦 ) = 𝑈 ) ↔ ( ( ( 𝑁 ‘ 𝐴 ) 𝐺 𝐴 ) = 𝑈 ∧ ( 𝐴 𝐺 ( 𝑁 ‘ 𝐴 ) ) = 𝑈 ) ) )
24 23 elrab ⊢ ( ( 𝑁 ‘ 𝐴 ) ∈ { 𝑦 ∈ 𝑋 ∣ ( ( 𝑦 𝐺 𝐴 ) = 𝑈 ∧ ( 𝐴 𝐺 𝑦 ) = 𝑈 ) } ↔ ( ( 𝑁 ‘ 𝐴 ) ∈ 𝑋 ∧ ( ( ( 𝑁 ‘ 𝐴 ) 𝐺 𝐴 ) = 𝑈 ∧ ( 𝐴 𝐺 ( 𝑁 ‘ 𝐴 ) ) = 𝑈 ) ) )
25 18 24 sylib ⊢ ( ( 𝐺 ∈ GrpOp ∧ 𝐴 ∈ 𝑋 ) → ( ( 𝑁 ‘ 𝐴 ) ∈ 𝑋 ∧ ( ( ( 𝑁 ‘ 𝐴 ) 𝐺 𝐴 ) = 𝑈 ∧ ( 𝐴 𝐺 ( 𝑁 ‘ 𝐴 ) ) = 𝑈 ) ) )
26 25 simprd ⊢ ( ( 𝐺 ∈ GrpOp ∧ 𝐴 ∈ 𝑋 ) → ( ( ( 𝑁 ‘ 𝐴 ) 𝐺 𝐴 ) = 𝑈 ∧ ( 𝐴 𝐺 ( 𝑁 ‘ 𝐴 ) ) = 𝑈 ) )