This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem idlsubcl

Description: An ideal is closed under subtraction. (Contributed by Jeff Madsen, 19-Jun-2010)

Ref Expression
Hypotheses idlsubcl.1 ⊢ 𝐺 = ( 1st ‘ 𝑅 )
idlsubcl.2 ⊢ 𝐷 = ( /𝑔 ‘ 𝐺 )
Assertion idlsubcl ( ( ( 𝑅 ∈ RingOps ∧ 𝐼 ∈ ( Idl ‘ 𝑅 ) ) ∧ ( 𝐴 ∈ 𝐼 ∧ 𝐵 ∈ 𝐼 ) ) → ( 𝐴 𝐷 𝐵 ) ∈ 𝐼 )

Proof

Step Hyp Ref Expression
1 idlsubcl.1 ⊢ 𝐺 = ( 1st ‘ 𝑅 )
2 idlsubcl.2 ⊢ 𝐷 = ( /𝑔 ‘ 𝐺 )
3 eqid ⊢ ran 𝐺 = ran 𝐺
4 1 3 idlcl ⊢ ( ( ( 𝑅 ∈ RingOps ∧ 𝐼 ∈ ( Idl ‘ 𝑅 ) ) ∧ 𝐴 ∈ 𝐼 ) → 𝐴 ∈ ran 𝐺 )
5 1 3 idlcl ⊢ ( ( ( 𝑅 ∈ RingOps ∧ 𝐼 ∈ ( Idl ‘ 𝑅 ) ) ∧ 𝐵 ∈ 𝐼 ) → 𝐵 ∈ ran 𝐺 )
6 4 5 anim12dan ⊢ ( ( ( 𝑅 ∈ RingOps ∧ 𝐼 ∈ ( Idl ‘ 𝑅 ) ) ∧ ( 𝐴 ∈ 𝐼 ∧ 𝐵 ∈ 𝐼 ) ) → ( 𝐴 ∈ ran 𝐺 ∧ 𝐵 ∈ ran 𝐺 ) )
7 eqid ⊢ ( inv ‘ 𝐺 ) = ( inv ‘ 𝐺 )
8 1 3 7 2 rngosub ⊢ ( ( 𝑅 ∈ RingOps ∧ 𝐴 ∈ ran 𝐺 ∧ 𝐵 ∈ ran 𝐺 ) → ( 𝐴 𝐷 𝐵 ) = ( 𝐴 𝐺 ( ( inv ‘ 𝐺 ) ‘ 𝐵 ) ) )
9 8 3expb ⊢ ( ( 𝑅 ∈ RingOps ∧ ( 𝐴 ∈ ran 𝐺 ∧ 𝐵 ∈ ran 𝐺 ) ) → ( 𝐴 𝐷 𝐵 ) = ( 𝐴 𝐺 ( ( inv ‘ 𝐺 ) ‘ 𝐵 ) ) )
10 9 adantlr ⊢ ( ( ( 𝑅 ∈ RingOps ∧ 𝐼 ∈ ( Idl ‘ 𝑅 ) ) ∧ ( 𝐴 ∈ ran 𝐺 ∧ 𝐵 ∈ ran 𝐺 ) ) → ( 𝐴 𝐷 𝐵 ) = ( 𝐴 𝐺 ( ( inv ‘ 𝐺 ) ‘ 𝐵 ) ) )
11 6 10 syldan ⊢ ( ( ( 𝑅 ∈ RingOps ∧ 𝐼 ∈ ( Idl ‘ 𝑅 ) ) ∧ ( 𝐴 ∈ 𝐼 ∧ 𝐵 ∈ 𝐼 ) ) → ( 𝐴 𝐷 𝐵 ) = ( 𝐴 𝐺 ( ( inv ‘ 𝐺 ) ‘ 𝐵 ) ) )
12 simprl ⊢ ( ( ( 𝑅 ∈ RingOps ∧ 𝐼 ∈ ( Idl ‘ 𝑅 ) ) ∧ ( 𝐴 ∈ 𝐼 ∧ 𝐵 ∈ 𝐼 ) ) → 𝐴 ∈ 𝐼 )
13 1 7 idlnegcl ⊢ ( ( ( 𝑅 ∈ RingOps ∧ 𝐼 ∈ ( Idl ‘ 𝑅 ) ) ∧ 𝐵 ∈ 𝐼 ) → ( ( inv ‘ 𝐺 ) ‘ 𝐵 ) ∈ 𝐼 )
14 13 adantrl ⊢ ( ( ( 𝑅 ∈ RingOps ∧ 𝐼 ∈ ( Idl ‘ 𝑅 ) ) ∧ ( 𝐴 ∈ 𝐼 ∧ 𝐵 ∈ 𝐼 ) ) → ( ( inv ‘ 𝐺 ) ‘ 𝐵 ) ∈ 𝐼 )
15 12 14 jca ⊢ ( ( ( 𝑅 ∈ RingOps ∧ 𝐼 ∈ ( Idl ‘ 𝑅 ) ) ∧ ( 𝐴 ∈ 𝐼 ∧ 𝐵 ∈ 𝐼 ) ) → ( 𝐴 ∈ 𝐼 ∧ ( ( inv ‘ 𝐺 ) ‘ 𝐵 ) ∈ 𝐼 ) )
16 1 idladdcl ⊢ ( ( ( 𝑅 ∈ RingOps ∧ 𝐼 ∈ ( Idl ‘ 𝑅 ) ) ∧ ( 𝐴 ∈ 𝐼 ∧ ( ( inv ‘ 𝐺 ) ‘ 𝐵 ) ∈ 𝐼 ) ) → ( 𝐴 𝐺 ( ( inv ‘ 𝐺 ) ‘ 𝐵 ) ) ∈ 𝐼 )
17 15 16 syldan ⊢ ( ( ( 𝑅 ∈ RingOps ∧ 𝐼 ∈ ( Idl ‘ 𝑅 ) ) ∧ ( 𝐴 ∈ 𝐼 ∧ 𝐵 ∈ 𝐼 ) ) → ( 𝐴 𝐺 ( ( inv ‘ 𝐺 ) ‘ 𝐵 ) ) ∈ 𝐼 )
18 11 17 eqeltrd ⊢ ( ( ( 𝑅 ∈ RingOps ∧ 𝐼 ∈ ( Idl ‘ 𝑅 ) ) ∧ ( 𝐴 ∈ 𝐼 ∧ 𝐵 ∈ 𝐼 ) ) → ( 𝐴 𝐷 𝐵 ) ∈ 𝐼 )