addcmpblnr

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

		Ref	Expression
	Assertion	addcmpblnr	$⊢ (((A \in 𝑷 \land B \in 𝑷) \land (C \in 𝑷 \land D \in 𝑷)) \land ((F \in 𝑷 \land G \in 𝑷) \land (R \in 𝑷 \land S \in 𝑷))) \to ((A +_{𝑷} D = B +_{𝑷} C \land F +_{𝑷} S = G +_{𝑷} R) \to ⟨A +_{𝑷} F, B +_{𝑷} G⟩ ~_{𝑹} ⟨C +_{𝑷} R, D +_{𝑷} S⟩)$

Proof

Step	Hyp	Ref	Expression
1		oveq12	$⊢ (A +_{𝑷} D = B +_{𝑷} C \land F +_{𝑷} S = G +_{𝑷} R) \to (A +_{𝑷} D) +_{𝑷} (F +_{𝑷} S) = (B +_{𝑷} C) +_{𝑷} (G +_{𝑷} R)$
2		addclpr	$⊢ (A \in 𝑷 \land F \in 𝑷) \to A +_{𝑷} F \in 𝑷$
3		addclpr	$⊢ (B \in 𝑷 \land G \in 𝑷) \to B +_{𝑷} G \in 𝑷$
4	2 3	anim12i	$⊢ ((A \in 𝑷 \land F \in 𝑷) \land (B \in 𝑷 \land G \in 𝑷)) \to (A +_{𝑷} F \in 𝑷 \land B +_{𝑷} G \in 𝑷)$
5	4	an4s	$⊢ ((A \in 𝑷 \land B \in 𝑷) \land (F \in 𝑷 \land G \in 𝑷)) \to (A +_{𝑷} F \in 𝑷 \land B +_{𝑷} G \in 𝑷)$
6		addclpr	$⊢ (C \in 𝑷 \land R \in 𝑷) \to C +_{𝑷} R \in 𝑷$
7		addclpr	$⊢ (D \in 𝑷 \land S \in 𝑷) \to D +_{𝑷} S \in 𝑷$
8	6 7	anim12i	$⊢ ((C \in 𝑷 \land R \in 𝑷) \land (D \in 𝑷 \land S \in 𝑷)) \to (C +_{𝑷} R \in 𝑷 \land D +_{𝑷} S \in 𝑷)$
9	8	an4s	$⊢ ((C \in 𝑷 \land D \in 𝑷) \land (R \in 𝑷 \land S \in 𝑷)) \to (C +_{𝑷} R \in 𝑷 \land D +_{𝑷} S \in 𝑷)$
10	5 9	anim12i	$⊢ (((A \in 𝑷 \land B \in 𝑷) \land (F \in 𝑷 \land G \in 𝑷)) \land ((C \in 𝑷 \land D \in 𝑷) \land (R \in 𝑷 \land S \in 𝑷))) \to ((A +_{𝑷} F \in 𝑷 \land B +_{𝑷} G \in 𝑷) \land (C +_{𝑷} R \in 𝑷 \land D +_{𝑷} S \in 𝑷))$
11	10	an4s	$⊢ (((A \in 𝑷 \land B \in 𝑷) \land (C \in 𝑷 \land D \in 𝑷)) \land ((F \in 𝑷 \land G \in 𝑷) \land (R \in 𝑷 \land S \in 𝑷))) \to ((A +_{𝑷} F \in 𝑷 \land B +_{𝑷} G \in 𝑷) \land (C +_{𝑷} R \in 𝑷 \land D +_{𝑷} S \in 𝑷))$
12		enrbreq	$⊢ ((A +_{𝑷} F \in 𝑷 \land B +_{𝑷} G \in 𝑷) \land (C +_{𝑷} R \in 𝑷 \land D +_{𝑷} S \in 𝑷)) \to (⟨A +_{𝑷} F, B +_{𝑷} G⟩ ~_{𝑹} ⟨C +_{𝑷} R, D +_{𝑷} S⟩ \leftrightarrow (A +_{𝑷} F) +_{𝑷} (D +_{𝑷} S) = (B +_{𝑷} G) +_{𝑷} (C +_{𝑷} R))$
13	11 12	syl	$⊢ (((A \in 𝑷 \land B \in 𝑷) \land (C \in 𝑷 \land D \in 𝑷)) \land ((F \in 𝑷 \land G \in 𝑷) \land (R \in 𝑷 \land S \in 𝑷))) \to (⟨A +_{𝑷} F, B +_{𝑷} G⟩ ~_{𝑹} ⟨C +_{𝑷} R, D +_{𝑷} S⟩ \leftrightarrow (A +_{𝑷} F) +_{𝑷} (D +_{𝑷} S) = (B +_{𝑷} G) +_{𝑷} (C +_{𝑷} R))$
14		addcompr	$⊢ F +_{𝑷} D = D +_{𝑷} F$
15	14	oveq1i	$⊢ (F +_{𝑷} D) +_{𝑷} S = (D +_{𝑷} F) +_{𝑷} S$
16		addasspr	$⊢ (F +_{𝑷} D) +_{𝑷} S = F +_{𝑷} (D +_{𝑷} S)$
17		addasspr	$⊢ (D +_{𝑷} F) +_{𝑷} S = D +_{𝑷} (F +_{𝑷} S)$
18	15 16 17	3eqtr3i	$⊢ F +_{𝑷} (D +_{𝑷} S) = D +_{𝑷} (F +_{𝑷} S)$
19	18	oveq2i	$⊢ A +_{𝑷} (F +_{𝑷} (D +_{𝑷} S)) = A +_{𝑷} (D +_{𝑷} (F +_{𝑷} S))$
20		addasspr	$⊢ (A +_{𝑷} F) +_{𝑷} (D +_{𝑷} S) = A +_{𝑷} (F +_{𝑷} (D +_{𝑷} S))$
21		addasspr	$⊢ (A +_{𝑷} D) +_{𝑷} (F +_{𝑷} S) = A +_{𝑷} (D +_{𝑷} (F +_{𝑷} S))$
22	19 20 21	3eqtr4i	$⊢ (A +_{𝑷} F) +_{𝑷} (D +_{𝑷} S) = (A +_{𝑷} D) +_{𝑷} (F +_{𝑷} S)$
23		addcompr	$⊢ G +_{𝑷} C = C +_{𝑷} G$
24	23	oveq1i	$⊢ (G +_{𝑷} C) +_{𝑷} R = (C +_{𝑷} G) +_{𝑷} R$
25		addasspr	$⊢ (G +_{𝑷} C) +_{𝑷} R = G +_{𝑷} (C +_{𝑷} R)$
26		addasspr	$⊢ (C +_{𝑷} G) +_{𝑷} R = C +_{𝑷} (G +_{𝑷} R)$
27	24 25 26	3eqtr3i	$⊢ G +_{𝑷} (C +_{𝑷} R) = C +_{𝑷} (G +_{𝑷} R)$
28	27	oveq2i	$⊢ B +_{𝑷} (G +_{𝑷} (C +_{𝑷} R)) = B +_{𝑷} (C +_{𝑷} (G +_{𝑷} R))$
29		addasspr	$⊢ (B +_{𝑷} G) +_{𝑷} (C +_{𝑷} R) = B +_{𝑷} (G +_{𝑷} (C +_{𝑷} R))$
30		addasspr	$⊢ (B +_{𝑷} C) +_{𝑷} (G +_{𝑷} R) = B +_{𝑷} (C +_{𝑷} (G +_{𝑷} R))$
31	28 29 30	3eqtr4i	$⊢ (B +_{𝑷} G) +_{𝑷} (C +_{𝑷} R) = (B +_{𝑷} C) +_{𝑷} (G +_{𝑷} R)$
32	22 31	eqeq12i	$⊢ (A +_{𝑷} F) +_{𝑷} (D +_{𝑷} S) = (B +_{𝑷} G) +_{𝑷} (C +_{𝑷} R) \leftrightarrow (A +_{𝑷} D) +_{𝑷} (F +_{𝑷} S) = (B +_{𝑷} C) +_{𝑷} (G +_{𝑷} R)$
33	13 32	bitrdi	$⊢ (((A \in 𝑷 \land B \in 𝑷) \land (C \in 𝑷 \land D \in 𝑷)) \land ((F \in 𝑷 \land G \in 𝑷) \land (R \in 𝑷 \land S \in 𝑷))) \to (⟨A +_{𝑷} F, B +_{𝑷} G⟩ ~_{𝑹} ⟨C +_{𝑷} R, D +_{𝑷} S⟩ \leftrightarrow (A +_{𝑷} D) +_{𝑷} (F +_{𝑷} S) = (B +_{𝑷} C) +_{𝑷} (G +_{𝑷} R))$
34	1 33	imbitrrid	$⊢ (((A \in 𝑷 \land B \in 𝑷) \land (C \in 𝑷 \land D \in 𝑷)) \land ((F \in 𝑷 \land G \in 𝑷) \land (R \in 𝑷 \land S \in 𝑷))) \to ((A +_{𝑷} D = B +_{𝑷} C \land F +_{𝑷} S = G +_{𝑷} R) \to ⟨A +_{𝑷} F, B +_{𝑷} G⟩ ~_{𝑹} ⟨C +_{𝑷} R, D +_{𝑷} S⟩)$

Metamath Proof Explorer

Theorem addcmpblnr

Proof