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 ⊢ A ∈ 𝑵 ∧ B ∈ 𝑵 ∧ C ∈ 𝑵 → A ⋅ 𝑵 B A ⋅ 𝑵 C ~ 𝑸 B C

Proof

Step Hyp Ref Expression
1 oveq2 ⊢ b = B → A ⋅ 𝑵 b = A ⋅ 𝑵 B
2 1 opeq1d ⊢ b = B → A ⋅ 𝑵 b A ⋅ 𝑵 c = A ⋅ 𝑵 B A ⋅ 𝑵 c
3 opeq1 ⊢ b = B → b c = B c
4 2 3 breq12d ⊢ b = B → A ⋅ 𝑵 b A ⋅ 𝑵 c ~ 𝑸 b c ↔ A ⋅ 𝑵 B A ⋅ 𝑵 c ~ 𝑸 B c
5 4 imbi2d ⊢ b = B → A ∈ 𝑵 → A ⋅ 𝑵 b A ⋅ 𝑵 c ~ 𝑸 b c ↔ A ∈ 𝑵 → A ⋅ 𝑵 B A ⋅ 𝑵 c ~ 𝑸 B c
6 oveq2 ⊢ c = C → A ⋅ 𝑵 c = A ⋅ 𝑵 C
7 6 opeq2d ⊢ c = C → A ⋅ 𝑵 B A ⋅ 𝑵 c = A ⋅ 𝑵 B A ⋅ 𝑵 C
8 opeq2 ⊢ c = C → B c = B C
9 7 8 breq12d ⊢ c = C → A ⋅ 𝑵 B A ⋅ 𝑵 c ~ 𝑸 B c ↔ A ⋅ 𝑵 B A ⋅ 𝑵 C ~ 𝑸 B C
10 9 imbi2d ⊢ c = C → A ∈ 𝑵 → A ⋅ 𝑵 B A ⋅ 𝑵 c ~ 𝑸 B c ↔ A ∈ 𝑵 → A ⋅ 𝑵 B A ⋅ 𝑵 C ~ 𝑸 B C
11 mulcompi ⊢ b ⋅ 𝑵 c = c ⋅ 𝑵 b
12 11 oveq2i ⊢ A ⋅ 𝑵 b ⋅ 𝑵 c = A ⋅ 𝑵 c ⋅ 𝑵 b
13 mulasspi ⊢ A ⋅ 𝑵 b ⋅ 𝑵 c = A ⋅ 𝑵 b ⋅ 𝑵 c
14 mulasspi ⊢ A ⋅ 𝑵 c ⋅ 𝑵 b = A ⋅ 𝑵 c ⋅ 𝑵 b
15 12 13 14 3eqtr4i ⊢ A ⋅ 𝑵 b ⋅ 𝑵 c = A ⋅ 𝑵 c ⋅ 𝑵 b
16 mulclpi ⊢ A ∈ 𝑵 ∧ b ∈ 𝑵 → A ⋅ 𝑵 b ∈ 𝑵
17 16 3adant3 ⊢ A ∈ 𝑵 ∧ b ∈ 𝑵 ∧ c ∈ 𝑵 → A ⋅ 𝑵 b ∈ 𝑵
18 mulclpi ⊢ A ∈ 𝑵 ∧ c ∈ 𝑵 → A ⋅ 𝑵 c ∈ 𝑵
19 18 3adant2 ⊢ A ∈ 𝑵 ∧ b ∈ 𝑵 ∧ c ∈ 𝑵 → A ⋅ 𝑵 c ∈ 𝑵
20 3simpc ⊢ A ∈ 𝑵 ∧ b ∈ 𝑵 ∧ c ∈ 𝑵 → b ∈ 𝑵 ∧ c ∈ 𝑵
21 enqbreq ⊢ A ⋅ 𝑵 b ∈ 𝑵 ∧ A ⋅ 𝑵 c ∈ 𝑵 ∧ b ∈ 𝑵 ∧ c ∈ 𝑵 → A ⋅ 𝑵 b A ⋅ 𝑵 c ~ 𝑸 b c ↔ A ⋅ 𝑵 b ⋅ 𝑵 c = A ⋅ 𝑵 c ⋅ 𝑵 b
22 17 19 20 21 syl21anc ⊢ A ∈ 𝑵 ∧ b ∈ 𝑵 ∧ c ∈ 𝑵 → A ⋅ 𝑵 b A ⋅ 𝑵 c ~ 𝑸 b c ↔ A ⋅ 𝑵 b ⋅ 𝑵 c = A ⋅ 𝑵 c ⋅ 𝑵 b
23 15 22 mpbiri ⊢ A ∈ 𝑵 ∧ b ∈ 𝑵 ∧ c ∈ 𝑵 → A ⋅ 𝑵 b A ⋅ 𝑵 c ~ 𝑸 b c
24 23 3expb ⊢ A ∈ 𝑵 ∧ b ∈ 𝑵 ∧ c ∈ 𝑵 → A ⋅ 𝑵 b A ⋅ 𝑵 c ~ 𝑸 b c
25 24 expcom ⊢ b ∈ 𝑵 ∧ c ∈ 𝑵 → A ∈ 𝑵 → A ⋅ 𝑵 b A ⋅ 𝑵 c ~ 𝑸 b c
26 5 10 25 vtocl2ga ⊢ B ∈ 𝑵 ∧ C ∈ 𝑵 → A ∈ 𝑵 → A ⋅ 𝑵 B A ⋅ 𝑵 C ~ 𝑸 B C
27 26 impcom ⊢ A ∈ 𝑵 ∧ B ∈ 𝑵 ∧ C ∈ 𝑵 → A ⋅ 𝑵 B A ⋅ 𝑵 C ~ 𝑸 B C
28 27 3impb ⊢ A ∈ 𝑵 ∧ B ∈ 𝑵 ∧ C ∈ 𝑵 → A ⋅ 𝑵 B A ⋅ 𝑵 C ~ 𝑸 B C