Theorem addcomprg 6404

Description: Addition of positive reals is commutative. Proposition 9-3.5(ii) of [Gleason] p. 123. (Contributed by Jim Kingdon, 11-Dec-2019.)

Assertion

Ref	Expression
addcomprg	⊢ ((A ∈ P ∧ B ∈ P) → (A +P B) = (B +P A))

Proof of Theorem addcomprg

Dummy variables x y z are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		prop 6316	. . . . . . . . 9 ⊢ (B ∈ P → ⟨(1st ‘B), (2nd ‘B)⟩ ∈ P)
2		elprnql 6322	. . . . . . . . 9 ⊢ ((⟨(1st ‘B), (2nd ‘B)⟩ ∈ P ∧ y ∈ (1st ‘B)) → y ∈ Q)
3	1, 2	sylan 267	. . . . . . . 8 ⊢ ((B ∈ P ∧ y ∈ (1st ‘B)) → y ∈ Q)
4		prop 6316	. . . . . . . . . . . . 13 ⊢ (A ∈ P → ⟨(1st ‘A), (2nd ‘A)⟩ ∈ P)
5		elprnql 6322	. . . . . . . . . . . . 13 ⊢ ((⟨(1st ‘A), (2nd ‘A)⟩ ∈ P ∧ z ∈ (1st ‘A)) → z ∈ Q)
6	4, 5	sylan 267	. . . . . . . . . . . 12 ⊢ ((A ∈ P ∧ z ∈ (1st ‘A)) → z ∈ Q)
7		addcomnqg 6227	. . . . . . . . . . . . 13 ⊢ ((y ∈ Q ∧ z ∈ Q) → (y +Q z) = (z +Q y))
8	7	eqeq2d 2025	. . . . . . . . . . . 12 ⊢ ((y ∈ Q ∧ z ∈ Q) → (x = (y +Q z) ↔ x = (z +Q y)))
9	6, 8	sylan2 270	. . . . . . . . . . 11 ⊢ ((y ∈ Q ∧ (A ∈ P ∧ z ∈ (1st ‘A))) → (x = (y +Q z) ↔ x = (z +Q y)))
10	9	anassrs 380	. . . . . . . . . 10 ⊢ (((y ∈ Q ∧ A ∈ P) ∧ z ∈ (1st ‘A)) → (x = (y +Q z) ↔ x = (z +Q y)))
11	10	rexbidva 2293	. . . . . . . . 9 ⊢ ((y ∈ Q ∧ A ∈ P) → (∃z ∈ (1st ‘A)x = (y +Q z) ↔ ∃z ∈ (1st ‘A)x = (z +Q y)))
12	11	ancoms 255	. . . . . . . 8 ⊢ ((A ∈ P ∧ y ∈ Q) → (∃z ∈ (1st ‘A)x = (y +Q z) ↔ ∃z ∈ (1st ‘A)x = (z +Q y)))
13	3, 12	sylan2 270	. . . . . . 7 ⊢ ((A ∈ P ∧ (B ∈ P ∧ y ∈ (1st ‘B))) → (∃z ∈ (1st ‘A)x = (y +Q z) ↔ ∃z ∈ (1st ‘A)x = (z +Q y)))
14	13	anassrs 380	. . . . . 6 ⊢ (((A ∈ P ∧ B ∈ P) ∧ y ∈ (1st ‘B)) → (∃z ∈ (1st ‘A)x = (y +Q z) ↔ ∃z ∈ (1st ‘A)x = (z +Q y)))
15	14	rexbidva 2293	. . . . 5 ⊢ ((A ∈ P ∧ B ∈ P) → (∃y ∈ (1st ‘B)∃z ∈ (1st ‘A)x = (y +Q z) ↔ ∃y ∈ (1st ‘B)∃z ∈ (1st ‘A)x = (z +Q y)))
16		rexcom 2444	. . . . 5 ⊢ (∃y ∈ (1st ‘B)∃z ∈ (1st ‘A)x = (z +Q y) ↔ ∃z ∈ (1st ‘A)∃y ∈ (1st ‘B)x = (z +Q y))
17	15, 16	syl6bb 185	. . . 4 ⊢ ((A ∈ P ∧ B ∈ P) → (∃y ∈ (1st ‘B)∃z ∈ (1st ‘A)x = (y +Q z) ↔ ∃z ∈ (1st ‘A)∃y ∈ (1st ‘B)x = (z +Q y)))
18	17	rabbidv 2519	. . 3 ⊢ ((A ∈ P ∧ B ∈ P) → {x ∈ Q ∣ ∃y ∈ (1st ‘B)∃z ∈ (1st ‘A)x = (y +Q z)} = {x ∈ Q ∣ ∃z ∈ (1st ‘A)∃y ∈ (1st ‘B)x = (z +Q y)})
19		elprnqu 6323	. . . . . . . . 9 ⊢ ((⟨(1st ‘B), (2nd ‘B)⟩ ∈ P ∧ y ∈ (2nd ‘B)) → y ∈ Q)
20	1, 19	sylan 267	. . . . . . . 8 ⊢ ((B ∈ P ∧ y ∈ (2nd ‘B)) → y ∈ Q)
21		elprnqu 6323	. . . . . . . . . . . . 13 ⊢ ((⟨(1st ‘A), (2nd ‘A)⟩ ∈ P ∧ z ∈ (2nd ‘A)) → z ∈ Q)
22	4, 21	sylan 267	. . . . . . . . . . . 12 ⊢ ((A ∈ P ∧ z ∈ (2nd ‘A)) → z ∈ Q)
23	22, 8	sylan2 270	. . . . . . . . . . 11 ⊢ ((y ∈ Q ∧ (A ∈ P ∧ z ∈ (2nd ‘A))) → (x = (y +Q z) ↔ x = (z +Q y)))
24	23	anassrs 380	. . . . . . . . . 10 ⊢ (((y ∈ Q ∧ A ∈ P) ∧ z ∈ (2nd ‘A)) → (x = (y +Q z) ↔ x = (z +Q y)))
25	24	rexbidva 2293	. . . . . . . . 9 ⊢ ((y ∈ Q ∧ A ∈ P) → (∃z ∈ (2nd ‘A)x = (y +Q z) ↔ ∃z ∈ (2nd ‘A)x = (z +Q y)))
26	25	ancoms 255	. . . . . . . 8 ⊢ ((A ∈ P ∧ y ∈ Q) → (∃z ∈ (2nd ‘A)x = (y +Q z) ↔ ∃z ∈ (2nd ‘A)x = (z +Q y)))
27	20, 26	sylan2 270	. . . . . . 7 ⊢ ((A ∈ P ∧ (B ∈ P ∧ y ∈ (2nd ‘B))) → (∃z ∈ (2nd ‘A)x = (y +Q z) ↔ ∃z ∈ (2nd ‘A)x = (z +Q y)))
28	27	anassrs 380	. . . . . 6 ⊢ (((A ∈ P ∧ B ∈ P) ∧ y ∈ (2nd ‘B)) → (∃z ∈ (2nd ‘A)x = (y +Q z) ↔ ∃z ∈ (2nd ‘A)x = (z +Q y)))
29	28	rexbidva 2293	. . . . 5 ⊢ ((A ∈ P ∧ B ∈ P) → (∃y ∈ (2nd ‘B)∃z ∈ (2nd ‘A)x = (y +Q z) ↔ ∃y ∈ (2nd ‘B)∃z ∈ (2nd ‘A)x = (z +Q y)))
30		rexcom 2444	. . . . 5 ⊢ (∃y ∈ (2nd ‘B)∃z ∈ (2nd ‘A)x = (z +Q y) ↔ ∃z ∈ (2nd ‘A)∃y ∈ (2nd ‘B)x = (z +Q y))
31	29, 30	syl6bb 185	. . . 4 ⊢ ((A ∈ P ∧ B ∈ P) → (∃y ∈ (2nd ‘B)∃z ∈ (2nd ‘A)x = (y +Q z) ↔ ∃z ∈ (2nd ‘A)∃y ∈ (2nd ‘B)x = (z +Q y)))
32	31	rabbidv 2519	. . 3 ⊢ ((A ∈ P ∧ B ∈ P) → {x ∈ Q ∣ ∃y ∈ (2nd ‘B)∃z ∈ (2nd ‘A)x = (y +Q z)} = {x ∈ Q ∣ ∃z ∈ (2nd ‘A)∃y ∈ (2nd ‘B)x = (z +Q y)})
33	18, 32	opeq12d 3521	. 2 ⊢ ((A ∈ P ∧ B ∈ P) → ⟨{x ∈ Q ∣ ∃y ∈ (1st ‘B)∃z ∈ (1st ‘A)x = (y +Q z)}, {x ∈ Q ∣ ∃y ∈ (2nd ‘B)∃z ∈ (2nd ‘A)x = (y +Q z)}⟩ = ⟨{x ∈ Q ∣ ∃z ∈ (1st ‘A)∃y ∈ (1st ‘B)x = (z +Q y)}, {x ∈ Q ∣ ∃z ∈ (2nd ‘A)∃y ∈ (2nd ‘B)x = (z +Q y)}⟩)
34		plpvlu 6380	. . 3 ⊢ ((B ∈ P ∧ A ∈ P) → (B +P A) = ⟨{x ∈ Q ∣ ∃y ∈ (1st ‘B)∃z ∈ (1st ‘A)x = (y +Q z)}, {x ∈ Q ∣ ∃y ∈ (2nd ‘B)∃z ∈ (2nd ‘A)x = (y +Q z)}⟩)
35	34	ancoms 255	. 2 ⊢ ((A ∈ P ∧ B ∈ P) → (B +P A) = ⟨{x ∈ Q ∣ ∃y ∈ (1st ‘B)∃z ∈ (1st ‘A)x = (y +Q z)}, {x ∈ Q ∣ ∃y ∈ (2nd ‘B)∃z ∈ (2nd ‘A)x = (y +Q z)}⟩)
36		plpvlu 6380	. 2 ⊢ ((A ∈ P ∧ B ∈ P) → (A +P B) = ⟨{x ∈ Q ∣ ∃z ∈ (1st ‘A)∃y ∈ (1st ‘B)x = (z +Q y)}, {x ∈ Q ∣ ∃z ∈ (2nd ‘A)∃y ∈ (2nd ‘B)x = (z +Q y)}⟩)
37	33, 35, 36	3eqtr4rd 2057	1 ⊢ ((A ∈ P ∧ B ∈ P) → (A +P B) = (B +P A))

Syntax hints:   → wi 4   ∧ wa 97   ↔ wb 98   = wceq 1224   ∈ wcel 1367  ∃wrex 2277  {crab 2280  ⟨cop 3343  ‘cfv 4818  (class class class)co 5425  1^st c1st 5677  2^nd c2nd 5678  Qcnq 6127   +_Q cplq 6129  Pcnp 6138   +_P cpp 6140

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 99  ax-ia2 100  ax-ia3 101  ax-in1 529  ax-in2 530  ax-io 614  ax-5 1310  ax-7 1311  ax-gen 1312  ax-ie1 1356  ax-ie2 1357  ax-8 1369  ax-10 1370  ax-11 1371  ax-i12 1372  ax-bnd 1373  ax-4 1374  ax-13 1378  ax-14 1379  ax-17 1393  ax-i9 1397  ax-ial 1401  ax-i5r 1402  ax-ext 1996  ax-coll 3836  ax-sep 3839  ax-nul 3847  ax-pow 3891  ax-pr 3908  ax-un 4109  ax-setind 4193  ax-iinf 4227

This theorem depends on definitions:  df-bi 110  df-dc 727  df-3or 868  df-3an 869  df-tru 1227  df-fal 1230  df-nf 1324  df-sb 1620  df-eu 1877  df-mo 1878  df-clab 2001  df-cleq 2007  df-clel 2010  df-nfc 2141  df-ne 2180  df-ral 2281  df-rex 2282  df-reu 2283  df-rab 2285  df-v 2529  df-sbc 2734  df-csb 2822  df-dif 2889  df-un 2891  df-in 2893  df-ss 2900  df-nul 3194  df-pw 3326  df-sn 3346  df-pr 3347  df-op 3349  df-uni 3545  df-int 3580  df-iun 3623  df-br 3729  df-opab 3783  df-mpt 3784  df-tr 3819  df-id 3994  df-iord 4042  df-on 4044  df-suc 4047  df-iom 4230  df-xp 4267  df-rel 4268  df-cnv 4269  df-co 4270  df-dm 4271  df-rn 4272  df-res 4273  df-ima 4274  df-iota 4783  df-fun 4820  df-fn 4821  df-f 4822  df-f1 4823  df-fo 4824  df-f1o 4825  df-fv 4826  df-ov 5428  df-oprab 5429  df-mpt2 5430  df-1st 5679  df-2nd 5680  df-recs 5831  df-irdg 5867  df-oadd 5909  df-omul 5910  df-er 6006  df-ec 6008  df-qs 6012  df-ni 6151  df-pli 6152  df-mi 6153  df-plpq 6190  df-enq 6193  df-nqqs 6194  df-plqqs 6195  df-inp 6307  df-iplp 6309

This theorem is referenced by:  addextpr  6443  enrer  6474  addcmpblnr  6478  mulcmpblnrlemg  6479  ltsrprg  6486  addcomsrg  6494  mulcomsrg  6496  mulasssrg  6497  distrsrg  6498  lttrsr  6501  ltposr  6502  ltsosr  6503  0lt1sr  6504  0idsr  6506  1idsr  6507  ltasrg  6509  recexgt0sr  6512  mulgt0sr  6515  aptisr  6516  mulextsr1lem  6517