Metamath Proof Explorer

Theorem rngoneglmul

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 rngoneglmul ⊢ R ∈ RingOps ∧ A ∈ X ∧ B ∈ X → N ⁡ A H B = N ⁡ A H 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 ∧ N ⁡ GId ⁡ H ∈ X ∧ A ∈ X ∧ B ∈ X → N ⁡ GId ⁡ H H A H B = N ⁡ GId ⁡ H H A H B
12 11 3exp2 ⊢ R ∈ RingOps → N ⁡ GId ⁡ H ∈ X → A ∈ X → B ∈ X → N ⁡ GId ⁡ H H A H B = N ⁡ GId ⁡ H H A H B
13 10 12 mpd ⊢ R ∈ RingOps → A ∈ X → B ∈ X → N ⁡ GId ⁡ H H A H B = N ⁡ GId ⁡ H H A H B
14 13 3imp ⊢ R ∈ RingOps ∧ A ∈ X ∧ B ∈ X → N ⁡ GId ⁡ H H A H B = N ⁡ GId ⁡ H H A H B
15 1 2 3 4 7 rngonegmn1l ⊢ R ∈ RingOps ∧ A ∈ X → N ⁡ A = N ⁡ GId ⁡ H H A
16 15 3adant3 ⊢ R ∈ RingOps ∧ A ∈ X ∧ B ∈ X → N ⁡ A = N ⁡ GId ⁡ H H A
17 16 oveq1d ⊢ R ∈ RingOps ∧ A ∈ X ∧ B ∈ X → N ⁡ A H B = N ⁡ GId ⁡ H H A H B
18 1 2 3 rngocl ⊢ R ∈ RingOps ∧ A ∈ X ∧ B ∈ X → A H B ∈ X
19 18 3expb ⊢ R ∈ RingOps ∧ A ∈ X ∧ B ∈ X → A H B ∈ X
20 1 2 3 4 7 rngonegmn1l ⊢ R ∈ RingOps ∧ A H B ∈ X → N ⁡ A H B = N ⁡ GId ⁡ H H A H B
21 19 20 syldan ⊢ R ∈ RingOps ∧ A ∈ X ∧ B ∈ X → N ⁡ A H B = N ⁡ GId ⁡ H H A H B
22 21 3impb ⊢ R ∈ RingOps ∧ A ∈ X ∧ B ∈ X → N ⁡ A H B = N ⁡ GId ⁡ H H A H B
23 14 17 22 3eqtr4rd ⊢ R ∈ RingOps ∧ A ∈ X ∧ B ∈ X → N ⁡ A H B = N ⁡ A H B