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 ‘ 𝑅 ) ) ∧ ( 𝐴 ∈ 𝐼 ∧ 𝐵 ∈ 𝐼 ) ) → ( 𝐴 𝐷 𝐵 ) ∈ 𝐼 )