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

Theorem pmodlem2 36428
Description: Lemma for pmod1i 36429. (Contributed by NM, 9-Mar-2012.)
Hypotheses
Ref Expression
pmodlem.l = (le‘𝐾)
pmodlem.j = (join‘𝐾)
pmodlem.a 𝐴 = (Atoms‘𝐾)
pmodlem.s 𝑆 = (PSubSp‘𝐾)
pmodlem.p + = (+𝑃𝐾)
Assertion
Ref Expression
pmodlem2 ((𝐾 ∈ HL ∧ (𝑋𝐴𝑌𝐴𝑍𝑆) ∧ 𝑋𝑍) → ((𝑋 + 𝑌) ∩ 𝑍) ⊆ (𝑋 + (𝑌𝑍)))

Proof of Theorem pmodlem2
Dummy variables 𝑞 𝑝 𝑟 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 simpr 477 . . . . . 6 (((𝐾 ∈ HL ∧ (𝑋𝐴𝑌𝐴𝑍𝑆) ∧ 𝑋𝑍) ∧ 𝑋 = ∅) → 𝑋 = ∅)
21oveq1d 6985 . . . . 5 (((𝐾 ∈ HL ∧ (𝑋𝐴𝑌𝐴𝑍𝑆) ∧ 𝑋𝑍) ∧ 𝑋 = ∅) → (𝑋 + 𝑌) = (∅ + 𝑌))
3 simpl1 1171 . . . . . 6 (((𝐾 ∈ HL ∧ (𝑋𝐴𝑌𝐴𝑍𝑆) ∧ 𝑋𝑍) ∧ 𝑋 = ∅) → 𝐾 ∈ HL)
4 simpl22 1232 . . . . . 6 (((𝐾 ∈ HL ∧ (𝑋𝐴𝑌𝐴𝑍𝑆) ∧ 𝑋𝑍) ∧ 𝑋 = ∅) → 𝑌𝐴)
5 pmodlem.a . . . . . . 7 𝐴 = (Atoms‘𝐾)
6 pmodlem.p . . . . . . 7 + = (+𝑃𝐾)
75, 6padd02 36393 . . . . . 6 ((𝐾 ∈ HL ∧ 𝑌𝐴) → (∅ + 𝑌) = 𝑌)
83, 4, 7syl2anc 576 . . . . 5 (((𝐾 ∈ HL ∧ (𝑋𝐴𝑌𝐴𝑍𝑆) ∧ 𝑋𝑍) ∧ 𝑋 = ∅) → (∅ + 𝑌) = 𝑌)
92, 8eqtrd 2808 . . . 4 (((𝐾 ∈ HL ∧ (𝑋𝐴𝑌𝐴𝑍𝑆) ∧ 𝑋𝑍) ∧ 𝑋 = ∅) → (𝑋 + 𝑌) = 𝑌)
109ineq1d 4069 . . 3 (((𝐾 ∈ HL ∧ (𝑋𝐴𝑌𝐴𝑍𝑆) ∧ 𝑋𝑍) ∧ 𝑋 = ∅) → ((𝑋 + 𝑌) ∩ 𝑍) = (𝑌𝑍))
11 ssinss1 4095 . . . . 5 (𝑌𝐴 → (𝑌𝑍) ⊆ 𝐴)
124, 11syl 17 . . . 4 (((𝐾 ∈ HL ∧ (𝑋𝐴𝑌𝐴𝑍𝑆) ∧ 𝑋𝑍) ∧ 𝑋 = ∅) → (𝑌𝑍) ⊆ 𝐴)
13 simpl21 1231 . . . 4 (((𝐾 ∈ HL ∧ (𝑋𝐴𝑌𝐴𝑍𝑆) ∧ 𝑋𝑍) ∧ 𝑋 = ∅) → 𝑋𝐴)
145, 6sspadd2 36397 . . . 4 ((𝐾 ∈ HL ∧ (𝑌𝑍) ⊆ 𝐴𝑋𝐴) → (𝑌𝑍) ⊆ (𝑋 + (𝑌𝑍)))
153, 12, 13, 14syl3anc 1351 . . 3 (((𝐾 ∈ HL ∧ (𝑋𝐴𝑌𝐴𝑍𝑆) ∧ 𝑋𝑍) ∧ 𝑋 = ∅) → (𝑌𝑍) ⊆ (𝑋 + (𝑌𝑍)))
1610, 15eqsstrd 3889 . 2 (((𝐾 ∈ HL ∧ (𝑋𝐴𝑌𝐴𝑍𝑆) ∧ 𝑋𝑍) ∧ 𝑋 = ∅) → ((𝑋 + 𝑌) ∩ 𝑍) ⊆ (𝑋 + (𝑌𝑍)))
17 oveq2 6978 . . . . 5 (𝑌 = ∅ → (𝑋 + 𝑌) = (𝑋 + ∅))
18 simp1 1116 . . . . . 6 ((𝐾 ∈ HL ∧ (𝑋𝐴𝑌𝐴𝑍𝑆) ∧ 𝑋𝑍) → 𝐾 ∈ HL)
19 simp21 1186 . . . . . 6 ((𝐾 ∈ HL ∧ (𝑋𝐴𝑌𝐴𝑍𝑆) ∧ 𝑋𝑍) → 𝑋𝐴)
205, 6padd01 36392 . . . . . 6 ((𝐾 ∈ HL ∧ 𝑋𝐴) → (𝑋 + ∅) = 𝑋)
2118, 19, 20syl2anc 576 . . . . 5 ((𝐾 ∈ HL ∧ (𝑋𝐴𝑌𝐴𝑍𝑆) ∧ 𝑋𝑍) → (𝑋 + ∅) = 𝑋)
2217, 21sylan9eqr 2830 . . . 4 (((𝐾 ∈ HL ∧ (𝑋𝐴𝑌𝐴𝑍𝑆) ∧ 𝑋𝑍) ∧ 𝑌 = ∅) → (𝑋 + 𝑌) = 𝑋)
2322ineq1d 4069 . . 3 (((𝐾 ∈ HL ∧ (𝑋𝐴𝑌𝐴𝑍𝑆) ∧ 𝑋𝑍) ∧ 𝑌 = ∅) → ((𝑋 + 𝑌) ∩ 𝑍) = (𝑋𝑍))
24 inss1 4086 . . . 4 (𝑋𝑍) ⊆ 𝑋
25 simpl1 1171 . . . . 5 (((𝐾 ∈ HL ∧ (𝑋𝐴𝑌𝐴𝑍𝑆) ∧ 𝑋𝑍) ∧ 𝑌 = ∅) → 𝐾 ∈ HL)
26 simpl21 1231 . . . . 5 (((𝐾 ∈ HL ∧ (𝑋𝐴𝑌𝐴𝑍𝑆) ∧ 𝑋𝑍) ∧ 𝑌 = ∅) → 𝑋𝐴)
27 simpl22 1232 . . . . . 6 (((𝐾 ∈ HL ∧ (𝑋𝐴𝑌𝐴𝑍𝑆) ∧ 𝑋𝑍) ∧ 𝑌 = ∅) → 𝑌𝐴)
2827, 11syl 17 . . . . 5 (((𝐾 ∈ HL ∧ (𝑋𝐴𝑌𝐴𝑍𝑆) ∧ 𝑋𝑍) ∧ 𝑌 = ∅) → (𝑌𝑍) ⊆ 𝐴)
295, 6sspadd1 36396 . . . . 5 ((𝐾 ∈ HL ∧ 𝑋𝐴 ∧ (𝑌𝑍) ⊆ 𝐴) → 𝑋 ⊆ (𝑋 + (𝑌𝑍)))
3025, 26, 28, 29syl3anc 1351 . . . 4 (((𝐾 ∈ HL ∧ (𝑋𝐴𝑌𝐴𝑍𝑆) ∧ 𝑋𝑍) ∧ 𝑌 = ∅) → 𝑋 ⊆ (𝑋 + (𝑌𝑍)))
3124, 30syl5ss 3863 . . 3 (((𝐾 ∈ HL ∧ (𝑋𝐴𝑌𝐴𝑍𝑆) ∧ 𝑋𝑍) ∧ 𝑌 = ∅) → (𝑋𝑍) ⊆ (𝑋 + (𝑌𝑍)))
3223, 31eqsstrd 3889 . 2 (((𝐾 ∈ HL ∧ (𝑋𝐴𝑌𝐴𝑍𝑆) ∧ 𝑋𝑍) ∧ 𝑌 = ∅) → ((𝑋 + 𝑌) ∩ 𝑍) ⊆ (𝑋 + (𝑌𝑍)))
33 elin 4051 . . . 4 (𝑝 ∈ ((𝑋 + 𝑌) ∩ 𝑍) ↔ (𝑝 ∈ (𝑋 + 𝑌) ∧ 𝑝𝑍))
34 simpl1 1171 . . . . . . . . . 10 (((𝐾 ∈ HL ∧ (𝑋𝐴𝑌𝐴𝑍𝑆) ∧ 𝑋𝑍) ∧ ((𝑋 ≠ ∅ ∧ 𝑌 ≠ ∅) ∧ 𝑝𝑍)) → 𝐾 ∈ HL)
3534hllatd 35945 . . . . . . . . 9 (((𝐾 ∈ HL ∧ (𝑋𝐴𝑌𝐴𝑍𝑆) ∧ 𝑋𝑍) ∧ ((𝑋 ≠ ∅ ∧ 𝑌 ≠ ∅) ∧ 𝑝𝑍)) → 𝐾 ∈ Lat)
36 simpl21 1231 . . . . . . . . 9 (((𝐾 ∈ HL ∧ (𝑋𝐴𝑌𝐴𝑍𝑆) ∧ 𝑋𝑍) ∧ ((𝑋 ≠ ∅ ∧ 𝑌 ≠ ∅) ∧ 𝑝𝑍)) → 𝑋𝐴)
37 simpl22 1232 . . . . . . . . 9 (((𝐾 ∈ HL ∧ (𝑋𝐴𝑌𝐴𝑍𝑆) ∧ 𝑋𝑍) ∧ ((𝑋 ≠ ∅ ∧ 𝑌 ≠ ∅) ∧ 𝑝𝑍)) → 𝑌𝐴)
38 simprl 758 . . . . . . . . 9 (((𝐾 ∈ HL ∧ (𝑋𝐴𝑌𝐴𝑍𝑆) ∧ 𝑋𝑍) ∧ ((𝑋 ≠ ∅ ∧ 𝑌 ≠ ∅) ∧ 𝑝𝑍)) → (𝑋 ≠ ∅ ∧ 𝑌 ≠ ∅))
39 pmodlem.l . . . . . . . . . 10 = (le‘𝐾)
40 pmodlem.j . . . . . . . . . 10 = (join‘𝐾)
4139, 40, 5, 6elpaddn0 36381 . . . . . . . . 9 (((𝐾 ∈ Lat ∧ 𝑋𝐴𝑌𝐴) ∧ (𝑋 ≠ ∅ ∧ 𝑌 ≠ ∅)) → (𝑝 ∈ (𝑋 + 𝑌) ↔ (𝑝𝐴 ∧ ∃𝑞𝑋𝑟𝑌 𝑝 (𝑞 𝑟))))
4235, 36, 37, 38, 41syl31anc 1353 . . . . . . . 8 (((𝐾 ∈ HL ∧ (𝑋𝐴𝑌𝐴𝑍𝑆) ∧ 𝑋𝑍) ∧ ((𝑋 ≠ ∅ ∧ 𝑌 ≠ ∅) ∧ 𝑝𝑍)) → (𝑝 ∈ (𝑋 + 𝑌) ↔ (𝑝𝐴 ∧ ∃𝑞𝑋𝑟𝑌 𝑝 (𝑞 𝑟))))
43 simpl1 1171 . . . . . . . . . . . . . 14 (((𝐾 ∈ HL ∧ (𝑋𝐴𝑌𝐴𝑍𝑆) ∧ 𝑋𝑍) ∧ (𝑝𝑍 ∧ (𝑞𝑋𝑟𝑌) ∧ 𝑝 (𝑞 𝑟))) → 𝐾 ∈ HL)
44 simpl21 1231 . . . . . . . . . . . . . 14 (((𝐾 ∈ HL ∧ (𝑋𝐴𝑌𝐴𝑍𝑆) ∧ 𝑋𝑍) ∧ (𝑝𝑍 ∧ (𝑞𝑋𝑟𝑌) ∧ 𝑝 (𝑞 𝑟))) → 𝑋𝐴)
45 simpl22 1232 . . . . . . . . . . . . . 14 (((𝐾 ∈ HL ∧ (𝑋𝐴𝑌𝐴𝑍𝑆) ∧ 𝑋𝑍) ∧ (𝑝𝑍 ∧ (𝑞𝑋𝑟𝑌) ∧ 𝑝 (𝑞 𝑟))) → 𝑌𝐴)
46 simpl23 1233 . . . . . . . . . . . . . 14 (((𝐾 ∈ HL ∧ (𝑋𝐴𝑌𝐴𝑍𝑆) ∧ 𝑋𝑍) ∧ (𝑝𝑍 ∧ (𝑞𝑋𝑟𝑌) ∧ 𝑝 (𝑞 𝑟))) → 𝑍𝑆)
47 simpl3 1173 . . . . . . . . . . . . . 14 (((𝐾 ∈ HL ∧ (𝑋𝐴𝑌𝐴𝑍𝑆) ∧ 𝑋𝑍) ∧ (𝑝𝑍 ∧ (𝑞𝑋𝑟𝑌) ∧ 𝑝 (𝑞 𝑟))) → 𝑋𝑍)
48 simpr1 1174 . . . . . . . . . . . . . 14 (((𝐾 ∈ HL ∧ (𝑋𝐴𝑌𝐴𝑍𝑆) ∧ 𝑋𝑍) ∧ (𝑝𝑍 ∧ (𝑞𝑋𝑟𝑌) ∧ 𝑝 (𝑞 𝑟))) → 𝑝𝑍)
49 simpr2l 1212 . . . . . . . . . . . . . 14 (((𝐾 ∈ HL ∧ (𝑋𝐴𝑌𝐴𝑍𝑆) ∧ 𝑋𝑍) ∧ (𝑝𝑍 ∧ (𝑞𝑋𝑟𝑌) ∧ 𝑝 (𝑞 𝑟))) → 𝑞𝑋)
50 simpr2r 1213 . . . . . . . . . . . . . 14 (((𝐾 ∈ HL ∧ (𝑋𝐴𝑌𝐴𝑍𝑆) ∧ 𝑋𝑍) ∧ (𝑝𝑍 ∧ (𝑞𝑋𝑟𝑌) ∧ 𝑝 (𝑞 𝑟))) → 𝑟𝑌)
51 simpr3 1176 . . . . . . . . . . . . . 14 (((𝐾 ∈ HL ∧ (𝑋𝐴𝑌𝐴𝑍𝑆) ∧ 𝑋𝑍) ∧ (𝑝𝑍 ∧ (𝑞𝑋𝑟𝑌) ∧ 𝑝 (𝑞 𝑟))) → 𝑝 (𝑞 𝑟))
52 pmodlem.s . . . . . . . . . . . . . . 15 𝑆 = (PSubSp‘𝐾)
5339, 40, 5, 52, 6pmodlem1 36427 . . . . . . . . . . . . . 14 (((𝐾 ∈ HL ∧ 𝑋𝐴𝑌𝐴) ∧ (𝑍𝑆𝑋𝑍𝑝𝑍) ∧ (𝑞𝑋𝑟𝑌𝑝 (𝑞 𝑟))) → 𝑝 ∈ (𝑋 + (𝑌𝑍)))
5443, 44, 45, 46, 47, 48, 49, 50, 51, 53syl333anc 1382 . . . . . . . . . . . . 13 (((𝐾 ∈ HL ∧ (𝑋𝐴𝑌𝐴𝑍𝑆) ∧ 𝑋𝑍) ∧ (𝑝𝑍 ∧ (𝑞𝑋𝑟𝑌) ∧ 𝑝 (𝑞 𝑟))) → 𝑝 ∈ (𝑋 + (𝑌𝑍)))
55543exp2 1334 . . . . . . . . . . . 12 ((𝐾 ∈ HL ∧ (𝑋𝐴𝑌𝐴𝑍𝑆) ∧ 𝑋𝑍) → (𝑝𝑍 → ((𝑞𝑋𝑟𝑌) → (𝑝 (𝑞 𝑟) → 𝑝 ∈ (𝑋 + (𝑌𝑍))))))
5655imp 398 . . . . . . . . . . 11 (((𝐾 ∈ HL ∧ (𝑋𝐴𝑌𝐴𝑍𝑆) ∧ 𝑋𝑍) ∧ 𝑝𝑍) → ((𝑞𝑋𝑟𝑌) → (𝑝 (𝑞 𝑟) → 𝑝 ∈ (𝑋 + (𝑌𝑍)))))
5756rexlimdvv 3232 . . . . . . . . . 10 (((𝐾 ∈ HL ∧ (𝑋𝐴𝑌𝐴𝑍𝑆) ∧ 𝑋𝑍) ∧ 𝑝𝑍) → (∃𝑞𝑋𝑟𝑌 𝑝 (𝑞 𝑟) → 𝑝 ∈ (𝑋 + (𝑌𝑍))))
5857adantld 483 . . . . . . . . 9 (((𝐾 ∈ HL ∧ (𝑋𝐴𝑌𝐴𝑍𝑆) ∧ 𝑋𝑍) ∧ 𝑝𝑍) → ((𝑝𝐴 ∧ ∃𝑞𝑋𝑟𝑌 𝑝 (𝑞 𝑟)) → 𝑝 ∈ (𝑋 + (𝑌𝑍))))
5958adantrl 703 . . . . . . . 8 (((𝐾 ∈ HL ∧ (𝑋𝐴𝑌𝐴𝑍𝑆) ∧ 𝑋𝑍) ∧ ((𝑋 ≠ ∅ ∧ 𝑌 ≠ ∅) ∧ 𝑝𝑍)) → ((𝑝𝐴 ∧ ∃𝑞𝑋𝑟𝑌 𝑝 (𝑞 𝑟)) → 𝑝 ∈ (𝑋 + (𝑌𝑍))))
6042, 59sylbid 232 . . . . . . 7 (((𝐾 ∈ HL ∧ (𝑋𝐴𝑌𝐴𝑍𝑆) ∧ 𝑋𝑍) ∧ ((𝑋 ≠ ∅ ∧ 𝑌 ≠ ∅) ∧ 𝑝𝑍)) → (𝑝 ∈ (𝑋 + 𝑌) → 𝑝 ∈ (𝑋 + (𝑌𝑍))))
6160exp32 413 . . . . . 6 ((𝐾 ∈ HL ∧ (𝑋𝐴𝑌𝐴𝑍𝑆) ∧ 𝑋𝑍) → ((𝑋 ≠ ∅ ∧ 𝑌 ≠ ∅) → (𝑝𝑍 → (𝑝 ∈ (𝑋 + 𝑌) → 𝑝 ∈ (𝑋 + (𝑌𝑍))))))
6261com34 91 . . . . 5 ((𝐾 ∈ HL ∧ (𝑋𝐴𝑌𝐴𝑍𝑆) ∧ 𝑋𝑍) → ((𝑋 ≠ ∅ ∧ 𝑌 ≠ ∅) → (𝑝 ∈ (𝑋 + 𝑌) → (𝑝𝑍𝑝 ∈ (𝑋 + (𝑌𝑍))))))
6362imp4b 414 . . . 4 (((𝐾 ∈ HL ∧ (𝑋𝐴𝑌𝐴𝑍𝑆) ∧ 𝑋𝑍) ∧ (𝑋 ≠ ∅ ∧ 𝑌 ≠ ∅)) → ((𝑝 ∈ (𝑋 + 𝑌) ∧ 𝑝𝑍) → 𝑝 ∈ (𝑋 + (𝑌𝑍))))
6433, 63syl5bi 234 . . 3 (((𝐾 ∈ HL ∧ (𝑋𝐴𝑌𝐴𝑍𝑆) ∧ 𝑋𝑍) ∧ (𝑋 ≠ ∅ ∧ 𝑌 ≠ ∅)) → (𝑝 ∈ ((𝑋 + 𝑌) ∩ 𝑍) → 𝑝 ∈ (𝑋 + (𝑌𝑍))))
6564ssrdv 3858 . 2 (((𝐾 ∈ HL ∧ (𝑋𝐴𝑌𝐴𝑍𝑆) ∧ 𝑋𝑍) ∧ (𝑋 ≠ ∅ ∧ 𝑌 ≠ ∅)) → ((𝑋 + 𝑌) ∩ 𝑍) ⊆ (𝑋 + (𝑌𝑍)))
6616, 32, 65pm2.61da2ne 3050 1 ((𝐾 ∈ HL ∧ (𝑋𝐴𝑌𝐴𝑍𝑆) ∧ 𝑋𝑍) → ((𝑋 + 𝑌) ∩ 𝑍) ⊆ (𝑋 + (𝑌𝑍)))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 198  wa 387  w3a 1068   = wceq 1507  wcel 2050  wne 2961  wrex 3083  cin 3822  wss 3823  c0 4172   class class class wbr 4923  cfv 6182  (class class class)co 6970  lecple 16422  joincjn 17406  Latclat 17507  Atomscatm 35844  HLchlt 35931  PSubSpcpsubsp 36077  +𝑃cpadd 36376
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1758  ax-4 1772  ax-5 1869  ax-6 1928  ax-7 1965  ax-8 2052  ax-9 2059  ax-10 2079  ax-11 2093  ax-12 2106  ax-13 2301  ax-ext 2744  ax-rep 5043  ax-sep 5054  ax-nul 5061  ax-pow 5113  ax-pr 5180  ax-un 7273
This theorem depends on definitions:  df-bi 199  df-an 388  df-or 834  df-3an 1070  df-tru 1510  df-ex 1743  df-nf 1747  df-sb 2016  df-mo 2547  df-eu 2584  df-clab 2753  df-cleq 2765  df-clel 2840  df-nfc 2912  df-ne 2962  df-ral 3087  df-rex 3088  df-reu 3089  df-rab 3091  df-v 3411  df-sbc 3676  df-csb 3781  df-dif 3826  df-un 3828  df-in 3830  df-ss 3837  df-nul 4173  df-if 4345  df-pw 4418  df-sn 4436  df-pr 4438  df-op 4442  df-uni 4707  df-iun 4788  df-br 4924  df-opab 4986  df-mpt 5003  df-id 5306  df-xp 5407  df-rel 5408  df-cnv 5409  df-co 5410  df-dm 5411  df-rn 5412  df-res 5413  df-ima 5414  df-iota 6146  df-fun 6184  df-fn 6185  df-f 6186  df-f1 6187  df-fo 6188  df-f1o 6189  df-fv 6190  df-riota 6931  df-ov 6973  df-oprab 6974  df-mpo 6975  df-1st 7495  df-2nd 7496  df-proset 17390  df-poset 17408  df-plt 17420  df-lub 17436  df-glb 17437  df-join 17438  df-meet 17439  df-p0 17501  df-lat 17508  df-covers 35847  df-ats 35848  df-atl 35879  df-cvlat 35903  df-hlat 35932  df-psubsp 36084  df-padd 36377
This theorem is referenced by:  pmod1i  36429
  Copyright terms: Public domain W3C validator