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 ⊢ 𝐺 = ( 1st ‘ 𝑅 )
ringnegmul.2 ⊢ 𝐻 = ( 2nd ‘ 𝑅 )
ringnegmul.3 ⊢ 𝑋 = ran 𝐺
ringnegmul.4 ⊢ 𝑁 = ( inv ‘ 𝐺 )
Assertion rngonegrmul ( ( 𝑅 ∈ RingOps ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) → ( 𝑁 ‘ ( 𝐴 𝐻 𝐵 ) ) = ( 𝐴 𝐻 ( 𝑁 ‘ 𝐵 ) ) )

Proof

Step Hyp Ref Expression
1 ringnegmul.1 ⊢ 𝐺 = ( 1st ‘ 𝑅 )
2 ringnegmul.2 ⊢ 𝐻 = ( 2nd ‘ 𝑅 )
3 ringnegmul.3 ⊢ 𝑋 = ran 𝐺
4 ringnegmul.4 ⊢ 𝑁 = ( inv ‘ 𝐺 )
5 1 rneqi ⊢ ran 𝐺 = ran ( 1st ‘ 𝑅 )
6 3 5 eqtri ⊢ 𝑋 = ran ( 1st ‘ 𝑅 )
7 eqid ⊢ ( GId ‘ 𝐻 ) = ( GId ‘ 𝐻 )
8 6 2 7 rngo1cl ⊢ ( 𝑅 ∈ RingOps → ( GId ‘ 𝐻 ) ∈ 𝑋 )
9 1 3 4 rngonegcl ⊢ ( ( 𝑅 ∈ RingOps ∧ ( GId ‘ 𝐻 ) ∈ 𝑋 ) → ( 𝑁 ‘ ( GId ‘ 𝐻 ) ) ∈ 𝑋 )
10 8 9 mpdan ⊢ ( 𝑅 ∈ RingOps → ( 𝑁 ‘ ( GId ‘ 𝐻 ) ) ∈ 𝑋 )
11 1 2 3 rngoass ⊢ ( ( 𝑅 ∈ RingOps ∧ ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ∧ ( 𝑁 ‘ ( GId ‘ 𝐻 ) ) ∈ 𝑋 ) ) → ( ( 𝐴 𝐻 𝐵 ) 𝐻 ( 𝑁 ‘ ( GId ‘ 𝐻 ) ) ) = ( 𝐴 𝐻 ( 𝐵 𝐻 ( 𝑁 ‘ ( GId ‘ 𝐻 ) ) ) ) )
12 11 3exp2 ⊢ ( 𝑅 ∈ RingOps → ( 𝐴 ∈ 𝑋 → ( 𝐵 ∈ 𝑋 → ( ( 𝑁 ‘ ( GId ‘ 𝐻 ) ) ∈ 𝑋 → ( ( 𝐴 𝐻 𝐵 ) 𝐻 ( 𝑁 ‘ ( GId ‘ 𝐻 ) ) ) = ( 𝐴 𝐻 ( 𝐵 𝐻 ( 𝑁 ‘ ( GId ‘ 𝐻 ) ) ) ) ) ) ) )
13 12 com24 ⊢ ( 𝑅 ∈ RingOps → ( ( 𝑁 ‘ ( GId ‘ 𝐻 ) ) ∈ 𝑋 → ( 𝐵 ∈ 𝑋 → ( 𝐴 ∈ 𝑋 → ( ( 𝐴 𝐻 𝐵 ) 𝐻 ( 𝑁 ‘ ( GId ‘ 𝐻 ) ) ) = ( 𝐴 𝐻 ( 𝐵 𝐻 ( 𝑁 ‘ ( GId ‘ 𝐻 ) ) ) ) ) ) ) )
14 13 com34 ⊢ ( 𝑅 ∈ RingOps → ( ( 𝑁 ‘ ( GId ‘ 𝐻 ) ) ∈ 𝑋 → ( 𝐴 ∈ 𝑋 → ( 𝐵 ∈ 𝑋 → ( ( 𝐴 𝐻 𝐵 ) 𝐻 ( 𝑁 ‘ ( GId ‘ 𝐻 ) ) ) = ( 𝐴 𝐻 ( 𝐵 𝐻 ( 𝑁 ‘ ( GId ‘ 𝐻 ) ) ) ) ) ) ) )
15 10 14 mpd ⊢ ( 𝑅 ∈ RingOps → ( 𝐴 ∈ 𝑋 → ( 𝐵 ∈ 𝑋 → ( ( 𝐴 𝐻 𝐵 ) 𝐻 ( 𝑁 ‘ ( GId ‘ 𝐻 ) ) ) = ( 𝐴 𝐻 ( 𝐵 𝐻 ( 𝑁 ‘ ( GId ‘ 𝐻 ) ) ) ) ) ) )
16 15 3imp ⊢ ( ( 𝑅 ∈ RingOps ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) → ( ( 𝐴 𝐻 𝐵 ) 𝐻 ( 𝑁 ‘ ( GId ‘ 𝐻 ) ) ) = ( 𝐴 𝐻 ( 𝐵 𝐻 ( 𝑁 ‘ ( GId ‘ 𝐻 ) ) ) ) )
17 1 2 3 rngocl ⊢ ( ( 𝑅 ∈ RingOps ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) → ( 𝐴 𝐻 𝐵 ) ∈ 𝑋 )
18 17 3expb ⊢ ( ( 𝑅 ∈ RingOps ∧ ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) ) → ( 𝐴 𝐻 𝐵 ) ∈ 𝑋 )
19 1 2 3 4 7 rngonegmn1r ⊢ ( ( 𝑅 ∈ RingOps ∧ ( 𝐴 𝐻 𝐵 ) ∈ 𝑋 ) → ( 𝑁 ‘ ( 𝐴 𝐻 𝐵 ) ) = ( ( 𝐴 𝐻 𝐵 ) 𝐻 ( 𝑁 ‘ ( GId ‘ 𝐻 ) ) ) )
20 18 19 syldan ⊢ ( ( 𝑅 ∈ RingOps ∧ ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) ) → ( 𝑁 ‘ ( 𝐴 𝐻 𝐵 ) ) = ( ( 𝐴 𝐻 𝐵 ) 𝐻 ( 𝑁 ‘ ( GId ‘ 𝐻 ) ) ) )
21 20 3impb ⊢ ( ( 𝑅 ∈ RingOps ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) → ( 𝑁 ‘ ( 𝐴 𝐻 𝐵 ) ) = ( ( 𝐴 𝐻 𝐵 ) 𝐻 ( 𝑁 ‘ ( GId ‘ 𝐻 ) ) ) )
22 1 2 3 4 7 rngonegmn1r ⊢ ( ( 𝑅 ∈ RingOps ∧ 𝐵 ∈ 𝑋 ) → ( 𝑁 ‘ 𝐵 ) = ( 𝐵 𝐻 ( 𝑁 ‘ ( GId ‘ 𝐻 ) ) ) )
23 22 3adant2 ⊢ ( ( 𝑅 ∈ RingOps ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) → ( 𝑁 ‘ 𝐵 ) = ( 𝐵 𝐻 ( 𝑁 ‘ ( GId ‘ 𝐻 ) ) ) )
24 23 oveq2d ⊢ ( ( 𝑅 ∈ RingOps ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) → ( 𝐴 𝐻 ( 𝑁 ‘ 𝐵 ) ) = ( 𝐴 𝐻 ( 𝐵 𝐻 ( 𝑁 ‘ ( GId ‘ 𝐻 ) ) ) ) )
25 16 21 24 3eqtr4d ⊢ ( ( 𝑅 ∈ RingOps ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) → ( 𝑁 ‘ ( 𝐴 𝐻 𝐵 ) ) = ( 𝐴 𝐻 ( 𝑁 ‘ 𝐵 ) ) )