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

Theorem osumcllem9N 35722
Description: Lemma for osumclN 35725. (Contributed by NM, 24-Mar-2012.) (New usage is discouraged.)
Hypotheses
Ref Expression
osumcllem.l = (le‘𝐾)
osumcllem.j = (join‘𝐾)
osumcllem.a 𝐴 = (Atoms‘𝐾)
osumcllem.p + = (+𝑃𝐾)
osumcllem.o = (⊥𝑃𝐾)
osumcllem.c 𝐶 = (PSubCl‘𝐾)
osumcllem.m 𝑀 = (𝑋 + {𝑝})
osumcllem.u 𝑈 = ( ‘( ‘(𝑋 + 𝑌)))
Assertion
Ref Expression
osumcllem9N (((𝐾 ∈ HL ∧ 𝑋𝐶𝑌𝐶) ∧ (𝑋 ⊆ ( 𝑌) ∧ 𝑋 ≠ ∅ ∧ 𝑝𝑈) ∧ ¬ 𝑝 ∈ (𝑋 + 𝑌)) → 𝑀 = 𝑋)

Proof of Theorem osumcllem9N
StepHypRef Expression
1 inass 3954 . . . . . . 7 ((( 𝑋) ∩ 𝑈) ∩ 𝑀) = (( 𝑋) ∩ (𝑈𝑀))
2 simp11 1222 . . . . . . . . 9 (((𝐾 ∈ HL ∧ 𝑋𝐶𝑌𝐶) ∧ (𝑋 ⊆ ( 𝑌) ∧ 𝑋 ≠ ∅ ∧ 𝑝𝑈) ∧ ¬ 𝑝 ∈ (𝑋 + 𝑌)) → 𝐾 ∈ HL)
3 simp13 1224 . . . . . . . . 9 (((𝐾 ∈ HL ∧ 𝑋𝐶𝑌𝐶) ∧ (𝑋 ⊆ ( 𝑌) ∧ 𝑋 ≠ ∅ ∧ 𝑝𝑈) ∧ ¬ 𝑝 ∈ (𝑋 + 𝑌)) → 𝑌𝐶)
4 simp21 1225 . . . . . . . . 9 (((𝐾 ∈ HL ∧ 𝑋𝐶𝑌𝐶) ∧ (𝑋 ⊆ ( 𝑌) ∧ 𝑋 ≠ ∅ ∧ 𝑝𝑈) ∧ ¬ 𝑝 ∈ (𝑋 + 𝑌)) → 𝑋 ⊆ ( 𝑌))
5 osumcllem.l . . . . . . . . . 10 = (le‘𝐾)
6 osumcllem.j . . . . . . . . . 10 = (join‘𝐾)
7 osumcllem.a . . . . . . . . . 10 𝐴 = (Atoms‘𝐾)
8 osumcllem.p . . . . . . . . . 10 + = (+𝑃𝐾)
9 osumcllem.o . . . . . . . . . 10 = (⊥𝑃𝐾)
10 osumcllem.c . . . . . . . . . 10 𝐶 = (PSubCl‘𝐾)
11 osumcllem.m . . . . . . . . . 10 𝑀 = (𝑋 + {𝑝})
12 osumcllem.u . . . . . . . . . 10 𝑈 = ( ‘( ‘(𝑋 + 𝑌)))
135, 6, 7, 8, 9, 10, 11, 12osumcllem3N 35716 . . . . . . . . 9 ((𝐾 ∈ HL ∧ 𝑌𝐶𝑋 ⊆ ( 𝑌)) → (( 𝑋) ∩ 𝑈) = 𝑌)
142, 3, 4, 13syl3anc 1463 . . . . . . . 8 (((𝐾 ∈ HL ∧ 𝑋𝐶𝑌𝐶) ∧ (𝑋 ⊆ ( 𝑌) ∧ 𝑋 ≠ ∅ ∧ 𝑝𝑈) ∧ ¬ 𝑝 ∈ (𝑋 + 𝑌)) → (( 𝑋) ∩ 𝑈) = 𝑌)
1514ineq1d 3944 . . . . . . 7 (((𝐾 ∈ HL ∧ 𝑋𝐶𝑌𝐶) ∧ (𝑋 ⊆ ( 𝑌) ∧ 𝑋 ≠ ∅ ∧ 𝑝𝑈) ∧ ¬ 𝑝 ∈ (𝑋 + 𝑌)) → ((( 𝑋) ∩ 𝑈) ∩ 𝑀) = (𝑌𝑀))
161, 15syl5eqr 2796 . . . . . 6 (((𝐾 ∈ HL ∧ 𝑋𝐶𝑌𝐶) ∧ (𝑋 ⊆ ( 𝑌) ∧ 𝑋 ≠ ∅ ∧ 𝑝𝑈) ∧ ¬ 𝑝 ∈ (𝑋 + 𝑌)) → (( 𝑋) ∩ (𝑈𝑀)) = (𝑌𝑀))
17 simp12 1223 . . . . . . . 8 (((𝐾 ∈ HL ∧ 𝑋𝐶𝑌𝐶) ∧ (𝑋 ⊆ ( 𝑌) ∧ 𝑋 ≠ ∅ ∧ 𝑝𝑈) ∧ ¬ 𝑝 ∈ (𝑋 + 𝑌)) → 𝑋𝐶)
187, 10psubclssatN 35699 . . . . . . . 8 ((𝐾 ∈ HL ∧ 𝑋𝐶) → 𝑋𝐴)
192, 17, 18syl2anc 696 . . . . . . 7 (((𝐾 ∈ HL ∧ 𝑋𝐶𝑌𝐶) ∧ (𝑋 ⊆ ( 𝑌) ∧ 𝑋 ≠ ∅ ∧ 𝑝𝑈) ∧ ¬ 𝑝 ∈ (𝑋 + 𝑌)) → 𝑋𝐴)
207, 10psubclssatN 35699 . . . . . . . 8 ((𝐾 ∈ HL ∧ 𝑌𝐶) → 𝑌𝐴)
212, 3, 20syl2anc 696 . . . . . . 7 (((𝐾 ∈ HL ∧ 𝑋𝐶𝑌𝐶) ∧ (𝑋 ⊆ ( 𝑌) ∧ 𝑋 ≠ ∅ ∧ 𝑝𝑈) ∧ ¬ 𝑝 ∈ (𝑋 + 𝑌)) → 𝑌𝐴)
22 simp22 1226 . . . . . . 7 (((𝐾 ∈ HL ∧ 𝑋𝐶𝑌𝐶) ∧ (𝑋 ⊆ ( 𝑌) ∧ 𝑋 ≠ ∅ ∧ 𝑝𝑈) ∧ ¬ 𝑝 ∈ (𝑋 + 𝑌)) → 𝑋 ≠ ∅)
237, 8paddssat 35572 . . . . . . . . . . . 12 ((𝐾 ∈ HL ∧ 𝑋𝐴𝑌𝐴) → (𝑋 + 𝑌) ⊆ 𝐴)
242, 19, 21, 23syl3anc 1463 . . . . . . . . . . 11 (((𝐾 ∈ HL ∧ 𝑋𝐶𝑌𝐶) ∧ (𝑋 ⊆ ( 𝑌) ∧ 𝑋 ≠ ∅ ∧ 𝑝𝑈) ∧ ¬ 𝑝 ∈ (𝑋 + 𝑌)) → (𝑋 + 𝑌) ⊆ 𝐴)
257, 9polssatN 35666 . . . . . . . . . . 11 ((𝐾 ∈ HL ∧ (𝑋 + 𝑌) ⊆ 𝐴) → ( ‘(𝑋 + 𝑌)) ⊆ 𝐴)
262, 24, 25syl2anc 696 . . . . . . . . . 10 (((𝐾 ∈ HL ∧ 𝑋𝐶𝑌𝐶) ∧ (𝑋 ⊆ ( 𝑌) ∧ 𝑋 ≠ ∅ ∧ 𝑝𝑈) ∧ ¬ 𝑝 ∈ (𝑋 + 𝑌)) → ( ‘(𝑋 + 𝑌)) ⊆ 𝐴)
277, 9polssatN 35666 . . . . . . . . . 10 ((𝐾 ∈ HL ∧ ( ‘(𝑋 + 𝑌)) ⊆ 𝐴) → ( ‘( ‘(𝑋 + 𝑌))) ⊆ 𝐴)
282, 26, 27syl2anc 696 . . . . . . . . 9 (((𝐾 ∈ HL ∧ 𝑋𝐶𝑌𝐶) ∧ (𝑋 ⊆ ( 𝑌) ∧ 𝑋 ≠ ∅ ∧ 𝑝𝑈) ∧ ¬ 𝑝 ∈ (𝑋 + 𝑌)) → ( ‘( ‘(𝑋 + 𝑌))) ⊆ 𝐴)
2912, 28syl5eqss 3778 . . . . . . . 8 (((𝐾 ∈ HL ∧ 𝑋𝐶𝑌𝐶) ∧ (𝑋 ⊆ ( 𝑌) ∧ 𝑋 ≠ ∅ ∧ 𝑝𝑈) ∧ ¬ 𝑝 ∈ (𝑋 + 𝑌)) → 𝑈𝐴)
30 simp23 1227 . . . . . . . 8 (((𝐾 ∈ HL ∧ 𝑋𝐶𝑌𝐶) ∧ (𝑋 ⊆ ( 𝑌) ∧ 𝑋 ≠ ∅ ∧ 𝑝𝑈) ∧ ¬ 𝑝 ∈ (𝑋 + 𝑌)) → 𝑝𝑈)
3129, 30sseldd 3733 . . . . . . 7 (((𝐾 ∈ HL ∧ 𝑋𝐶𝑌𝐶) ∧ (𝑋 ⊆ ( 𝑌) ∧ 𝑋 ≠ ∅ ∧ 𝑝𝑈) ∧ ¬ 𝑝 ∈ (𝑋 + 𝑌)) → 𝑝𝐴)
32 simp3 1130 . . . . . . 7 (((𝐾 ∈ HL ∧ 𝑋𝐶𝑌𝐶) ∧ (𝑋 ⊆ ( 𝑌) ∧ 𝑋 ≠ ∅ ∧ 𝑝𝑈) ∧ ¬ 𝑝 ∈ (𝑋 + 𝑌)) → ¬ 𝑝 ∈ (𝑋 + 𝑌))
335, 6, 7, 8, 9, 10, 11, 12osumcllem8N 35721 . . . . . . 7 (((𝐾 ∈ HL ∧ 𝑋𝐴𝑌𝐴) ∧ (𝑋 ⊆ ( 𝑌) ∧ 𝑋 ≠ ∅ ∧ 𝑝𝐴) ∧ ¬ 𝑝 ∈ (𝑋 + 𝑌)) → (𝑌𝑀) = ∅)
342, 19, 21, 4, 22, 31, 32, 33syl331anc 1488 . . . . . 6 (((𝐾 ∈ HL ∧ 𝑋𝐶𝑌𝐶) ∧ (𝑋 ⊆ ( 𝑌) ∧ 𝑋 ≠ ∅ ∧ 𝑝𝑈) ∧ ¬ 𝑝 ∈ (𝑋 + 𝑌)) → (𝑌𝑀) = ∅)
3516, 34eqtrd 2782 . . . . 5 (((𝐾 ∈ HL ∧ 𝑋𝐶𝑌𝐶) ∧ (𝑋 ⊆ ( 𝑌) ∧ 𝑋 ≠ ∅ ∧ 𝑝𝑈) ∧ ¬ 𝑝 ∈ (𝑋 + 𝑌)) → (( 𝑋) ∩ (𝑈𝑀)) = ∅)
3635fveq2d 6344 . . . 4 (((𝐾 ∈ HL ∧ 𝑋𝐶𝑌𝐶) ∧ (𝑋 ⊆ ( 𝑌) ∧ 𝑋 ≠ ∅ ∧ 𝑝𝑈) ∧ ¬ 𝑝 ∈ (𝑋 + 𝑌)) → ( ‘(( 𝑋) ∩ (𝑈𝑀))) = ( ‘∅))
377, 9pol0N 35667 . . . . 5 (𝐾 ∈ HL → ( ‘∅) = 𝐴)
382, 37syl 17 . . . 4 (((𝐾 ∈ HL ∧ 𝑋𝐶𝑌𝐶) ∧ (𝑋 ⊆ ( 𝑌) ∧ 𝑋 ≠ ∅ ∧ 𝑝𝑈) ∧ ¬ 𝑝 ∈ (𝑋 + 𝑌)) → ( ‘∅) = 𝐴)
3936, 38eqtrd 2782 . . 3 (((𝐾 ∈ HL ∧ 𝑋𝐶𝑌𝐶) ∧ (𝑋 ⊆ ( 𝑌) ∧ 𝑋 ≠ ∅ ∧ 𝑝𝑈) ∧ ¬ 𝑝 ∈ (𝑋 + 𝑌)) → ( ‘(( 𝑋) ∩ (𝑈𝑀))) = 𝐴)
405, 6, 7, 8, 9, 10, 11, 12osumcllem1N 35714 . . . 4 (((𝐾 ∈ HL ∧ 𝑋𝐴𝑌𝐴) ∧ 𝑝𝑈) → (𝑈𝑀) = 𝑀)
412, 19, 21, 30, 40syl31anc 1466 . . 3 (((𝐾 ∈ HL ∧ 𝑋𝐶𝑌𝐶) ∧ (𝑋 ⊆ ( 𝑌) ∧ 𝑋 ≠ ∅ ∧ 𝑝𝑈) ∧ ¬ 𝑝 ∈ (𝑋 + 𝑌)) → (𝑈𝑀) = 𝑀)
4239, 41ineq12d 3946 . 2 (((𝐾 ∈ HL ∧ 𝑋𝐶𝑌𝐶) ∧ (𝑋 ⊆ ( 𝑌) ∧ 𝑋 ≠ ∅ ∧ 𝑝𝑈) ∧ ¬ 𝑝 ∈ (𝑋 + 𝑌)) → (( ‘(( 𝑋) ∩ (𝑈𝑀))) ∩ (𝑈𝑀)) = (𝐴𝑀))
437, 9, 10polsubclN 35710 . . . . . 6 ((𝐾 ∈ HL ∧ ( ‘(𝑋 + 𝑌)) ⊆ 𝐴) → ( ‘( ‘(𝑋 + 𝑌))) ∈ 𝐶)
442, 26, 43syl2anc 696 . . . . 5 (((𝐾 ∈ HL ∧ 𝑋𝐶𝑌𝐶) ∧ (𝑋 ⊆ ( 𝑌) ∧ 𝑋 ≠ ∅ ∧ 𝑝𝑈) ∧ ¬ 𝑝 ∈ (𝑋 + 𝑌)) → ( ‘( ‘(𝑋 + 𝑌))) ∈ 𝐶)
4512, 44syl5eqel 2831 . . . 4 (((𝐾 ∈ HL ∧ 𝑋𝐶𝑌𝐶) ∧ (𝑋 ⊆ ( 𝑌) ∧ 𝑋 ≠ ∅ ∧ 𝑝𝑈) ∧ ¬ 𝑝 ∈ (𝑋 + 𝑌)) → 𝑈𝐶)
467, 8, 10paddatclN 35707 . . . . . 6 ((𝐾 ∈ HL ∧ 𝑋𝐶𝑝𝐴) → (𝑋 + {𝑝}) ∈ 𝐶)
472, 17, 31, 46syl3anc 1463 . . . . 5 (((𝐾 ∈ HL ∧ 𝑋𝐶𝑌𝐶) ∧ (𝑋 ⊆ ( 𝑌) ∧ 𝑋 ≠ ∅ ∧ 𝑝𝑈) ∧ ¬ 𝑝 ∈ (𝑋 + 𝑌)) → (𝑋 + {𝑝}) ∈ 𝐶)
4811, 47syl5eqel 2831 . . . 4 (((𝐾 ∈ HL ∧ 𝑋𝐶𝑌𝐶) ∧ (𝑋 ⊆ ( 𝑌) ∧ 𝑋 ≠ ∅ ∧ 𝑝𝑈) ∧ ¬ 𝑝 ∈ (𝑋 + 𝑌)) → 𝑀𝐶)
4910psubclinN 35706 . . . 4 ((𝐾 ∈ HL ∧ 𝑈𝐶𝑀𝐶) → (𝑈𝑀) ∈ 𝐶)
502, 45, 48, 49syl3anc 1463 . . 3 (((𝐾 ∈ HL ∧ 𝑋𝐶𝑌𝐶) ∧ (𝑋 ⊆ ( 𝑌) ∧ 𝑋 ≠ ∅ ∧ 𝑝𝑈) ∧ ¬ 𝑝 ∈ (𝑋 + 𝑌)) → (𝑈𝑀) ∈ 𝐶)
515, 6, 7, 8, 9, 10, 11, 12osumcllem2N 35715 . . . 4 (((𝐾 ∈ HL ∧ 𝑋𝐴𝑌𝐴) ∧ 𝑝𝑈) → 𝑋 ⊆ (𝑈𝑀))
522, 19, 21, 30, 51syl31anc 1466 . . 3 (((𝐾 ∈ HL ∧ 𝑋𝐶𝑌𝐶) ∧ (𝑋 ⊆ ( 𝑌) ∧ 𝑋 ≠ ∅ ∧ 𝑝𝑈) ∧ ¬ 𝑝 ∈ (𝑋 + 𝑌)) → 𝑋 ⊆ (𝑈𝑀))
5310, 9poml6N 35713 . . 3 (((𝐾 ∈ HL ∧ 𝑋𝐶 ∧ (𝑈𝑀) ∈ 𝐶) ∧ 𝑋 ⊆ (𝑈𝑀)) → (( ‘(( 𝑋) ∩ (𝑈𝑀))) ∩ (𝑈𝑀)) = 𝑋)
542, 17, 50, 52, 53syl31anc 1466 . 2 (((𝐾 ∈ HL ∧ 𝑋𝐶𝑌𝐶) ∧ (𝑋 ⊆ ( 𝑌) ∧ 𝑋 ≠ ∅ ∧ 𝑝𝑈) ∧ ¬ 𝑝 ∈ (𝑋 + 𝑌)) → (( ‘(( 𝑋) ∩ (𝑈𝑀))) ∩ (𝑈𝑀)) = 𝑋)
5531snssd 4473 . . . . 5 (((𝐾 ∈ HL ∧ 𝑋𝐶𝑌𝐶) ∧ (𝑋 ⊆ ( 𝑌) ∧ 𝑋 ≠ ∅ ∧ 𝑝𝑈) ∧ ¬ 𝑝 ∈ (𝑋 + 𝑌)) → {𝑝} ⊆ 𝐴)
567, 8paddssat 35572 . . . . 5 ((𝐾 ∈ HL ∧ 𝑋𝐴 ∧ {𝑝} ⊆ 𝐴) → (𝑋 + {𝑝}) ⊆ 𝐴)
572, 19, 55, 56syl3anc 1463 . . . 4 (((𝐾 ∈ HL ∧ 𝑋𝐶𝑌𝐶) ∧ (𝑋 ⊆ ( 𝑌) ∧ 𝑋 ≠ ∅ ∧ 𝑝𝑈) ∧ ¬ 𝑝 ∈ (𝑋 + 𝑌)) → (𝑋 + {𝑝}) ⊆ 𝐴)
5811, 57syl5eqss 3778 . . 3 (((𝐾 ∈ HL ∧ 𝑋𝐶𝑌𝐶) ∧ (𝑋 ⊆ ( 𝑌) ∧ 𝑋 ≠ ∅ ∧ 𝑝𝑈) ∧ ¬ 𝑝 ∈ (𝑋 + 𝑌)) → 𝑀𝐴)
59 sseqin2 3948 . . 3 (𝑀𝐴 ↔ (𝐴𝑀) = 𝑀)
6058, 59sylib 208 . 2 (((𝐾 ∈ HL ∧ 𝑋𝐶𝑌𝐶) ∧ (𝑋 ⊆ ( 𝑌) ∧ 𝑋 ≠ ∅ ∧ 𝑝𝑈) ∧ ¬ 𝑝 ∈ (𝑋 + 𝑌)) → (𝐴𝑀) = 𝑀)
6142, 54, 603eqtr3rd 2791 1 (((𝐾 ∈ HL ∧ 𝑋𝐶𝑌𝐶) ∧ (𝑋 ⊆ ( 𝑌) ∧ 𝑋 ≠ ∅ ∧ 𝑝𝑈) ∧ ¬ 𝑝 ∈ (𝑋 + 𝑌)) → 𝑀 = 𝑋)
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  w3a 1072   = wceq 1620  wcel 2127  wne 2920  cin 3702  wss 3703  c0 4046  {csn 4309  cfv 6037  (class class class)co 6801  lecple 16121  joincjn 17116  Atomscatm 35022  HLchlt 35109  +𝑃cpadd 35553  𝑃cpolN 35660  PSubClcpscN 35692
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1859  ax-4 1874  ax-5 1976  ax-6 2042  ax-7 2078  ax-8 2129  ax-9 2136  ax-10 2156  ax-11 2171  ax-12 2184  ax-13 2379  ax-ext 2728  ax-rep 4911  ax-sep 4921  ax-nul 4929  ax-pow 4980  ax-pr 5043  ax-un 7102  ax-riotaBAD 34711
This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-3an 1074  df-tru 1623  df-ex 1842  df-nf 1847  df-sb 2035  df-eu 2599  df-mo 2600  df-clab 2735  df-cleq 2741  df-clel 2744  df-nfc 2879  df-ne 2921  df-nel 3024  df-ral 3043  df-rex 3044  df-reu 3045  df-rmo 3046  df-rab 3047  df-v 3330  df-sbc 3565  df-csb 3663  df-dif 3706  df-un 3708  df-in 3710  df-ss 3717  df-nul 4047  df-if 4219  df-pw 4292  df-sn 4310  df-pr 4312  df-op 4316  df-uni 4577  df-iun 4662  df-iin 4663  df-br 4793  df-opab 4853  df-mpt 4870  df-id 5162  df-xp 5260  df-rel 5261  df-cnv 5262  df-co 5263  df-dm 5264  df-rn 5265  df-res 5266  df-ima 5267  df-iota 6000  df-fun 6039  df-fn 6040  df-f 6041  df-f1 6042  df-fo 6043  df-f1o 6044  df-fv 6045  df-riota 6762  df-ov 6804  df-oprab 6805  df-mpt2 6806  df-1st 7321  df-2nd 7322  df-undef 7556  df-preset 17100  df-poset 17118  df-plt 17130  df-lub 17146  df-glb 17147  df-join 17148  df-meet 17149  df-p0 17211  df-p1 17212  df-lat 17218  df-clat 17280  df-oposet 34935  df-ol 34937  df-oml 34938  df-covers 35025  df-ats 35026  df-atl 35057  df-cvlat 35081  df-hlat 35110  df-psubsp 35261  df-pmap 35262  df-padd 35554  df-polarityN 35661  df-psubclN 35693
This theorem is referenced by:  osumcllem11N  35724
  Copyright terms: Public domain W3C validator