Users' Mathboxes Mathbox for Norm Megill < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  paddcom Structured version   Visualization version   GIF version

Theorem paddcom 34618
Description: Projective subspace sum commutes. (Contributed by NM, 3-Jan-2012.)
Hypotheses
Ref Expression
padd0.a 𝐴 = (Atoms‘𝐾)
padd0.p + = (+𝑃𝐾)
Assertion
Ref Expression
paddcom ((𝐾 ∈ Lat ∧ 𝑋𝐴𝑌𝐴) → (𝑋 + 𝑌) = (𝑌 + 𝑋))

Proof of Theorem paddcom
Dummy variables 𝑞 𝑝 𝑟 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 uncom 3741 . . . 4 (𝑋𝑌) = (𝑌𝑋)
21a1i 11 . . 3 ((𝐾 ∈ Lat ∧ 𝑋𝐴𝑌𝐴) → (𝑋𝑌) = (𝑌𝑋))
3 simpl1 1062 . . . . . . . 8 (((𝐾 ∈ Lat ∧ 𝑋𝐴𝑌𝐴) ∧ (𝑞𝑋𝑟𝑌)) → 𝐾 ∈ Lat)
4 simpl2 1063 . . . . . . . . . 10 (((𝐾 ∈ Lat ∧ 𝑋𝐴𝑌𝐴) ∧ (𝑞𝑋𝑟𝑌)) → 𝑋𝐴)
5 simprl 793 . . . . . . . . . 10 (((𝐾 ∈ Lat ∧ 𝑋𝐴𝑌𝐴) ∧ (𝑞𝑋𝑟𝑌)) → 𝑞𝑋)
64, 5sseldd 3589 . . . . . . . . 9 (((𝐾 ∈ Lat ∧ 𝑋𝐴𝑌𝐴) ∧ (𝑞𝑋𝑟𝑌)) → 𝑞𝐴)
7 eqid 2621 . . . . . . . . . 10 (Base‘𝐾) = (Base‘𝐾)
8 padd0.a . . . . . . . . . 10 𝐴 = (Atoms‘𝐾)
97, 8atbase 34095 . . . . . . . . 9 (𝑞𝐴𝑞 ∈ (Base‘𝐾))
106, 9syl 17 . . . . . . . 8 (((𝐾 ∈ Lat ∧ 𝑋𝐴𝑌𝐴) ∧ (𝑞𝑋𝑟𝑌)) → 𝑞 ∈ (Base‘𝐾))
11 simpl3 1064 . . . . . . . . . 10 (((𝐾 ∈ Lat ∧ 𝑋𝐴𝑌𝐴) ∧ (𝑞𝑋𝑟𝑌)) → 𝑌𝐴)
12 simprr 795 . . . . . . . . . 10 (((𝐾 ∈ Lat ∧ 𝑋𝐴𝑌𝐴) ∧ (𝑞𝑋𝑟𝑌)) → 𝑟𝑌)
1311, 12sseldd 3589 . . . . . . . . 9 (((𝐾 ∈ Lat ∧ 𝑋𝐴𝑌𝐴) ∧ (𝑞𝑋𝑟𝑌)) → 𝑟𝐴)
147, 8atbase 34095 . . . . . . . . 9 (𝑟𝐴𝑟 ∈ (Base‘𝐾))
1513, 14syl 17 . . . . . . . 8 (((𝐾 ∈ Lat ∧ 𝑋𝐴𝑌𝐴) ∧ (𝑞𝑋𝑟𝑌)) → 𝑟 ∈ (Base‘𝐾))
16 eqid 2621 . . . . . . . . 9 (join‘𝐾) = (join‘𝐾)
177, 16latjcom 16999 . . . . . . . 8 ((𝐾 ∈ Lat ∧ 𝑞 ∈ (Base‘𝐾) ∧ 𝑟 ∈ (Base‘𝐾)) → (𝑞(join‘𝐾)𝑟) = (𝑟(join‘𝐾)𝑞))
183, 10, 15, 17syl3anc 1323 . . . . . . 7 (((𝐾 ∈ Lat ∧ 𝑋𝐴𝑌𝐴) ∧ (𝑞𝑋𝑟𝑌)) → (𝑞(join‘𝐾)𝑟) = (𝑟(join‘𝐾)𝑞))
1918breq2d 4635 . . . . . 6 (((𝐾 ∈ Lat ∧ 𝑋𝐴𝑌𝐴) ∧ (𝑞𝑋𝑟𝑌)) → (𝑝(le‘𝐾)(𝑞(join‘𝐾)𝑟) ↔ 𝑝(le‘𝐾)(𝑟(join‘𝐾)𝑞)))
20192rexbidva 3051 . . . . 5 ((𝐾 ∈ Lat ∧ 𝑋𝐴𝑌𝐴) → (∃𝑞𝑋𝑟𝑌 𝑝(le‘𝐾)(𝑞(join‘𝐾)𝑟) ↔ ∃𝑞𝑋𝑟𝑌 𝑝(le‘𝐾)(𝑟(join‘𝐾)𝑞)))
21 rexcom 3093 . . . . 5 (∃𝑞𝑋𝑟𝑌 𝑝(le‘𝐾)(𝑟(join‘𝐾)𝑞) ↔ ∃𝑟𝑌𝑞𝑋 𝑝(le‘𝐾)(𝑟(join‘𝐾)𝑞))
2220, 21syl6bb 276 . . . 4 ((𝐾 ∈ Lat ∧ 𝑋𝐴𝑌𝐴) → (∃𝑞𝑋𝑟𝑌 𝑝(le‘𝐾)(𝑞(join‘𝐾)𝑟) ↔ ∃𝑟𝑌𝑞𝑋 𝑝(le‘𝐾)(𝑟(join‘𝐾)𝑞)))
2322rabbidv 3181 . . 3 ((𝐾 ∈ Lat ∧ 𝑋𝐴𝑌𝐴) → {𝑝𝐴 ∣ ∃𝑞𝑋𝑟𝑌 𝑝(le‘𝐾)(𝑞(join‘𝐾)𝑟)} = {𝑝𝐴 ∣ ∃𝑟𝑌𝑞𝑋 𝑝(le‘𝐾)(𝑟(join‘𝐾)𝑞)})
242, 23uneq12d 3752 . 2 ((𝐾 ∈ Lat ∧ 𝑋𝐴𝑌𝐴) → ((𝑋𝑌) ∪ {𝑝𝐴 ∣ ∃𝑞𝑋𝑟𝑌 𝑝(le‘𝐾)(𝑞(join‘𝐾)𝑟)}) = ((𝑌𝑋) ∪ {𝑝𝐴 ∣ ∃𝑟𝑌𝑞𝑋 𝑝(le‘𝐾)(𝑟(join‘𝐾)𝑞)}))
25 eqid 2621 . . 3 (le‘𝐾) = (le‘𝐾)
26 padd0.p . . 3 + = (+𝑃𝐾)
2725, 16, 8, 26paddval 34603 . 2 ((𝐾 ∈ Lat ∧ 𝑋𝐴𝑌𝐴) → (𝑋 + 𝑌) = ((𝑋𝑌) ∪ {𝑝𝐴 ∣ ∃𝑞𝑋𝑟𝑌 𝑝(le‘𝐾)(𝑞(join‘𝐾)𝑟)}))
2825, 16, 8, 26paddval 34603 . . 3 ((𝐾 ∈ Lat ∧ 𝑌𝐴𝑋𝐴) → (𝑌 + 𝑋) = ((𝑌𝑋) ∪ {𝑝𝐴 ∣ ∃𝑟𝑌𝑞𝑋 𝑝(le‘𝐾)(𝑟(join‘𝐾)𝑞)}))
29283com23 1268 . 2 ((𝐾 ∈ Lat ∧ 𝑋𝐴𝑌𝐴) → (𝑌 + 𝑋) = ((𝑌𝑋) ∪ {𝑝𝐴 ∣ ∃𝑟𝑌𝑞𝑋 𝑝(le‘𝐾)(𝑟(join‘𝐾)𝑞)}))
3024, 27, 293eqtr4d 2665 1 ((𝐾 ∈ Lat ∧ 𝑋𝐴𝑌𝐴) → (𝑋 + 𝑌) = (𝑌 + 𝑋))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 384  w3a 1036   = wceq 1480  wcel 1987  wrex 2909  {crab 2912  cun 3558  wss 3560   class class class wbr 4623  cfv 5857  (class class class)co 6615  Basecbs 15800  lecple 15888  joincjn 16884  Latclat 16985  Atomscatm 34069  +𝑃cpadd 34600
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1719  ax-4 1734  ax-5 1836  ax-6 1885  ax-7 1932  ax-8 1989  ax-9 1996  ax-10 2016  ax-11 2031  ax-12 2044  ax-13 2245  ax-ext 2601  ax-rep 4741  ax-sep 4751  ax-nul 4759  ax-pow 4813  ax-pr 4877  ax-un 6914
This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-3an 1038  df-tru 1483  df-ex 1702  df-nf 1707  df-sb 1878  df-eu 2473  df-mo 2474  df-clab 2608  df-cleq 2614  df-clel 2617  df-nfc 2750  df-ne 2791  df-ral 2913  df-rex 2914  df-reu 2915  df-rab 2917  df-v 3192  df-sbc 3423  df-csb 3520  df-dif 3563  df-un 3565  df-in 3567  df-ss 3574  df-nul 3898  df-if 4065  df-pw 4138  df-sn 4156  df-pr 4158  df-op 4162  df-uni 4410  df-iun 4494  df-br 4624  df-opab 4684  df-mpt 4685  df-id 4999  df-xp 5090  df-rel 5091  df-cnv 5092  df-co 5093  df-dm 5094  df-rn 5095  df-res 5096  df-ima 5097  df-iota 5820  df-fun 5859  df-fn 5860  df-f 5861  df-f1 5862  df-fo 5863  df-f1o 5864  df-fv 5865  df-riota 6576  df-ov 6618  df-oprab 6619  df-mpt2 6620  df-1st 7128  df-2nd 7129  df-lub 16914  df-join 16916  df-lat 16986  df-ats 34073  df-padd 34601
This theorem is referenced by:  paddass  34643  padd12N  34644  pmod2iN  34654  pmodN  34655  pmapjat2  34659
  Copyright terms: Public domain W3C validator