Theorem mulcmpblnr 11090

Description: Lemma showing compatibility of multiplication. (Contributed by NM, 5-Sep-1995.) (New usage is discouraged.)

Assertion

Ref	Expression
mulcmpblnr	⊢ ((((𝐴 ∈ P ∧ 𝐵 ∈ P) ∧ (𝐶 ∈ P ∧ 𝐷 ∈ P)) ∧ ((𝐹 ∈ P ∧ 𝐺 ∈ P) ∧ (𝑅 ∈ P ∧ 𝑆 ∈ P))) → (((𝐴 +P 𝐷) = (𝐵 +P 𝐶) ∧ (𝐹 +P 𝑆) = (𝐺 +P 𝑅)) → ⟨((𝐴 ·P 𝐹) +P (𝐵 ·P 𝐺)), ((𝐴 ·P 𝐺) +P (𝐵 ·P 𝐹))⟩ ~R ⟨((𝐶 ·P 𝑅) +P (𝐷 ·P 𝑆)), ((𝐶 ·P 𝑆) +P (𝐷 ·P 𝑅))⟩))

Proof of Theorem mulcmpblnr

Step	Hyp	Ref	Expression
1		mulcmpblnrlem 11089	. . 3 ⊢ (((𝐴 +P 𝐷) = (𝐵 +P 𝐶) ∧ (𝐹 +P 𝑆) = (𝐺 +P 𝑅)) → ((𝐷 ·P 𝐹) +P (((𝐴 ·P 𝐹) +P (𝐵 ·P 𝐺)) +P ((𝐶 ·P 𝑆) +P (𝐷 ·P 𝑅)))) = ((𝐷 ·P 𝐹) +P (((𝐴 ·P 𝐺) +P (𝐵 ·P 𝐹)) +P ((𝐶 ·P 𝑅) +P (𝐷 ·P 𝑆)))))
2		mulclpr 11039	. . . . . 6 ⊢ ((𝐷 ∈ P ∧ 𝐹 ∈ P) → (𝐷 ·P 𝐹) ∈ P)
3	2	ad2ant2lr 748	. . . . 5 ⊢ (((𝐶 ∈ P ∧ 𝐷 ∈ P) ∧ (𝐹 ∈ P ∧ 𝐺 ∈ P)) → (𝐷 ·P 𝐹) ∈ P)
4	3	ad2ant2lr 748	. . . 4 ⊢ ((((𝐴 ∈ P ∧ 𝐵 ∈ P) ∧ (𝐶 ∈ P ∧ 𝐷 ∈ P)) ∧ ((𝐹 ∈ P ∧ 𝐺 ∈ P) ∧ (𝑅 ∈ P ∧ 𝑆 ∈ P))) → (𝐷 ·P 𝐹) ∈ P)
5		simplll 774	. . . . . . 7 ⊢ ((((𝐴 ∈ P ∧ 𝐵 ∈ P) ∧ (𝐶 ∈ P ∧ 𝐷 ∈ P)) ∧ ((𝐹 ∈ P ∧ 𝐺 ∈ P) ∧ (𝑅 ∈ P ∧ 𝑆 ∈ P))) → 𝐴 ∈ P)
6		simprll 778	. . . . . . 7 ⊢ ((((𝐴 ∈ P ∧ 𝐵 ∈ P) ∧ (𝐶 ∈ P ∧ 𝐷 ∈ P)) ∧ ((𝐹 ∈ P ∧ 𝐺 ∈ P) ∧ (𝑅 ∈ P ∧ 𝑆 ∈ P))) → 𝐹 ∈ P)
7		mulclpr 11039	. . . . . . 7 ⊢ ((𝐴 ∈ P ∧ 𝐹 ∈ P) → (𝐴 ·P 𝐹) ∈ P)
8	5, 6, 7	syl2anc 584	. . . . . 6 ⊢ ((((𝐴 ∈ P ∧ 𝐵 ∈ P) ∧ (𝐶 ∈ P ∧ 𝐷 ∈ P)) ∧ ((𝐹 ∈ P ∧ 𝐺 ∈ P) ∧ (𝑅 ∈ P ∧ 𝑆 ∈ P))) → (𝐴 ·P 𝐹) ∈ P)
9		simpllr 775	. . . . . . 7 ⊢ ((((𝐴 ∈ P ∧ 𝐵 ∈ P) ∧ (𝐶 ∈ P ∧ 𝐷 ∈ P)) ∧ ((𝐹 ∈ P ∧ 𝐺 ∈ P) ∧ (𝑅 ∈ P ∧ 𝑆 ∈ P))) → 𝐵 ∈ P)
10		simprlr 779	. . . . . . 7 ⊢ ((((𝐴 ∈ P ∧ 𝐵 ∈ P) ∧ (𝐶 ∈ P ∧ 𝐷 ∈ P)) ∧ ((𝐹 ∈ P ∧ 𝐺 ∈ P) ∧ (𝑅 ∈ P ∧ 𝑆 ∈ P))) → 𝐺 ∈ P)
11		mulclpr 11039	. . . . . . 7 ⊢ ((𝐵 ∈ P ∧ 𝐺 ∈ P) → (𝐵 ·P 𝐺) ∈ P)
12	9, 10, 11	syl2anc 584	. . . . . 6 ⊢ ((((𝐴 ∈ P ∧ 𝐵 ∈ P) ∧ (𝐶 ∈ P ∧ 𝐷 ∈ P)) ∧ ((𝐹 ∈ P ∧ 𝐺 ∈ P) ∧ (𝑅 ∈ P ∧ 𝑆 ∈ P))) → (𝐵 ·P 𝐺) ∈ P)
13		addclpr 11037	. . . . . 6 ⊢ (((𝐴 ·P 𝐹) ∈ P ∧ (𝐵 ·P 𝐺) ∈ P) → ((𝐴 ·P 𝐹) +P (𝐵 ·P 𝐺)) ∈ P)
14	8, 12, 13	syl2anc 584	. . . . 5 ⊢ ((((𝐴 ∈ P ∧ 𝐵 ∈ P) ∧ (𝐶 ∈ P ∧ 𝐷 ∈ P)) ∧ ((𝐹 ∈ P ∧ 𝐺 ∈ P) ∧ (𝑅 ∈ P ∧ 𝑆 ∈ P))) → ((𝐴 ·P 𝐹) +P (𝐵 ·P 𝐺)) ∈ P)
15		simplrl 776	. . . . . . 7 ⊢ ((((𝐴 ∈ P ∧ 𝐵 ∈ P) ∧ (𝐶 ∈ P ∧ 𝐷 ∈ P)) ∧ ((𝐹 ∈ P ∧ 𝐺 ∈ P) ∧ (𝑅 ∈ P ∧ 𝑆 ∈ P))) → 𝐶 ∈ P)
16		simprrr 781	. . . . . . 7 ⊢ ((((𝐴 ∈ P ∧ 𝐵 ∈ P) ∧ (𝐶 ∈ P ∧ 𝐷 ∈ P)) ∧ ((𝐹 ∈ P ∧ 𝐺 ∈ P) ∧ (𝑅 ∈ P ∧ 𝑆 ∈ P))) → 𝑆 ∈ P)
17		mulclpr 11039	. . . . . . 7 ⊢ ((𝐶 ∈ P ∧ 𝑆 ∈ P) → (𝐶 ·P 𝑆) ∈ P)
18	15, 16, 17	syl2anc 584	. . . . . 6 ⊢ ((((𝐴 ∈ P ∧ 𝐵 ∈ P) ∧ (𝐶 ∈ P ∧ 𝐷 ∈ P)) ∧ ((𝐹 ∈ P ∧ 𝐺 ∈ P) ∧ (𝑅 ∈ P ∧ 𝑆 ∈ P))) → (𝐶 ·P 𝑆) ∈ P)
19		simplrr 777	. . . . . . 7 ⊢ ((((𝐴 ∈ P ∧ 𝐵 ∈ P) ∧ (𝐶 ∈ P ∧ 𝐷 ∈ P)) ∧ ((𝐹 ∈ P ∧ 𝐺 ∈ P) ∧ (𝑅 ∈ P ∧ 𝑆 ∈ P))) → 𝐷 ∈ P)
20		simprrl 780	. . . . . . 7 ⊢ ((((𝐴 ∈ P ∧ 𝐵 ∈ P) ∧ (𝐶 ∈ P ∧ 𝐷 ∈ P)) ∧ ((𝐹 ∈ P ∧ 𝐺 ∈ P) ∧ (𝑅 ∈ P ∧ 𝑆 ∈ P))) → 𝑅 ∈ P)
21		mulclpr 11039	. . . . . . 7 ⊢ ((𝐷 ∈ P ∧ 𝑅 ∈ P) → (𝐷 ·P 𝑅) ∈ P)
22	19, 20, 21	syl2anc 584	. . . . . 6 ⊢ ((((𝐴 ∈ P ∧ 𝐵 ∈ P) ∧ (𝐶 ∈ P ∧ 𝐷 ∈ P)) ∧ ((𝐹 ∈ P ∧ 𝐺 ∈ P) ∧ (𝑅 ∈ P ∧ 𝑆 ∈ P))) → (𝐷 ·P 𝑅) ∈ P)
23		addclpr 11037	. . . . . 6 ⊢ (((𝐶 ·P 𝑆) ∈ P ∧ (𝐷 ·P 𝑅) ∈ P) → ((𝐶 ·P 𝑆) +P (𝐷 ·P 𝑅)) ∈ P)
24	18, 22, 23	syl2anc 584	. . . . 5 ⊢ ((((𝐴 ∈ P ∧ 𝐵 ∈ P) ∧ (𝐶 ∈ P ∧ 𝐷 ∈ P)) ∧ ((𝐹 ∈ P ∧ 𝐺 ∈ P) ∧ (𝑅 ∈ P ∧ 𝑆 ∈ P))) → ((𝐶 ·P 𝑆) +P (𝐷 ·P 𝑅)) ∈ P)
25		addclpr 11037	. . . . 5 ⊢ ((((𝐴 ·P 𝐹) +P (𝐵 ·P 𝐺)) ∈ P ∧ ((𝐶 ·P 𝑆) +P (𝐷 ·P 𝑅)) ∈ P) → (((𝐴 ·P 𝐹) +P (𝐵 ·P 𝐺)) +P ((𝐶 ·P 𝑆) +P (𝐷 ·P 𝑅))) ∈ P)
26	14, 24, 25	syl2anc 584	. . . 4 ⊢ ((((𝐴 ∈ P ∧ 𝐵 ∈ P) ∧ (𝐶 ∈ P ∧ 𝐷 ∈ P)) ∧ ((𝐹 ∈ P ∧ 𝐺 ∈ P) ∧ (𝑅 ∈ P ∧ 𝑆 ∈ P))) → (((𝐴 ·P 𝐹) +P (𝐵 ·P 𝐺)) +P ((𝐶 ·P 𝑆) +P (𝐷 ·P 𝑅))) ∈ P)
27		addcanpr 11065	. . . 4 ⊢ (((𝐷 ·P 𝐹) ∈ P ∧ (((𝐴 ·P 𝐹) +P (𝐵 ·P 𝐺)) +P ((𝐶 ·P 𝑆) +P (𝐷 ·P 𝑅))) ∈ P) → (((𝐷 ·P 𝐹) +P (((𝐴 ·P 𝐹) +P (𝐵 ·P 𝐺)) +P ((𝐶 ·P 𝑆) +P (𝐷 ·P 𝑅)))) = ((𝐷 ·P 𝐹) +P (((𝐴 ·P 𝐺) +P (𝐵 ·P 𝐹)) +P ((𝐶 ·P 𝑅) +P (𝐷 ·P 𝑆)))) → (((𝐴 ·P 𝐹) +P (𝐵 ·P 𝐺)) +P ((𝐶 ·P 𝑆) +P (𝐷 ·P 𝑅))) = (((𝐴 ·P 𝐺) +P (𝐵 ·P 𝐹)) +P ((𝐶 ·P 𝑅) +P (𝐷 ·P 𝑆)))))
28	4, 26, 27	syl2anc 584	. . 3 ⊢ ((((𝐴 ∈ P ∧ 𝐵 ∈ P) ∧ (𝐶 ∈ P ∧ 𝐷 ∈ P)) ∧ ((𝐹 ∈ P ∧ 𝐺 ∈ P) ∧ (𝑅 ∈ P ∧ 𝑆 ∈ P))) → (((𝐷 ·P 𝐹) +P (((𝐴 ·P 𝐹) +P (𝐵 ·P 𝐺)) +P ((𝐶 ·P 𝑆) +P (𝐷 ·P 𝑅)))) = ((𝐷 ·P 𝐹) +P (((𝐴 ·P 𝐺) +P (𝐵 ·P 𝐹)) +P ((𝐶 ·P 𝑅) +P (𝐷 ·P 𝑆)))) → (((𝐴 ·P 𝐹) +P (𝐵 ·P 𝐺)) +P ((𝐶 ·P 𝑆) +P (𝐷 ·P 𝑅))) = (((𝐴 ·P 𝐺) +P (𝐵 ·P 𝐹)) +P ((𝐶 ·P 𝑅) +P (𝐷 ·P 𝑆)))))
29	1, 28	syl5 34	. 2 ⊢ ((((𝐴 ∈ P ∧ 𝐵 ∈ P) ∧ (𝐶 ∈ P ∧ 𝐷 ∈ P)) ∧ ((𝐹 ∈ P ∧ 𝐺 ∈ P) ∧ (𝑅 ∈ P ∧ 𝑆 ∈ P))) → (((𝐴 +P 𝐷) = (𝐵 +P 𝐶) ∧ (𝐹 +P 𝑆) = (𝐺 +P 𝑅)) → (((𝐴 ·P 𝐹) +P (𝐵 ·P 𝐺)) +P ((𝐶 ·P 𝑆) +P (𝐷 ·P 𝑅))) = (((𝐴 ·P 𝐺) +P (𝐵 ·P 𝐹)) +P ((𝐶 ·P 𝑅) +P (𝐷 ·P 𝑆)))))
30		mulclpr 11039	. . . . 5 ⊢ ((𝐴 ∈ P ∧ 𝐺 ∈ P) → (𝐴 ·P 𝐺) ∈ P)
31		mulclpr 11039	. . . . 5 ⊢ ((𝐵 ∈ P ∧ 𝐹 ∈ P) → (𝐵 ·P 𝐹) ∈ P)
32		addclpr 11037	. . . . 5 ⊢ (((𝐴 ·P 𝐺) ∈ P ∧ (𝐵 ·P 𝐹) ∈ P) → ((𝐴 ·P 𝐺) +P (𝐵 ·P 𝐹)) ∈ P)
33	30, 31, 32	syl2an 596	. . . 4 ⊢ (((𝐴 ∈ P ∧ 𝐺 ∈ P) ∧ (𝐵 ∈ P ∧ 𝐹 ∈ P)) → ((𝐴 ·P 𝐺) +P (𝐵 ·P 𝐹)) ∈ P)
34	5, 10, 9, 6, 33	syl22anc 838	. . 3 ⊢ ((((𝐴 ∈ P ∧ 𝐵 ∈ P) ∧ (𝐶 ∈ P ∧ 𝐷 ∈ P)) ∧ ((𝐹 ∈ P ∧ 𝐺 ∈ P) ∧ (𝑅 ∈ P ∧ 𝑆 ∈ P))) → ((𝐴 ·P 𝐺) +P (𝐵 ·P 𝐹)) ∈ P)
35		mulclpr 11039	. . . . 5 ⊢ ((𝐶 ∈ P ∧ 𝑅 ∈ P) → (𝐶 ·P 𝑅) ∈ P)
36		mulclpr 11039	. . . . 5 ⊢ ((𝐷 ∈ P ∧ 𝑆 ∈ P) → (𝐷 ·P 𝑆) ∈ P)
37		addclpr 11037	. . . . 5 ⊢ (((𝐶 ·P 𝑅) ∈ P ∧ (𝐷 ·P 𝑆) ∈ P) → ((𝐶 ·P 𝑅) +P (𝐷 ·P 𝑆)) ∈ P)
38	35, 36, 37	syl2an 596	. . . 4 ⊢ (((𝐶 ∈ P ∧ 𝑅 ∈ P) ∧ (𝐷 ∈ P ∧ 𝑆 ∈ P)) → ((𝐶 ·P 𝑅) +P (𝐷 ·P 𝑆)) ∈ P)
39	15, 20, 19, 16, 38	syl22anc 838	. . 3 ⊢ ((((𝐴 ∈ P ∧ 𝐵 ∈ P) ∧ (𝐶 ∈ P ∧ 𝐷 ∈ P)) ∧ ((𝐹 ∈ P ∧ 𝐺 ∈ P) ∧ (𝑅 ∈ P ∧ 𝑆 ∈ P))) → ((𝐶 ·P 𝑅) +P (𝐷 ·P 𝑆)) ∈ P)
40		enrbreq 11084	. . 3 ⊢ (((((𝐴 ·P 𝐹) +P (𝐵 ·P 𝐺)) ∈ P ∧ ((𝐴 ·P 𝐺) +P (𝐵 ·P 𝐹)) ∈ P) ∧ (((𝐶 ·P 𝑅) +P (𝐷 ·P 𝑆)) ∈ P ∧ ((𝐶 ·P 𝑆) +P (𝐷 ·P 𝑅)) ∈ P)) → (⟨((𝐴 ·P 𝐹) +P (𝐵 ·P 𝐺)), ((𝐴 ·P 𝐺) +P (𝐵 ·P 𝐹))⟩ ~R ⟨((𝐶 ·P 𝑅) +P (𝐷 ·P 𝑆)), ((𝐶 ·P 𝑆) +P (𝐷 ·P 𝑅))⟩ ↔ (((𝐴 ·P 𝐹) +P (𝐵 ·P 𝐺)) +P ((𝐶 ·P 𝑆) +P (𝐷 ·P 𝑅))) = (((𝐴 ·P 𝐺) +P (𝐵 ·P 𝐹)) +P ((𝐶 ·P 𝑅) +P (𝐷 ·P 𝑆)))))
41	14, 34, 39, 24, 40	syl22anc 838	. 2 ⊢ ((((𝐴 ∈ P ∧ 𝐵 ∈ P) ∧ (𝐶 ∈ P ∧ 𝐷 ∈ P)) ∧ ((𝐹 ∈ P ∧ 𝐺 ∈ P) ∧ (𝑅 ∈ P ∧ 𝑆 ∈ P))) → (⟨((𝐴 ·P 𝐹) +P (𝐵 ·P 𝐺)), ((𝐴 ·P 𝐺) +P (𝐵 ·P 𝐹))⟩ ~R ⟨((𝐶 ·P 𝑅) +P (𝐷 ·P 𝑆)), ((𝐶 ·P 𝑆) +P (𝐷 ·P 𝑅))⟩ ↔ (((𝐴 ·P 𝐹) +P (𝐵 ·P 𝐺)) +P ((𝐶 ·P 𝑆) +P (𝐷 ·P 𝑅))) = (((𝐴 ·P 𝐺) +P (𝐵 ·P 𝐹)) +P ((𝐶 ·P 𝑅) +P (𝐷 ·P 𝑆)))))
42	29, 41	sylibrd 259	1 ⊢ ((((𝐴 ∈ P ∧ 𝐵 ∈ P) ∧ (𝐶 ∈ P ∧ 𝐷 ∈ P)) ∧ ((𝐹 ∈ P ∧ 𝐺 ∈ P) ∧ (𝑅 ∈ P ∧ 𝑆 ∈ P))) → (((𝐴 +P 𝐷) = (𝐵 +P 𝐶) ∧ (𝐹 +P 𝑆) = (𝐺 +P 𝑅)) → ⟨((𝐴 ·P 𝐹) +P (𝐵 ·P 𝐺)), ((𝐴 ·P 𝐺) +P (𝐵 ·P 𝐹))⟩ ~R ⟨((𝐶 ·P 𝑅) +P (𝐷 ·P 𝑆)), ((𝐶 ·P 𝑆) +P (𝐷 ·P 𝑅))⟩))

Syntax hints:   → wi 4   ↔ wb 206   ∧ wa 395   = wceq 1540   ∈ wcel 2109  ⟨cop 4612   class class class wbr 5124  (class class class)co 7410  Pcnp 10878   +_P cpp 10880   ·_P cmp 10881   ~_R cer 10883

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-10 2142  ax-11 2158  ax-12 2178  ax-ext 2708  ax-sep 5271  ax-nul 5281  ax-pow 5340  ax-pr 5407  ax-un 7734  ax-inf2 9660

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3or 1087  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1780  df-nf 1784  df-sb 2066  df-mo 2540  df-eu 2569  df-clab 2715  df-cleq 2728  df-clel 2810  df-nfc 2886  df-ne 2934  df-ral 3053  df-rex 3062  df-rmo 3364  df-reu 3365  df-rab 3421  df-v 3466  df-sbc 3771  df-csb 3880  df-dif 3934  df-un 3936  df-in 3938  df-ss 3948  df-pss 3951  df-nul 4314  df-if 4506  df-pw 4582  df-sn 4607  df-pr 4609  df-op 4613  df-uni 4889  df-int 4928  df-iun 4974  df-br 5125  df-opab 5187  df-mpt 5207  df-tr 5235  df-id 5553  df-eprel 5558  df-po 5566  df-so 5567  df-fr 5611  df-we 5613  df-xp 5665  df-rel 5666  df-cnv 5667  df-co 5668  df-dm 5669  df-rn 5670  df-res 5671  df-ima 5672  df-pred 6295  df-ord 6360  df-on 6361  df-lim 6362  df-suc 6363  df-iota 6489  df-fun 6538  df-fn 6539  df-f 6540  df-f1 6541  df-fo 6542  df-f1o 6543  df-fv 6544  df-ov 7413  df-oprab 7414  df-mpo 7415  df-om 7867  df-1st 7993  df-2nd 7994  df-frecs 8285  df-wrecs 8316  df-recs 8390  df-rdg 8429  df-1o 8485  df-oadd 8489  df-omul 8490  df-er 8724  df-ni 10891  df-pli 10892  df-mi 10893  df-lti 10894  df-plpq 10927  df-mpq 10928  df-ltpq 10929  df-enq 10930  df-nq 10931  df-erq 10932  df-plq 10933  df-mq 10934  df-1nq 10935  df-rq 10936  df-ltnq 10937  df-np 11000  df-plp 11002  df-mp 11003  df-ltp 11004  df-enr 11074

This theorem is referenced by:  mulsrmo  11093