Theorem addcmpblnr

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

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

Proof

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