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

Metamath Proof Explorer

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 ∧ ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ∧ 𝐶 ∈ 𝑋 ) ) ∧ 𝐶 ≠ 𝑍 ) → ( ( 𝐴 𝐻 𝐶 ) = ( 𝐵 𝐻 𝐶 ) → 𝐴 = 𝐵 ) )