Theorem dmncan2

Description: Cancellation law for domains. (Contributed by Jeff Madsen, 6-Jan-2011)

	Ref	Expression
Hypotheses	dmncan.1	⊢ 𝐺 = ( 1st ‘ 𝑅 )
	dmncan.2	⊢ 𝐻 = ( 2nd ‘ 𝑅 )
	dmncan.3	⊢ 𝑋 = ran 𝐺
	dmncan.4	⊢ 𝑍 = ( GId ‘ 𝐺 )
Assertion	dmncan2	⊢ ( ( ( 𝑅 ∈ Dmn ∧ ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ∧ 𝐶 ∈ 𝑋 ) ) ∧ 𝐶 ≠ 𝑍 ) → ( ( 𝐴 𝐻 𝐶 ) = ( 𝐵 𝐻 𝐶 ) → 𝐴 = 𝐵 ) )

Proof

Step	Hyp	Ref	Expression
1		dmncan.1	⊢ 𝐺 = ( 1st ‘ 𝑅 )
2		dmncan.2	⊢ 𝐻 = ( 2nd ‘ 𝑅 )
3		dmncan.3	⊢ 𝑋 = ran 𝐺
4		dmncan.4	⊢ 𝑍 = ( GId ‘ 𝐺 )
5		dmncrng	⊢ ( 𝑅 ∈ Dmn → 𝑅 ∈ CRingOps )
6	1 2 3	crngocom	⊢ ( ( 𝑅 ∈ CRingOps ∧ 𝐴 ∈ 𝑋 ∧ 𝐶 ∈ 𝑋 ) → ( 𝐴 𝐻 𝐶 ) = ( 𝐶 𝐻 𝐴 ) )
7	6	3adant3r2	⊢ ( ( 𝑅 ∈ CRingOps ∧ ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ∧ 𝐶 ∈ 𝑋 ) ) → ( 𝐴 𝐻 𝐶 ) = ( 𝐶 𝐻 𝐴 ) )
8	1 2 3	crngocom	⊢ ( ( 𝑅 ∈ CRingOps ∧ 𝐵 ∈ 𝑋 ∧ 𝐶 ∈ 𝑋 ) → ( 𝐵 𝐻 𝐶 ) = ( 𝐶 𝐻 𝐵 ) )
9	8	3adant3r1	⊢ ( ( 𝑅 ∈ CRingOps ∧ ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ∧ 𝐶 ∈ 𝑋 ) ) → ( 𝐵 𝐻 𝐶 ) = ( 𝐶 𝐻 𝐵 ) )
10	7 9	eqeq12d	⊢ ( ( 𝑅 ∈ CRingOps ∧ ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ∧ 𝐶 ∈ 𝑋 ) ) → ( ( 𝐴 𝐻 𝐶 ) = ( 𝐵 𝐻 𝐶 ) ↔ ( 𝐶 𝐻 𝐴 ) = ( 𝐶 𝐻 𝐵 ) ) )
11	5 10	sylan	⊢ ( ( 𝑅 ∈ Dmn ∧ ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ∧ 𝐶 ∈ 𝑋 ) ) → ( ( 𝐴 𝐻 𝐶 ) = ( 𝐵 𝐻 𝐶 ) ↔ ( 𝐶 𝐻 𝐴 ) = ( 𝐶 𝐻 𝐵 ) ) )
12	11	adantr	⊢ ( ( ( 𝑅 ∈ Dmn ∧ ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ∧ 𝐶 ∈ 𝑋 ) ) ∧ 𝐶 ≠ 𝑍 ) → ( ( 𝐴 𝐻 𝐶 ) = ( 𝐵 𝐻 𝐶 ) ↔ ( 𝐶 𝐻 𝐴 ) = ( 𝐶 𝐻 𝐵 ) ) )
13		3anrot	⊢ ( ( 𝐶 ∈ 𝑋 ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) ↔ ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ∧ 𝐶 ∈ 𝑋 ) )
14	13	biimpri	⊢ ( ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ∧ 𝐶 ∈ 𝑋 ) → ( 𝐶 ∈ 𝑋 ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) )
15	1 2 3 4	dmncan1	⊢ ( ( ( 𝑅 ∈ Dmn ∧ ( 𝐶 ∈ 𝑋 ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) ) ∧ 𝐶 ≠ 𝑍 ) → ( ( 𝐶 𝐻 𝐴 ) = ( 𝐶 𝐻 𝐵 ) → 𝐴 = 𝐵 ) )
16	14 15	sylanl2	⊢ ( ( ( 𝑅 ∈ Dmn ∧ ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ∧ 𝐶 ∈ 𝑋 ) ) ∧ 𝐶 ≠ 𝑍 ) → ( ( 𝐶 𝐻 𝐴 ) = ( 𝐶 𝐻 𝐵 ) → 𝐴 = 𝐵 ) )
17	12 16	sylbid	⊢ ( ( ( 𝑅 ∈ Dmn ∧ ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ∧ 𝐶 ∈ 𝑋 ) ) ∧ 𝐶 ≠ 𝑍 ) → ( ( 𝐴 𝐻 𝐶 ) = ( 𝐵 𝐻 𝐶 ) → 𝐴 = 𝐵 ) )