Step | Hyp | Ref
| Expression |
1 | | dvh4dimat.k |
. . . . 5
⊢ (𝜑 → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻)) |
2 | 1 | simpld 475 |
. . . 4
⊢ (𝜑 → 𝐾 ∈ HL) |
3 | | dvh4dimat.p |
. . . . 5
⊢ (𝜑 → 𝑃 ∈ 𝐴) |
4 | | eqid 2622 |
. . . . . 6
⊢
(Atoms‘𝐾) =
(Atoms‘𝐾) |
5 | | dvh4dimat.h |
. . . . . 6
⊢ 𝐻 = (LHyp‘𝐾) |
6 | | dvh4dimat.u |
. . . . . 6
⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊) |
7 | | eqid 2622 |
. . . . . 6
⊢
((DIsoH‘𝐾)‘𝑊) = ((DIsoH‘𝐾)‘𝑊) |
8 | | dvh4dimat.a |
. . . . . 6
⊢ 𝐴 = (LSAtoms‘𝑈) |
9 | 4, 5, 6, 7, 8 | dihlatat 36626 |
. . . . 5
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝑃 ∈ 𝐴) → (◡((DIsoH‘𝐾)‘𝑊)‘𝑃) ∈ (Atoms‘𝐾)) |
10 | 1, 3, 9 | syl2anc 693 |
. . . 4
⊢ (𝜑 → (◡((DIsoH‘𝐾)‘𝑊)‘𝑃) ∈ (Atoms‘𝐾)) |
11 | | dvh4dimat.q |
. . . . 5
⊢ (𝜑 → 𝑄 ∈ 𝐴) |
12 | 4, 5, 6, 7, 8 | dihlatat 36626 |
. . . . 5
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝑄 ∈ 𝐴) → (◡((DIsoH‘𝐾)‘𝑊)‘𝑄) ∈ (Atoms‘𝐾)) |
13 | 1, 11, 12 | syl2anc 693 |
. . . 4
⊢ (𝜑 → (◡((DIsoH‘𝐾)‘𝑊)‘𝑄) ∈ (Atoms‘𝐾)) |
14 | | dvh4dimat.r |
. . . . 5
⊢ (𝜑 → 𝑅 ∈ 𝐴) |
15 | 4, 5, 6, 7, 8 | dihlatat 36626 |
. . . . 5
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝑅 ∈ 𝐴) → (◡((DIsoH‘𝐾)‘𝑊)‘𝑅) ∈ (Atoms‘𝐾)) |
16 | 1, 14, 15 | syl2anc 693 |
. . . 4
⊢ (𝜑 → (◡((DIsoH‘𝐾)‘𝑊)‘𝑅) ∈ (Atoms‘𝐾)) |
17 | | eqid 2622 |
. . . . 5
⊢
(join‘𝐾) =
(join‘𝐾) |
18 | | eqid 2622 |
. . . . 5
⊢
(le‘𝐾) =
(le‘𝐾) |
19 | 17, 18, 4 | 3dim3 34755 |
. . . 4
⊢ ((𝐾 ∈ HL ∧ ((◡((DIsoH‘𝐾)‘𝑊)‘𝑃) ∈ (Atoms‘𝐾) ∧ (◡((DIsoH‘𝐾)‘𝑊)‘𝑄) ∈ (Atoms‘𝐾) ∧ (◡((DIsoH‘𝐾)‘𝑊)‘𝑅) ∈ (Atoms‘𝐾))) → ∃𝑟 ∈ (Atoms‘𝐾) ¬ 𝑟(le‘𝐾)(((◡((DIsoH‘𝐾)‘𝑊)‘𝑃)(join‘𝐾)(◡((DIsoH‘𝐾)‘𝑊)‘𝑄))(join‘𝐾)(◡((DIsoH‘𝐾)‘𝑊)‘𝑅))) |
20 | 2, 10, 13, 16, 19 | syl13anc 1328 |
. . 3
⊢ (𝜑 → ∃𝑟 ∈ (Atoms‘𝐾) ¬ 𝑟(le‘𝐾)(((◡((DIsoH‘𝐾)‘𝑊)‘𝑃)(join‘𝐾)(◡((DIsoH‘𝐾)‘𝑊)‘𝑄))(join‘𝐾)(◡((DIsoH‘𝐾)‘𝑊)‘𝑅))) |
21 | | dvh4dimat.s |
. . . . . . . . 9
⊢ ⊕ =
(LSSum‘𝑈) |
22 | 1 | adantr 481 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑟 ∈ (Atoms‘𝐾)) → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻)) |
23 | 5, 6, 7, 8 | dih1dimat 36619 |
. . . . . . . . . . . 12
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝑃 ∈ 𝐴) → 𝑃 ∈ ran ((DIsoH‘𝐾)‘𝑊)) |
24 | 1, 3, 23 | syl2anc 693 |
. . . . . . . . . . 11
⊢ (𝜑 → 𝑃 ∈ ran ((DIsoH‘𝐾)‘𝑊)) |
25 | 5, 7, 6, 21, 8, 1,
24, 11 | dihsmatrn 36725 |
. . . . . . . . . 10
⊢ (𝜑 → (𝑃 ⊕ 𝑄) ∈ ran ((DIsoH‘𝐾)‘𝑊)) |
26 | 25 | adantr 481 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑟 ∈ (Atoms‘𝐾)) → (𝑃 ⊕ 𝑄) ∈ ran ((DIsoH‘𝐾)‘𝑊)) |
27 | 14 | adantr 481 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑟 ∈ (Atoms‘𝐾)) → 𝑅 ∈ 𝐴) |
28 | 17, 5, 7, 6, 21, 8,
22, 26, 27 | dihjat4 36722 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑟 ∈ (Atoms‘𝐾)) → ((𝑃 ⊕ 𝑄) ⊕ 𝑅) = (((DIsoH‘𝐾)‘𝑊)‘((◡((DIsoH‘𝐾)‘𝑊)‘(𝑃 ⊕ 𝑄))(join‘𝐾)(◡((DIsoH‘𝐾)‘𝑊)‘𝑅)))) |
29 | 24 | adantr 481 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑟 ∈ (Atoms‘𝐾)) → 𝑃 ∈ ran ((DIsoH‘𝐾)‘𝑊)) |
30 | 11 | adantr 481 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑟 ∈ (Atoms‘𝐾)) → 𝑄 ∈ 𝐴) |
31 | 17, 5, 7, 6, 21, 8,
22, 29, 30 | dihjat6 36723 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑟 ∈ (Atoms‘𝐾)) → (◡((DIsoH‘𝐾)‘𝑊)‘(𝑃 ⊕ 𝑄)) = ((◡((DIsoH‘𝐾)‘𝑊)‘𝑃)(join‘𝐾)(◡((DIsoH‘𝐾)‘𝑊)‘𝑄))) |
32 | 31 | oveq1d 6665 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑟 ∈ (Atoms‘𝐾)) → ((◡((DIsoH‘𝐾)‘𝑊)‘(𝑃 ⊕ 𝑄))(join‘𝐾)(◡((DIsoH‘𝐾)‘𝑊)‘𝑅)) = (((◡((DIsoH‘𝐾)‘𝑊)‘𝑃)(join‘𝐾)(◡((DIsoH‘𝐾)‘𝑊)‘𝑄))(join‘𝐾)(◡((DIsoH‘𝐾)‘𝑊)‘𝑅))) |
33 | 32 | fveq2d 6195 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑟 ∈ (Atoms‘𝐾)) → (((DIsoH‘𝐾)‘𝑊)‘((◡((DIsoH‘𝐾)‘𝑊)‘(𝑃 ⊕ 𝑄))(join‘𝐾)(◡((DIsoH‘𝐾)‘𝑊)‘𝑅))) = (((DIsoH‘𝐾)‘𝑊)‘(((◡((DIsoH‘𝐾)‘𝑊)‘𝑃)(join‘𝐾)(◡((DIsoH‘𝐾)‘𝑊)‘𝑄))(join‘𝐾)(◡((DIsoH‘𝐾)‘𝑊)‘𝑅)))) |
34 | 28, 33 | eqtrd 2656 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑟 ∈ (Atoms‘𝐾)) → ((𝑃 ⊕ 𝑄) ⊕ 𝑅) = (((DIsoH‘𝐾)‘𝑊)‘(((◡((DIsoH‘𝐾)‘𝑊)‘𝑃)(join‘𝐾)(◡((DIsoH‘𝐾)‘𝑊)‘𝑄))(join‘𝐾)(◡((DIsoH‘𝐾)‘𝑊)‘𝑅)))) |
35 | 34 | sseq2d 3633 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑟 ∈ (Atoms‘𝐾)) → ((((DIsoH‘𝐾)‘𝑊)‘𝑟) ⊆ ((𝑃 ⊕ 𝑄) ⊕ 𝑅) ↔ (((DIsoH‘𝐾)‘𝑊)‘𝑟) ⊆ (((DIsoH‘𝐾)‘𝑊)‘(((◡((DIsoH‘𝐾)‘𝑊)‘𝑃)(join‘𝐾)(◡((DIsoH‘𝐾)‘𝑊)‘𝑄))(join‘𝐾)(◡((DIsoH‘𝐾)‘𝑊)‘𝑅))))) |
36 | | eqid 2622 |
. . . . . . . . 9
⊢
(Base‘𝐾) =
(Base‘𝐾) |
37 | 36, 4 | atbase 34576 |
. . . . . . . 8
⊢ (𝑟 ∈ (Atoms‘𝐾) → 𝑟 ∈ (Base‘𝐾)) |
38 | 37 | adantl 482 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑟 ∈ (Atoms‘𝐾)) → 𝑟 ∈ (Base‘𝐾)) |
39 | | hllat 34650 |
. . . . . . . . . 10
⊢ (𝐾 ∈ HL → 𝐾 ∈ Lat) |
40 | 2, 39 | syl 17 |
. . . . . . . . 9
⊢ (𝜑 → 𝐾 ∈ Lat) |
41 | 36, 17, 4 | hlatjcl 34653 |
. . . . . . . . . 10
⊢ ((𝐾 ∈ HL ∧ (◡((DIsoH‘𝐾)‘𝑊)‘𝑃) ∈ (Atoms‘𝐾) ∧ (◡((DIsoH‘𝐾)‘𝑊)‘𝑄) ∈ (Atoms‘𝐾)) → ((◡((DIsoH‘𝐾)‘𝑊)‘𝑃)(join‘𝐾)(◡((DIsoH‘𝐾)‘𝑊)‘𝑄)) ∈ (Base‘𝐾)) |
42 | 2, 10, 13, 41 | syl3anc 1326 |
. . . . . . . . 9
⊢ (𝜑 → ((◡((DIsoH‘𝐾)‘𝑊)‘𝑃)(join‘𝐾)(◡((DIsoH‘𝐾)‘𝑊)‘𝑄)) ∈ (Base‘𝐾)) |
43 | 36, 4 | atbase 34576 |
. . . . . . . . . 10
⊢ ((◡((DIsoH‘𝐾)‘𝑊)‘𝑅) ∈ (Atoms‘𝐾) → (◡((DIsoH‘𝐾)‘𝑊)‘𝑅) ∈ (Base‘𝐾)) |
44 | 16, 43 | syl 17 |
. . . . . . . . 9
⊢ (𝜑 → (◡((DIsoH‘𝐾)‘𝑊)‘𝑅) ∈ (Base‘𝐾)) |
45 | 36, 17 | latjcl 17051 |
. . . . . . . . 9
⊢ ((𝐾 ∈ Lat ∧ ((◡((DIsoH‘𝐾)‘𝑊)‘𝑃)(join‘𝐾)(◡((DIsoH‘𝐾)‘𝑊)‘𝑄)) ∈ (Base‘𝐾) ∧ (◡((DIsoH‘𝐾)‘𝑊)‘𝑅) ∈ (Base‘𝐾)) → (((◡((DIsoH‘𝐾)‘𝑊)‘𝑃)(join‘𝐾)(◡((DIsoH‘𝐾)‘𝑊)‘𝑄))(join‘𝐾)(◡((DIsoH‘𝐾)‘𝑊)‘𝑅)) ∈ (Base‘𝐾)) |
46 | 40, 42, 44, 45 | syl3anc 1326 |
. . . . . . . 8
⊢ (𝜑 → (((◡((DIsoH‘𝐾)‘𝑊)‘𝑃)(join‘𝐾)(◡((DIsoH‘𝐾)‘𝑊)‘𝑄))(join‘𝐾)(◡((DIsoH‘𝐾)‘𝑊)‘𝑅)) ∈ (Base‘𝐾)) |
47 | 46 | adantr 481 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑟 ∈ (Atoms‘𝐾)) → (((◡((DIsoH‘𝐾)‘𝑊)‘𝑃)(join‘𝐾)(◡((DIsoH‘𝐾)‘𝑊)‘𝑄))(join‘𝐾)(◡((DIsoH‘𝐾)‘𝑊)‘𝑅)) ∈ (Base‘𝐾)) |
48 | 36, 18, 5, 7 | dihord 36553 |
. . . . . . 7
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝑟 ∈ (Base‘𝐾) ∧ (((◡((DIsoH‘𝐾)‘𝑊)‘𝑃)(join‘𝐾)(◡((DIsoH‘𝐾)‘𝑊)‘𝑄))(join‘𝐾)(◡((DIsoH‘𝐾)‘𝑊)‘𝑅)) ∈ (Base‘𝐾)) → ((((DIsoH‘𝐾)‘𝑊)‘𝑟) ⊆ (((DIsoH‘𝐾)‘𝑊)‘(((◡((DIsoH‘𝐾)‘𝑊)‘𝑃)(join‘𝐾)(◡((DIsoH‘𝐾)‘𝑊)‘𝑄))(join‘𝐾)(◡((DIsoH‘𝐾)‘𝑊)‘𝑅))) ↔ 𝑟(le‘𝐾)(((◡((DIsoH‘𝐾)‘𝑊)‘𝑃)(join‘𝐾)(◡((DIsoH‘𝐾)‘𝑊)‘𝑄))(join‘𝐾)(◡((DIsoH‘𝐾)‘𝑊)‘𝑅)))) |
49 | 22, 38, 47, 48 | syl3anc 1326 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑟 ∈ (Atoms‘𝐾)) → ((((DIsoH‘𝐾)‘𝑊)‘𝑟) ⊆ (((DIsoH‘𝐾)‘𝑊)‘(((◡((DIsoH‘𝐾)‘𝑊)‘𝑃)(join‘𝐾)(◡((DIsoH‘𝐾)‘𝑊)‘𝑄))(join‘𝐾)(◡((DIsoH‘𝐾)‘𝑊)‘𝑅))) ↔ 𝑟(le‘𝐾)(((◡((DIsoH‘𝐾)‘𝑊)‘𝑃)(join‘𝐾)(◡((DIsoH‘𝐾)‘𝑊)‘𝑄))(join‘𝐾)(◡((DIsoH‘𝐾)‘𝑊)‘𝑅)))) |
50 | 35, 49 | bitr2d 269 |
. . . . 5
⊢ ((𝜑 ∧ 𝑟 ∈ (Atoms‘𝐾)) → (𝑟(le‘𝐾)(((◡((DIsoH‘𝐾)‘𝑊)‘𝑃)(join‘𝐾)(◡((DIsoH‘𝐾)‘𝑊)‘𝑄))(join‘𝐾)(◡((DIsoH‘𝐾)‘𝑊)‘𝑅)) ↔ (((DIsoH‘𝐾)‘𝑊)‘𝑟) ⊆ ((𝑃 ⊕ 𝑄) ⊕ 𝑅))) |
51 | 50 | notbid 308 |
. . . 4
⊢ ((𝜑 ∧ 𝑟 ∈ (Atoms‘𝐾)) → (¬ 𝑟(le‘𝐾)(((◡((DIsoH‘𝐾)‘𝑊)‘𝑃)(join‘𝐾)(◡((DIsoH‘𝐾)‘𝑊)‘𝑄))(join‘𝐾)(◡((DIsoH‘𝐾)‘𝑊)‘𝑅)) ↔ ¬ (((DIsoH‘𝐾)‘𝑊)‘𝑟) ⊆ ((𝑃 ⊕ 𝑄) ⊕ 𝑅))) |
52 | 51 | rexbidva 3049 |
. . 3
⊢ (𝜑 → (∃𝑟 ∈ (Atoms‘𝐾) ¬ 𝑟(le‘𝐾)(((◡((DIsoH‘𝐾)‘𝑊)‘𝑃)(join‘𝐾)(◡((DIsoH‘𝐾)‘𝑊)‘𝑄))(join‘𝐾)(◡((DIsoH‘𝐾)‘𝑊)‘𝑅)) ↔ ∃𝑟 ∈ (Atoms‘𝐾) ¬ (((DIsoH‘𝐾)‘𝑊)‘𝑟) ⊆ ((𝑃 ⊕ 𝑄) ⊕ 𝑅))) |
53 | 20, 52 | mpbid 222 |
. 2
⊢ (𝜑 → ∃𝑟 ∈ (Atoms‘𝐾) ¬ (((DIsoH‘𝐾)‘𝑊)‘𝑟) ⊆ ((𝑃 ⊕ 𝑄) ⊕ 𝑅)) |
54 | 4, 5, 6, 7, 8 | dihatlat 36623 |
. . . 4
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝑟 ∈ (Atoms‘𝐾)) → (((DIsoH‘𝐾)‘𝑊)‘𝑟) ∈ 𝐴) |
55 | 1, 54 | sylan 488 |
. . 3
⊢ ((𝜑 ∧ 𝑟 ∈ (Atoms‘𝐾)) → (((DIsoH‘𝐾)‘𝑊)‘𝑟) ∈ 𝐴) |
56 | 4, 5, 6, 7, 8 | dihlatat 36626 |
. . . . 5
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝑠 ∈ 𝐴) → (◡((DIsoH‘𝐾)‘𝑊)‘𝑠) ∈ (Atoms‘𝐾)) |
57 | 1, 56 | sylan 488 |
. . . 4
⊢ ((𝜑 ∧ 𝑠 ∈ 𝐴) → (◡((DIsoH‘𝐾)‘𝑊)‘𝑠) ∈ (Atoms‘𝐾)) |
58 | 1 | adantr 481 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑠 ∈ 𝐴) → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻)) |
59 | 5, 6, 7, 8 | dih1dimat 36619 |
. . . . . . 7
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝑠 ∈ 𝐴) → 𝑠 ∈ ran ((DIsoH‘𝐾)‘𝑊)) |
60 | 1, 59 | sylan 488 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑠 ∈ 𝐴) → 𝑠 ∈ ran ((DIsoH‘𝐾)‘𝑊)) |
61 | 5, 7 | dihcnvid2 36562 |
. . . . . 6
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝑠 ∈ ran ((DIsoH‘𝐾)‘𝑊)) → (((DIsoH‘𝐾)‘𝑊)‘(◡((DIsoH‘𝐾)‘𝑊)‘𝑠)) = 𝑠) |
62 | 58, 60, 61 | syl2anc 693 |
. . . . 5
⊢ ((𝜑 ∧ 𝑠 ∈ 𝐴) → (((DIsoH‘𝐾)‘𝑊)‘(◡((DIsoH‘𝐾)‘𝑊)‘𝑠)) = 𝑠) |
63 | 62 | eqcomd 2628 |
. . . 4
⊢ ((𝜑 ∧ 𝑠 ∈ 𝐴) → 𝑠 = (((DIsoH‘𝐾)‘𝑊)‘(◡((DIsoH‘𝐾)‘𝑊)‘𝑠))) |
64 | | fveq2 6191 |
. . . . . 6
⊢ (𝑟 = (◡((DIsoH‘𝐾)‘𝑊)‘𝑠) → (((DIsoH‘𝐾)‘𝑊)‘𝑟) = (((DIsoH‘𝐾)‘𝑊)‘(◡((DIsoH‘𝐾)‘𝑊)‘𝑠))) |
65 | 64 | eqeq2d 2632 |
. . . . 5
⊢ (𝑟 = (◡((DIsoH‘𝐾)‘𝑊)‘𝑠) → (𝑠 = (((DIsoH‘𝐾)‘𝑊)‘𝑟) ↔ 𝑠 = (((DIsoH‘𝐾)‘𝑊)‘(◡((DIsoH‘𝐾)‘𝑊)‘𝑠)))) |
66 | 65 | rspcev 3309 |
. . . 4
⊢ (((◡((DIsoH‘𝐾)‘𝑊)‘𝑠) ∈ (Atoms‘𝐾) ∧ 𝑠 = (((DIsoH‘𝐾)‘𝑊)‘(◡((DIsoH‘𝐾)‘𝑊)‘𝑠))) → ∃𝑟 ∈ (Atoms‘𝐾)𝑠 = (((DIsoH‘𝐾)‘𝑊)‘𝑟)) |
67 | 57, 63, 66 | syl2anc 693 |
. . 3
⊢ ((𝜑 ∧ 𝑠 ∈ 𝐴) → ∃𝑟 ∈ (Atoms‘𝐾)𝑠 = (((DIsoH‘𝐾)‘𝑊)‘𝑟)) |
68 | | sseq1 3626 |
. . . . 5
⊢ (𝑠 = (((DIsoH‘𝐾)‘𝑊)‘𝑟) → (𝑠 ⊆ ((𝑃 ⊕ 𝑄) ⊕ 𝑅) ↔ (((DIsoH‘𝐾)‘𝑊)‘𝑟) ⊆ ((𝑃 ⊕ 𝑄) ⊕ 𝑅))) |
69 | 68 | notbid 308 |
. . . 4
⊢ (𝑠 = (((DIsoH‘𝐾)‘𝑊)‘𝑟) → (¬ 𝑠 ⊆ ((𝑃 ⊕ 𝑄) ⊕ 𝑅) ↔ ¬ (((DIsoH‘𝐾)‘𝑊)‘𝑟) ⊆ ((𝑃 ⊕ 𝑄) ⊕ 𝑅))) |
70 | 69 | adantl 482 |
. . 3
⊢ ((𝜑 ∧ 𝑠 = (((DIsoH‘𝐾)‘𝑊)‘𝑟)) → (¬ 𝑠 ⊆ ((𝑃 ⊕ 𝑄) ⊕ 𝑅) ↔ ¬ (((DIsoH‘𝐾)‘𝑊)‘𝑟) ⊆ ((𝑃 ⊕ 𝑄) ⊕ 𝑅))) |
71 | 55, 67, 70 | rexxfrd 4881 |
. 2
⊢ (𝜑 → (∃𝑠 ∈ 𝐴 ¬ 𝑠 ⊆ ((𝑃 ⊕ 𝑄) ⊕ 𝑅) ↔ ∃𝑟 ∈ (Atoms‘𝐾) ¬ (((DIsoH‘𝐾)‘𝑊)‘𝑟) ⊆ ((𝑃 ⊕ 𝑄) ⊕ 𝑅))) |
72 | 53, 71 | mpbird 247 |
1
⊢ (𝜑 → ∃𝑠 ∈ 𝐴 ¬ 𝑠 ⊆ ((𝑃 ⊕ 𝑄) ⊕ 𝑅)) |