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 ⟨ 𝐵 , 𝐶 ⟩ )