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

Metamath Proof Explorer

Theorem mulcanenq

Description: Lemma for distributive law: cancellation of common factor. (Contributed by NM, 2-Sep-1995) (Revised by Mario Carneiro, 8-May-2013) (New usage is discouraged.)

Ref Expression
Assertion mulcanenq ( ( 𝐴 ∈ N ∧ 𝐵 ∈ N ∧ 𝐶 ∈ N ) → ⟨ ( 𝐴 ·N 𝐵 ) , ( 𝐴 ·N 𝐶 ) ⟩ ~Q ⟨ 𝐵 , 𝐶 ⟩ )

Proof

Step Hyp Ref Expression
1 oveq2 ⊢ ( 𝑏 = 𝐵 → ( 𝐴 ·N 𝑏 ) = ( 𝐴 ·N 𝐵 ) )
2 1 opeq1d ⊢ ( 𝑏 = 𝐵 → ⟨ ( 𝐴 ·N 𝑏 ) , ( 𝐴 ·N 𝑐 ) ⟩ = ⟨ ( 𝐴 ·N 𝐵 ) , ( 𝐴 ·N 𝑐 ) ⟩ )
3 opeq1 ⊢ ( 𝑏 = 𝐵 → ⟨ 𝑏 , 𝑐 ⟩ = ⟨ 𝐵 , 𝑐 ⟩ )
4 2 3 breq12d ⊢ ( 𝑏 = 𝐵 → ( ⟨ ( 𝐴 ·N 𝑏 ) , ( 𝐴 ·N 𝑐 ) ⟩ ~Q ⟨ 𝑏 , 𝑐 ⟩ ↔ ⟨ ( 𝐴 ·N 𝐵 ) , ( 𝐴 ·N 𝑐 ) ⟩ ~Q ⟨ 𝐵 , 𝑐 ⟩ ) )
5 4 imbi2d ⊢ ( 𝑏 = 𝐵 → ( ( 𝐴 ∈ N → ⟨ ( 𝐴 ·N 𝑏 ) , ( 𝐴 ·N 𝑐 ) ⟩ ~Q ⟨ 𝑏 , 𝑐 ⟩ ) ↔ ( 𝐴 ∈ N → ⟨ ( 𝐴 ·N 𝐵 ) , ( 𝐴 ·N 𝑐 ) ⟩ ~Q ⟨ 𝐵 , 𝑐 ⟩ ) ) )
6 oveq2 ⊢ ( 𝑐 = 𝐶 → ( 𝐴 ·N 𝑐 ) = ( 𝐴 ·N 𝐶 ) )
7 6 opeq2d ⊢ ( 𝑐 = 𝐶 → ⟨ ( 𝐴 ·N 𝐵 ) , ( 𝐴 ·N 𝑐 ) ⟩ = ⟨ ( 𝐴 ·N 𝐵 ) , ( 𝐴 ·N 𝐶 ) ⟩ )
8 opeq2 ⊢ ( 𝑐 = 𝐶 → ⟨ 𝐵 , 𝑐 ⟩ = ⟨ 𝐵 , 𝐶 ⟩ )
9 7 8 breq12d ⊢ ( 𝑐 = 𝐶 → ( ⟨ ( 𝐴 ·N 𝐵 ) , ( 𝐴 ·N 𝑐 ) ⟩ ~Q ⟨ 𝐵 , 𝑐 ⟩ ↔ ⟨ ( 𝐴 ·N 𝐵 ) , ( 𝐴 ·N 𝐶 ) ⟩ ~Q ⟨ 𝐵 , 𝐶 ⟩ ) )
10 9 imbi2d ⊢ ( 𝑐 = 𝐶 → ( ( 𝐴 ∈ N → ⟨ ( 𝐴 ·N 𝐵 ) , ( 𝐴 ·N 𝑐 ) ⟩ ~Q ⟨ 𝐵 , 𝑐 ⟩ ) ↔ ( 𝐴 ∈ N → ⟨ ( 𝐴 ·N 𝐵 ) , ( 𝐴 ·N 𝐶 ) ⟩ ~Q ⟨ 𝐵 , 𝐶 ⟩ ) ) )
11 mulcompi ⊢ ( 𝑏 ·N 𝑐 ) = ( 𝑐 ·N 𝑏 )
12 11 oveq2i ⊢ ( 𝐴 ·N ( 𝑏 ·N 𝑐 ) ) = ( 𝐴 ·N ( 𝑐 ·N 𝑏 ) )
13 mulasspi ⊢ ( ( 𝐴 ·N 𝑏 ) ·N 𝑐 ) = ( 𝐴 ·N ( 𝑏 ·N 𝑐 ) )
14 mulasspi ⊢ ( ( 𝐴 ·N 𝑐 ) ·N 𝑏 ) = ( 𝐴 ·N ( 𝑐 ·N 𝑏 ) )
15 12 13 14 3eqtr4i ⊢ ( ( 𝐴 ·N 𝑏 ) ·N 𝑐 ) = ( ( 𝐴 ·N 𝑐 ) ·N 𝑏 )
16 mulclpi ⊢ ( ( 𝐴 ∈ N ∧ 𝑏 ∈ N ) → ( 𝐴 ·N 𝑏 ) ∈ N )
17 16 3adant3 ⊢ ( ( 𝐴 ∈ N ∧ 𝑏 ∈ N ∧ 𝑐 ∈ N ) → ( 𝐴 ·N 𝑏 ) ∈ N )
18 mulclpi ⊢ ( ( 𝐴 ∈ N ∧ 𝑐 ∈ N ) → ( 𝐴 ·N 𝑐 ) ∈ N )
19 18 3adant2 ⊢ ( ( 𝐴 ∈ N ∧ 𝑏 ∈ N ∧ 𝑐 ∈ N ) → ( 𝐴 ·N 𝑐 ) ∈ N )
20 3simpc ⊢ ( ( 𝐴 ∈ N ∧ 𝑏 ∈ N ∧ 𝑐 ∈ N ) → ( 𝑏 ∈ N ∧ 𝑐 ∈ N ) )
21 enqbreq ⊢ ( ( ( ( 𝐴 ·N 𝑏 ) ∈ N ∧ ( 𝐴 ·N 𝑐 ) ∈ N ) ∧ ( 𝑏 ∈ N ∧ 𝑐 ∈ N ) ) → ( ⟨ ( 𝐴 ·N 𝑏 ) , ( 𝐴 ·N 𝑐 ) ⟩ ~Q ⟨ 𝑏 , 𝑐 ⟩ ↔ ( ( 𝐴 ·N 𝑏 ) ·N 𝑐 ) = ( ( 𝐴 ·N 𝑐 ) ·N 𝑏 ) ) )
22 17 19 20 21 syl21anc ⊢ ( ( 𝐴 ∈ N ∧ 𝑏 ∈ N ∧ 𝑐 ∈ N ) → ( ⟨ ( 𝐴 ·N 𝑏 ) , ( 𝐴 ·N 𝑐 ) ⟩ ~Q ⟨ 𝑏 , 𝑐 ⟩ ↔ ( ( 𝐴 ·N 𝑏 ) ·N 𝑐 ) = ( ( 𝐴 ·N 𝑐 ) ·N 𝑏 ) ) )
23 15 22 mpbiri ⊢ ( ( 𝐴 ∈ N ∧ 𝑏 ∈ N ∧ 𝑐 ∈ N ) → ⟨ ( 𝐴 ·N 𝑏 ) , ( 𝐴 ·N 𝑐 ) ⟩ ~Q ⟨ 𝑏 , 𝑐 ⟩ )
24 23 3expb ⊢ ( ( 𝐴 ∈ N ∧ ( 𝑏 ∈ N ∧ 𝑐 ∈ N ) ) → ⟨ ( 𝐴 ·N 𝑏 ) , ( 𝐴 ·N 𝑐 ) ⟩ ~Q ⟨ 𝑏 , 𝑐 ⟩ )
25 24 expcom ⊢ ( ( 𝑏 ∈ N ∧ 𝑐 ∈ N ) → ( 𝐴 ∈ N → ⟨ ( 𝐴 ·N 𝑏 ) , ( 𝐴 ·N 𝑐 ) ⟩ ~Q ⟨ 𝑏 , 𝑐 ⟩ ) )
26 5 10 25 vtocl2ga ⊢ ( ( 𝐵 ∈ N ∧ 𝐶 ∈ N ) → ( 𝐴 ∈ N → ⟨ ( 𝐴 ·N 𝐵 ) , ( 𝐴 ·N 𝐶 ) ⟩ ~Q ⟨ 𝐵 , 𝐶 ⟩ ) )
27 26 impcom ⊢ ( ( 𝐴 ∈ N ∧ ( 𝐵 ∈ N ∧ 𝐶 ∈ N ) ) → ⟨ ( 𝐴 ·N 𝐵 ) , ( 𝐴 ·N 𝐶 ) ⟩ ~Q ⟨ 𝐵 , 𝐶 ⟩ )
28 27 3impb ⊢ ( ( 𝐴 ∈ N ∧ 𝐵 ∈ N ∧ 𝐶 ∈ N ) → ⟨ ( 𝐴 ·N 𝐵 ) , ( 𝐴 ·N 𝐶 ) ⟩ ~Q ⟨ 𝐵 , 𝐶 ⟩ )