Description: Division of a group member by itself. (Contributed by NM, 15-Feb-2008) (New usage is discouraged.)
| Ref | Expression | ||
|---|---|---|---|
| Hypotheses | grpdivf.1 | ⊢ 𝑋 = ran 𝐺 | |
| grpdivf.3 | ⊢ 𝐷 = ( /𝑔 ‘ 𝐺 ) | ||
| grpdivid.3 | ⊢ 𝑈 = ( GId ‘ 𝐺 ) | ||
| Assertion | grpodivid | ⊢ ( ( 𝐺 ∈ GrpOp ∧ 𝐴 ∈ 𝑋 ) → ( 𝐴 𝐷 𝐴 ) = 𝑈 ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | grpdivf.1 | ⊢ 𝑋 = ran 𝐺 | |
| 2 | grpdivf.3 | ⊢ 𝐷 = ( /𝑔 ‘ 𝐺 ) | |
| 3 | grpdivid.3 | ⊢ 𝑈 = ( GId ‘ 𝐺 ) | |
| 4 | eqid | ⊢ ( inv ‘ 𝐺 ) = ( inv ‘ 𝐺 ) | |
| 5 | 1 4 2 | grpodivval | ⊢ ( ( 𝐺 ∈ GrpOp ∧ 𝐴 ∈ 𝑋 ∧ 𝐴 ∈ 𝑋 ) → ( 𝐴 𝐷 𝐴 ) = ( 𝐴 𝐺 ( ( inv ‘ 𝐺 ) ‘ 𝐴 ) ) ) |
| 6 | 5 | 3anidm23 | ⊢ ( ( 𝐺 ∈ GrpOp ∧ 𝐴 ∈ 𝑋 ) → ( 𝐴 𝐷 𝐴 ) = ( 𝐴 𝐺 ( ( inv ‘ 𝐺 ) ‘ 𝐴 ) ) ) |
| 7 | 1 3 4 | grporinv | ⊢ ( ( 𝐺 ∈ GrpOp ∧ 𝐴 ∈ 𝑋 ) → ( 𝐴 𝐺 ( ( inv ‘ 𝐺 ) ‘ 𝐴 ) ) = 𝑈 ) |
| 8 | 6 7 | eqtrd | ⊢ ( ( 𝐺 ∈ GrpOp ∧ 𝐴 ∈ 𝑋 ) → ( 𝐴 𝐷 𝐴 ) = 𝑈 ) |