Proof of Theorem osumcllem1N
Step | Hyp | Ref
| Expression |
1 | | osumcllem.m |
. . 3
⊢ 𝑀 = (𝑋 + {𝑝}) |
2 | | osumcllem.a |
. . . . . . 7
⊢ 𝐴 = (Atoms‘𝐾) |
3 | | osumcllem.p |
. . . . . . 7
⊢ + =
(+𝑃‘𝐾) |
4 | 2, 3 | sspadd1 37603 |
. . . . . 6
⊢ ((𝐾 ∈ HL ∧ 𝑋 ⊆ 𝐴 ∧ 𝑌 ⊆ 𝐴) → 𝑋 ⊆ (𝑋 + 𝑌)) |
5 | 4 | adantr 484 |
. . . . 5
⊢ (((𝐾 ∈ HL ∧ 𝑋 ⊆ 𝐴 ∧ 𝑌 ⊆ 𝐴) ∧ 𝑝 ∈ 𝑈) → 𝑋 ⊆ (𝑋 + 𝑌)) |
6 | | simpl1 1193 |
. . . . . . 7
⊢ (((𝐾 ∈ HL ∧ 𝑋 ⊆ 𝐴 ∧ 𝑌 ⊆ 𝐴) ∧ 𝑝 ∈ 𝑈) → 𝐾 ∈ HL) |
7 | 2, 3 | paddssat 37602 |
. . . . . . . 8
⊢ ((𝐾 ∈ HL ∧ 𝑋 ⊆ 𝐴 ∧ 𝑌 ⊆ 𝐴) → (𝑋 + 𝑌) ⊆ 𝐴) |
8 | 7 | adantr 484 |
. . . . . . 7
⊢ (((𝐾 ∈ HL ∧ 𝑋 ⊆ 𝐴 ∧ 𝑌 ⊆ 𝐴) ∧ 𝑝 ∈ 𝑈) → (𝑋 + 𝑌) ⊆ 𝐴) |
9 | | osumcllem.o |
. . . . . . . 8
⊢ ⊥ =
(⊥𝑃‘𝐾) |
10 | 2, 9 | 2polssN 37703 |
. . . . . . 7
⊢ ((𝐾 ∈ HL ∧ (𝑋 + 𝑌) ⊆ 𝐴) → (𝑋 + 𝑌) ⊆ ( ⊥ ‘( ⊥
‘(𝑋 + 𝑌)))) |
11 | 6, 8, 10 | syl2anc 587 |
. . . . . 6
⊢ (((𝐾 ∈ HL ∧ 𝑋 ⊆ 𝐴 ∧ 𝑌 ⊆ 𝐴) ∧ 𝑝 ∈ 𝑈) → (𝑋 + 𝑌) ⊆ ( ⊥ ‘( ⊥
‘(𝑋 + 𝑌)))) |
12 | | osumcllem.u |
. . . . . 6
⊢ 𝑈 = ( ⊥ ‘( ⊥
‘(𝑋 + 𝑌))) |
13 | 11, 12 | sseqtrrdi 3969 |
. . . . 5
⊢ (((𝐾 ∈ HL ∧ 𝑋 ⊆ 𝐴 ∧ 𝑌 ⊆ 𝐴) ∧ 𝑝 ∈ 𝑈) → (𝑋 + 𝑌) ⊆ 𝑈) |
14 | 5, 13 | sstrd 3928 |
. . . 4
⊢ (((𝐾 ∈ HL ∧ 𝑋 ⊆ 𝐴 ∧ 𝑌 ⊆ 𝐴) ∧ 𝑝 ∈ 𝑈) → 𝑋 ⊆ 𝑈) |
15 | | simpr 488 |
. . . . 5
⊢ (((𝐾 ∈ HL ∧ 𝑋 ⊆ 𝐴 ∧ 𝑌 ⊆ 𝐴) ∧ 𝑝 ∈ 𝑈) → 𝑝 ∈ 𝑈) |
16 | 15 | snssd 4739 |
. . . 4
⊢ (((𝐾 ∈ HL ∧ 𝑋 ⊆ 𝐴 ∧ 𝑌 ⊆ 𝐴) ∧ 𝑝 ∈ 𝑈) → {𝑝} ⊆ 𝑈) |
17 | | simpl2 1194 |
. . . . 5
⊢ (((𝐾 ∈ HL ∧ 𝑋 ⊆ 𝐴 ∧ 𝑌 ⊆ 𝐴) ∧ 𝑝 ∈ 𝑈) → 𝑋 ⊆ 𝐴) |
18 | 2, 9 | polssatN 37696 |
. . . . . . . . 9
⊢ ((𝐾 ∈ HL ∧ (𝑋 + 𝑌) ⊆ 𝐴) → ( ⊥ ‘(𝑋 + 𝑌)) ⊆ 𝐴) |
19 | 6, 8, 18 | syl2anc 587 |
. . . . . . . 8
⊢ (((𝐾 ∈ HL ∧ 𝑋 ⊆ 𝐴 ∧ 𝑌 ⊆ 𝐴) ∧ 𝑝 ∈ 𝑈) → ( ⊥ ‘(𝑋 + 𝑌)) ⊆ 𝐴) |
20 | 2, 9 | polssatN 37696 |
. . . . . . . 8
⊢ ((𝐾 ∈ HL ∧ ( ⊥
‘(𝑋 + 𝑌)) ⊆ 𝐴) → ( ⊥ ‘( ⊥
‘(𝑋 + 𝑌))) ⊆ 𝐴) |
21 | 6, 19, 20 | syl2anc 587 |
. . . . . . 7
⊢ (((𝐾 ∈ HL ∧ 𝑋 ⊆ 𝐴 ∧ 𝑌 ⊆ 𝐴) ∧ 𝑝 ∈ 𝑈) → ( ⊥ ‘( ⊥
‘(𝑋 + 𝑌))) ⊆ 𝐴) |
22 | 12, 21 | eqsstrid 3966 |
. . . . . 6
⊢ (((𝐾 ∈ HL ∧ 𝑋 ⊆ 𝐴 ∧ 𝑌 ⊆ 𝐴) ∧ 𝑝 ∈ 𝑈) → 𝑈 ⊆ 𝐴) |
23 | 16, 22 | sstrd 3928 |
. . . . 5
⊢ (((𝐾 ∈ HL ∧ 𝑋 ⊆ 𝐴 ∧ 𝑌 ⊆ 𝐴) ∧ 𝑝 ∈ 𝑈) → {𝑝} ⊆ 𝐴) |
24 | | eqid 2739 |
. . . . . . . 8
⊢
(PSubSp‘𝐾) =
(PSubSp‘𝐾) |
25 | 2, 24, 9 | polsubN 37695 |
. . . . . . 7
⊢ ((𝐾 ∈ HL ∧ ( ⊥
‘(𝑋 + 𝑌)) ⊆ 𝐴) → ( ⊥ ‘( ⊥
‘(𝑋 + 𝑌))) ∈ (PSubSp‘𝐾)) |
26 | 6, 19, 25 | syl2anc 587 |
. . . . . 6
⊢ (((𝐾 ∈ HL ∧ 𝑋 ⊆ 𝐴 ∧ 𝑌 ⊆ 𝐴) ∧ 𝑝 ∈ 𝑈) → ( ⊥ ‘( ⊥
‘(𝑋 + 𝑌))) ∈ (PSubSp‘𝐾)) |
27 | 12, 26 | eqeltrid 2844 |
. . . . 5
⊢ (((𝐾 ∈ HL ∧ 𝑋 ⊆ 𝐴 ∧ 𝑌 ⊆ 𝐴) ∧ 𝑝 ∈ 𝑈) → 𝑈 ∈ (PSubSp‘𝐾)) |
28 | 2, 24, 3 | paddss 37633 |
. . . . 5
⊢ ((𝐾 ∈ HL ∧ (𝑋 ⊆ 𝐴 ∧ {𝑝} ⊆ 𝐴 ∧ 𝑈 ∈ (PSubSp‘𝐾))) → ((𝑋 ⊆ 𝑈 ∧ {𝑝} ⊆ 𝑈) ↔ (𝑋 + {𝑝}) ⊆ 𝑈)) |
29 | 6, 17, 23, 27, 28 | syl13anc 1374 |
. . . 4
⊢ (((𝐾 ∈ HL ∧ 𝑋 ⊆ 𝐴 ∧ 𝑌 ⊆ 𝐴) ∧ 𝑝 ∈ 𝑈) → ((𝑋 ⊆ 𝑈 ∧ {𝑝} ⊆ 𝑈) ↔ (𝑋 + {𝑝}) ⊆ 𝑈)) |
30 | 14, 16, 29 | mpbi2and 712 |
. . 3
⊢ (((𝐾 ∈ HL ∧ 𝑋 ⊆ 𝐴 ∧ 𝑌 ⊆ 𝐴) ∧ 𝑝 ∈ 𝑈) → (𝑋 + {𝑝}) ⊆ 𝑈) |
31 | 1, 30 | eqsstrid 3966 |
. 2
⊢ (((𝐾 ∈ HL ∧ 𝑋 ⊆ 𝐴 ∧ 𝑌 ⊆ 𝐴) ∧ 𝑝 ∈ 𝑈) → 𝑀 ⊆ 𝑈) |
32 | | sseqin2 4147 |
. 2
⊢ (𝑀 ⊆ 𝑈 ↔ (𝑈 ∩ 𝑀) = 𝑀) |
33 | 31, 32 | sylib 221 |
1
⊢ (((𝐾 ∈ HL ∧ 𝑋 ⊆ 𝐴 ∧ 𝑌 ⊆ 𝐴) ∧ 𝑝 ∈ 𝑈) → (𝑈 ∩ 𝑀) = 𝑀) |