Metamath Proof Explorer

Theorem rngonegrmul

Description: Negation of a product in a ring. (Contributed by Jeff Madsen, 19-Jun-2010)

Ref Expression
Hypotheses ringnegmul.1 ⊢ G = 1 st ⁡ R
ringnegmul.2 ⊢ H = 2 nd ⁡ R
ringnegmul.3 ⊢ X = ran ⁡ G
ringnegmul.4 ⊢ N = inv ⁡ G
Assertion rngonegrmul ⊢ R ∈ RingOps ∧ A ∈ X ∧ B ∈ X → N ⁡ A H B = A H N ⁡ B

Proof

Step Hyp Ref Expression
1 ringnegmul.1 ⊢ G = 1 st ⁡ R
2 ringnegmul.2 ⊢ H = 2 nd ⁡ R
3 ringnegmul.3 ⊢ X = ran ⁡ G
4 ringnegmul.4 ⊢ N = inv ⁡ G
5 1 rneqi ⊢ ran ⁡ G = ran ⁡ 1 st ⁡ R
6 3 5 eqtri ⊢ X = ran ⁡ 1 st ⁡ R
7 eqid ⊢ GId ⁡ H = GId ⁡ H
8 6 2 7 rngo1cl ⊢ R ∈ RingOps → GId ⁡ H ∈ X
9 1 3 4 rngonegcl ⊢ R ∈ RingOps ∧ GId ⁡ H ∈ X → N ⁡ GId ⁡ H ∈ X
10 8 9 mpdan ⊢ R ∈ RingOps → N ⁡ GId ⁡ H ∈ X
11 1 2 3 rngoass ⊢ R ∈ RingOps ∧ A ∈ X ∧ B ∈ X ∧ N ⁡ GId ⁡ H ∈ X → A H B H N ⁡ GId ⁡ H = A H B H N ⁡ GId ⁡ H
12 11 3exp2 ⊢ R ∈ RingOps → A ∈ X → B ∈ X → N ⁡ GId ⁡ H ∈ X → A H B H N ⁡ GId ⁡ H = A H B H N ⁡ GId ⁡ H
13 12 com24 ⊢ R ∈ RingOps → N ⁡ GId ⁡ H ∈ X → B ∈ X → A ∈ X → A H B H N ⁡ GId ⁡ H = A H B H N ⁡ GId ⁡ H
14 13 com34 ⊢ R ∈ RingOps → N ⁡ GId ⁡ H ∈ X → A ∈ X → B ∈ X → A H B H N ⁡ GId ⁡ H = A H B H N ⁡ GId ⁡ H
15 10 14 mpd ⊢ R ∈ RingOps → A ∈ X → B ∈ X → A H B H N ⁡ GId ⁡ H = A H B H N ⁡ GId ⁡ H
16 15 3imp ⊢ R ∈ RingOps ∧ A ∈ X ∧ B ∈ X → A H B H N ⁡ GId ⁡ H = A H B H N ⁡ GId ⁡ H
17 1 2 3 rngocl ⊢ R ∈ RingOps ∧ A ∈ X ∧ B ∈ X → A H B ∈ X
18 17 3expb ⊢ R ∈ RingOps ∧ A ∈ X ∧ B ∈ X → A H B ∈ X
19 1 2 3 4 7 rngonegmn1r ⊢ R ∈ RingOps ∧ A H B ∈ X → N ⁡ A H B = A H B H N ⁡ GId ⁡ H
20 18 19 syldan ⊢ R ∈ RingOps ∧ A ∈ X ∧ B ∈ X → N ⁡ A H B = A H B H N ⁡ GId ⁡ H
21 20 3impb ⊢ R ∈ RingOps ∧ A ∈ X ∧ B ∈ X → N ⁡ A H B = A H B H N ⁡ GId ⁡ H
22 1 2 3 4 7 rngonegmn1r ⊢ R ∈ RingOps ∧ B ∈ X → N ⁡ B = B H N ⁡ GId ⁡ H
23 22 3adant2 ⊢ R ∈ RingOps ∧ A ∈ X ∧ B ∈ X → N ⁡ B = B H N ⁡ GId ⁡ H
24 23 oveq2d ⊢ R ∈ RingOps ∧ A ∈ X ∧ B ∈ X → A H N ⁡ B = A H B H N ⁡ GId ⁡ H
25 16 21 24 3eqtr4d ⊢ R ∈ RingOps ∧ A ∈ X ∧ B ∈ X → N ⁡ A H B = A H N ⁡ B