Proof of Theorem osumclN
Step | Hyp | Ref
| Expression |
1 | | simpl1 1057 |
. . 3
⊢ (((𝐾 ∈ HL ∧ 𝑋 ∈ 𝐶 ∧ 𝑌 ∈ 𝐶) ∧ 𝑋 ⊆ ( ⊥ ‘𝑌)) → 𝐾 ∈ HL) |
2 | | simpl2 1058 |
. . . 4
⊢ (((𝐾 ∈ HL ∧ 𝑋 ∈ 𝐶 ∧ 𝑌 ∈ 𝐶) ∧ 𝑋 ⊆ ( ⊥ ‘𝑌)) → 𝑋 ∈ 𝐶) |
3 | | eqid 2610 |
. . . . 5
⊢
(Atoms‘𝐾) =
(Atoms‘𝐾) |
4 | | osumcl.c |
. . . . 5
⊢ 𝐶 = (PSubCl‘𝐾) |
5 | 3, 4 | psubclssatN 34245 |
. . . 4
⊢ ((𝐾 ∈ HL ∧ 𝑋 ∈ 𝐶) → 𝑋 ⊆ (Atoms‘𝐾)) |
6 | 1, 2, 5 | syl2anc 691 |
. . 3
⊢ (((𝐾 ∈ HL ∧ 𝑋 ∈ 𝐶 ∧ 𝑌 ∈ 𝐶) ∧ 𝑋 ⊆ ( ⊥ ‘𝑌)) → 𝑋 ⊆ (Atoms‘𝐾)) |
7 | | simpl3 1059 |
. . . 4
⊢ (((𝐾 ∈ HL ∧ 𝑋 ∈ 𝐶 ∧ 𝑌 ∈ 𝐶) ∧ 𝑋 ⊆ ( ⊥ ‘𝑌)) → 𝑌 ∈ 𝐶) |
8 | 3, 4 | psubclssatN 34245 |
. . . 4
⊢ ((𝐾 ∈ HL ∧ 𝑌 ∈ 𝐶) → 𝑌 ⊆ (Atoms‘𝐾)) |
9 | 1, 7, 8 | syl2anc 691 |
. . 3
⊢ (((𝐾 ∈ HL ∧ 𝑋 ∈ 𝐶 ∧ 𝑌 ∈ 𝐶) ∧ 𝑋 ⊆ ( ⊥ ‘𝑌)) → 𝑌 ⊆ (Atoms‘𝐾)) |
10 | | osumcl.p |
. . . 4
⊢ + =
(+𝑃‘𝐾) |
11 | 3, 10 | paddssat 34118 |
. . 3
⊢ ((𝐾 ∈ HL ∧ 𝑋 ⊆ (Atoms‘𝐾) ∧ 𝑌 ⊆ (Atoms‘𝐾)) → (𝑋 + 𝑌) ⊆ (Atoms‘𝐾)) |
12 | 1, 6, 9, 11 | syl3anc 1318 |
. 2
⊢ (((𝐾 ∈ HL ∧ 𝑋 ∈ 𝐶 ∧ 𝑌 ∈ 𝐶) ∧ 𝑋 ⊆ ( ⊥ ‘𝑌)) → (𝑋 + 𝑌) ⊆ (Atoms‘𝐾)) |
13 | | simpll1 1093 |
. . . 4
⊢ ((((𝐾 ∈ HL ∧ 𝑋 ∈ 𝐶 ∧ 𝑌 ∈ 𝐶) ∧ 𝑋 ⊆ ( ⊥ ‘𝑌)) ∧ 𝑋 = ∅) → 𝐾 ∈ HL) |
14 | | oveq1 6556 |
. . . . . 6
⊢ (𝑋 = ∅ → (𝑋 + 𝑌) = (∅ + 𝑌)) |
15 | 3, 10 | padd02 34116 |
. . . . . . 7
⊢ ((𝐾 ∈ HL ∧ 𝑌 ⊆ (Atoms‘𝐾)) → (∅ + 𝑌) = 𝑌) |
16 | 1, 9, 15 | syl2anc 691 |
. . . . . 6
⊢ (((𝐾 ∈ HL ∧ 𝑋 ∈ 𝐶 ∧ 𝑌 ∈ 𝐶) ∧ 𝑋 ⊆ ( ⊥ ‘𝑌)) → (∅ + 𝑌) = 𝑌) |
17 | 14, 16 | sylan9eqr 2666 |
. . . . 5
⊢ ((((𝐾 ∈ HL ∧ 𝑋 ∈ 𝐶 ∧ 𝑌 ∈ 𝐶) ∧ 𝑋 ⊆ ( ⊥ ‘𝑌)) ∧ 𝑋 = ∅) → (𝑋 + 𝑌) = 𝑌) |
18 | | simpll3 1095 |
. . . . 5
⊢ ((((𝐾 ∈ HL ∧ 𝑋 ∈ 𝐶 ∧ 𝑌 ∈ 𝐶) ∧ 𝑋 ⊆ ( ⊥ ‘𝑌)) ∧ 𝑋 = ∅) → 𝑌 ∈ 𝐶) |
19 | 17, 18 | eqeltrd 2688 |
. . . 4
⊢ ((((𝐾 ∈ HL ∧ 𝑋 ∈ 𝐶 ∧ 𝑌 ∈ 𝐶) ∧ 𝑋 ⊆ ( ⊥ ‘𝑌)) ∧ 𝑋 = ∅) → (𝑋 + 𝑌) ∈ 𝐶) |
20 | | osumcl.o |
. . . . 5
⊢ ⊥ =
(⊥𝑃‘𝐾) |
21 | 20, 4 | psubcli2N 34243 |
. . . 4
⊢ ((𝐾 ∈ HL ∧ (𝑋 + 𝑌) ∈ 𝐶) → ( ⊥ ‘( ⊥
‘(𝑋 + 𝑌))) = (𝑋 + 𝑌)) |
22 | 13, 19, 21 | syl2anc 691 |
. . 3
⊢ ((((𝐾 ∈ HL ∧ 𝑋 ∈ 𝐶 ∧ 𝑌 ∈ 𝐶) ∧ 𝑋 ⊆ ( ⊥ ‘𝑌)) ∧ 𝑋 = ∅) → ( ⊥ ‘( ⊥
‘(𝑋 + 𝑌))) = (𝑋 + 𝑌)) |
23 | 10, 20, 4 | osumcllem11N 34270 |
. . . . 5
⊢ (((𝐾 ∈ HL ∧ 𝑋 ∈ 𝐶 ∧ 𝑌 ∈ 𝐶) ∧ (𝑋 ⊆ ( ⊥ ‘𝑌) ∧ 𝑋 ≠ ∅)) → (𝑋 + 𝑌) = ( ⊥ ‘( ⊥
‘(𝑋 + 𝑌)))) |
24 | 23 | anassrs 678 |
. . . 4
⊢ ((((𝐾 ∈ HL ∧ 𝑋 ∈ 𝐶 ∧ 𝑌 ∈ 𝐶) ∧ 𝑋 ⊆ ( ⊥ ‘𝑌)) ∧ 𝑋 ≠ ∅) → (𝑋 + 𝑌) = ( ⊥ ‘( ⊥
‘(𝑋 + 𝑌)))) |
25 | 24 | eqcomd 2616 |
. . 3
⊢ ((((𝐾 ∈ HL ∧ 𝑋 ∈ 𝐶 ∧ 𝑌 ∈ 𝐶) ∧ 𝑋 ⊆ ( ⊥ ‘𝑌)) ∧ 𝑋 ≠ ∅) → ( ⊥ ‘( ⊥
‘(𝑋 + 𝑌))) = (𝑋 + 𝑌)) |
26 | 22, 25 | pm2.61dane 2869 |
. 2
⊢ (((𝐾 ∈ HL ∧ 𝑋 ∈ 𝐶 ∧ 𝑌 ∈ 𝐶) ∧ 𝑋 ⊆ ( ⊥ ‘𝑌)) → ( ⊥ ‘( ⊥
‘(𝑋 + 𝑌))) = (𝑋 + 𝑌)) |
27 | 3, 20, 4 | ispsubclN 34241 |
. . 3
⊢ (𝐾 ∈ HL → ((𝑋 + 𝑌) ∈ 𝐶 ↔ ((𝑋 + 𝑌) ⊆ (Atoms‘𝐾) ∧ ( ⊥ ‘( ⊥
‘(𝑋 + 𝑌))) = (𝑋 + 𝑌)))) |
28 | 1, 27 | syl 17 |
. 2
⊢ (((𝐾 ∈ HL ∧ 𝑋 ∈ 𝐶 ∧ 𝑌 ∈ 𝐶) ∧ 𝑋 ⊆ ( ⊥ ‘𝑌)) → ((𝑋 + 𝑌) ∈ 𝐶 ↔ ((𝑋 + 𝑌) ⊆ (Atoms‘𝐾) ∧ ( ⊥ ‘( ⊥
‘(𝑋 + 𝑌))) = (𝑋 + 𝑌)))) |
29 | 12, 26, 28 | mpbir2and 959 |
1
⊢ (((𝐾 ∈ HL ∧ 𝑋 ∈ 𝐶 ∧ 𝑌 ∈ 𝐶) ∧ 𝑋 ⊆ ( ⊥ ‘𝑌)) → (𝑋 + 𝑌) ∈ 𝐶) |