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⋅𝑵BA⋅𝑵C~𝑸BC

Proof

Step Hyp Ref Expression
1 oveq2 ⊢b=B→A⋅𝑵b=A⋅𝑵B
2 1 opeq1d ⊢b=B→A⋅𝑵bA⋅𝑵c=A⋅𝑵BA⋅𝑵c
3 opeq1 ⊢b=B→bc=Bc
4 2 3 breq12d ⊢b=B→A⋅𝑵bA⋅𝑵c~𝑸bc↔A⋅𝑵BA⋅𝑵c~𝑸Bc
5 4 imbi2d ⊢b=B→A∈𝑵→A⋅𝑵bA⋅𝑵c~𝑸bc↔A∈𝑵→A⋅𝑵BA⋅𝑵c~𝑸Bc
6 oveq2 ⊢c=C→A⋅𝑵c=A⋅𝑵C
7 6 opeq2d ⊢c=C→A⋅𝑵BA⋅𝑵c=A⋅𝑵BA⋅𝑵C
8 opeq2 ⊢c=C→Bc=BC
9 7 8 breq12d ⊢c=C→A⋅𝑵BA⋅𝑵c~𝑸Bc↔A⋅𝑵BA⋅𝑵C~𝑸BC
10 9 imbi2d ⊢c=C→A∈𝑵→A⋅𝑵BA⋅𝑵c~𝑸Bc↔A∈𝑵→A⋅𝑵BA⋅𝑵C~𝑸BC
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⋅𝑵bA⋅𝑵c~𝑸bc↔A⋅𝑵b⋅𝑵c=A⋅𝑵c⋅𝑵b
22 17 19 20 21 syl21anc ⊢A∈𝑵∧b∈𝑵∧c∈𝑵→A⋅𝑵bA⋅𝑵c~𝑸bc↔A⋅𝑵b⋅𝑵c=A⋅𝑵c⋅𝑵b
23 15 22 mpbiri ⊢A∈𝑵∧b∈𝑵∧c∈𝑵→A⋅𝑵bA⋅𝑵c~𝑸bc
24 23 3expb ⊢A∈𝑵∧b∈𝑵∧c∈𝑵→A⋅𝑵bA⋅𝑵c~𝑸bc
25 24 expcom ⊢b∈𝑵∧c∈𝑵→A∈𝑵→A⋅𝑵bA⋅𝑵c~𝑸bc
26 5 10 25 vtocl2ga ⊢B∈𝑵∧C∈𝑵→A∈𝑵→A⋅𝑵BA⋅𝑵C~𝑸BC
27 26 impcom ⊢A∈𝑵∧B∈𝑵∧C∈𝑵→A⋅𝑵BA⋅𝑵C~𝑸BC
28 27 3impb ⊢A∈𝑵∧B∈𝑵∧C∈𝑵→A⋅𝑵BA⋅𝑵C~𝑸BC