Step | Hyp | Ref
| Expression |
1 | | djhcvat42.k |
. . . 4
⊢ (𝜑 → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻)) |
2 | 1 | simpld 498 |
. . 3
⊢ (𝜑 → 𝐾 ∈ HL) |
3 | | djhcvat42.s |
. . . 4
⊢ (𝜑 → 𝑆 ∈ ran 𝐼) |
4 | | eqid 2739 |
. . . . 5
⊢
(Base‘𝐾) =
(Base‘𝐾) |
5 | | djhcvat42.h |
. . . . 5
⊢ 𝐻 = (LHyp‘𝐾) |
6 | | djhcvat42.i |
. . . . 5
⊢ 𝐼 = ((DIsoH‘𝐾)‘𝑊) |
7 | 4, 5, 6 | dihcnvcl 38941 |
. . . 4
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝑆 ∈ ran 𝐼) → (◡𝐼‘𝑆) ∈ (Base‘𝐾)) |
8 | 1, 3, 7 | syl2anc 587 |
. . 3
⊢ (𝜑 → (◡𝐼‘𝑆) ∈ (Base‘𝐾)) |
9 | | djhcvat42.x |
. . . . 5
⊢ (𝜑 → 𝑋 ∈ (𝑉 ∖ { 0 })) |
10 | 9 | eldifad 3865 |
. . . 4
⊢ (𝜑 → 𝑋 ∈ 𝑉) |
11 | | eldifsni 4688 |
. . . . 5
⊢ (𝑋 ∈ (𝑉 ∖ { 0 }) → 𝑋 ≠ 0 ) |
12 | 9, 11 | syl 17 |
. . . 4
⊢ (𝜑 → 𝑋 ≠ 0 ) |
13 | | eqid 2739 |
. . . . 5
⊢
(Atoms‘𝐾) =
(Atoms‘𝐾) |
14 | | djhcvat42.u |
. . . . 5
⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊) |
15 | | djhcvat42.v |
. . . . 5
⊢ 𝑉 = (Base‘𝑈) |
16 | | djhcvat42.o |
. . . . 5
⊢ 0 =
(0g‘𝑈) |
17 | | djhcvat42.n |
. . . . 5
⊢ 𝑁 = (LSpan‘𝑈) |
18 | 13, 5, 14, 15, 16, 17, 6 | dihlspsnat 39003 |
. . . 4
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝑋 ∈ 𝑉 ∧ 𝑋 ≠ 0 ) → (◡𝐼‘(𝑁‘{𝑋})) ∈ (Atoms‘𝐾)) |
19 | 1, 10, 12, 18 | syl3anc 1372 |
. . 3
⊢ (𝜑 → (◡𝐼‘(𝑁‘{𝑋})) ∈ (Atoms‘𝐾)) |
20 | | djhcvat42.y |
. . . . 5
⊢ (𝜑 → 𝑌 ∈ (𝑉 ∖ { 0 })) |
21 | 20 | eldifad 3865 |
. . . 4
⊢ (𝜑 → 𝑌 ∈ 𝑉) |
22 | | eldifsni 4688 |
. . . . 5
⊢ (𝑌 ∈ (𝑉 ∖ { 0 }) → 𝑌 ≠ 0 ) |
23 | 20, 22 | syl 17 |
. . . 4
⊢ (𝜑 → 𝑌 ≠ 0 ) |
24 | 13, 5, 14, 15, 16, 17, 6 | dihlspsnat 39003 |
. . . 4
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝑌 ∈ 𝑉 ∧ 𝑌 ≠ 0 ) → (◡𝐼‘(𝑁‘{𝑌})) ∈ (Atoms‘𝐾)) |
25 | 1, 21, 23, 24 | syl3anc 1372 |
. . 3
⊢ (𝜑 → (◡𝐼‘(𝑁‘{𝑌})) ∈ (Atoms‘𝐾)) |
26 | | eqid 2739 |
. . . 4
⊢
(le‘𝐾) =
(le‘𝐾) |
27 | | eqid 2739 |
. . . 4
⊢
(join‘𝐾) =
(join‘𝐾) |
28 | | eqid 2739 |
. . . 4
⊢
(0.‘𝐾) =
(0.‘𝐾) |
29 | 4, 26, 27, 28, 13 | cvrat42 37114 |
. . 3
⊢ ((𝐾 ∈ HL ∧ ((◡𝐼‘𝑆) ∈ (Base‘𝐾) ∧ (◡𝐼‘(𝑁‘{𝑋})) ∈ (Atoms‘𝐾) ∧ (◡𝐼‘(𝑁‘{𝑌})) ∈ (Atoms‘𝐾))) → (((◡𝐼‘𝑆) ≠ (0.‘𝐾) ∧ (◡𝐼‘(𝑁‘{𝑋}))(le‘𝐾)((◡𝐼‘𝑆)(join‘𝐾)(◡𝐼‘(𝑁‘{𝑌})))) → ∃𝑟 ∈ (Atoms‘𝐾)(𝑟(le‘𝐾)(◡𝐼‘𝑆) ∧ (◡𝐼‘(𝑁‘{𝑋}))(le‘𝐾)(𝑟(join‘𝐾)(◡𝐼‘(𝑁‘{𝑌})))))) |
30 | 2, 8, 19, 25, 29 | syl13anc 1373 |
. 2
⊢ (𝜑 → (((◡𝐼‘𝑆) ≠ (0.‘𝐾) ∧ (◡𝐼‘(𝑁‘{𝑋}))(le‘𝐾)((◡𝐼‘𝑆)(join‘𝐾)(◡𝐼‘(𝑁‘{𝑌})))) → ∃𝑟 ∈ (Atoms‘𝐾)(𝑟(le‘𝐾)(◡𝐼‘𝑆) ∧ (◡𝐼‘(𝑁‘{𝑋}))(le‘𝐾)(𝑟(join‘𝐾)(◡𝐼‘(𝑁‘{𝑌})))))) |
31 | 5, 28, 6, 14, 15, 16, 17, 1, 3 | dih0sb 38955 |
. . . 4
⊢ (𝜑 → (𝑆 = { 0 } ↔ (◡𝐼‘𝑆) = (0.‘𝐾))) |
32 | 31 | necon3bid 2979 |
. . 3
⊢ (𝜑 → (𝑆 ≠ { 0 } ↔ (◡𝐼‘𝑆) ≠ (0.‘𝐾))) |
33 | 5, 14, 15, 17, 6 | dihlsprn 39001 |
. . . . . 6
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝑋 ∈ 𝑉) → (𝑁‘{𝑋}) ∈ ran 𝐼) |
34 | 1, 10, 33 | syl2anc 587 |
. . . . 5
⊢ (𝜑 → (𝑁‘{𝑋}) ∈ ran 𝐼) |
35 | 5, 14, 6, 15 | dihrnss 38948 |
. . . . . . 7
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝑆 ∈ ran 𝐼) → 𝑆 ⊆ 𝑉) |
36 | 1, 3, 35 | syl2anc 587 |
. . . . . 6
⊢ (𝜑 → 𝑆 ⊆ 𝑉) |
37 | 5, 14, 15, 17, 6 | dihlsprn 39001 |
. . . . . . . 8
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝑌 ∈ 𝑉) → (𝑁‘{𝑌}) ∈ ran 𝐼) |
38 | 1, 21, 37 | syl2anc 587 |
. . . . . . 7
⊢ (𝜑 → (𝑁‘{𝑌}) ∈ ran 𝐼) |
39 | 5, 14, 6, 15 | dihrnss 38948 |
. . . . . . 7
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑁‘{𝑌}) ∈ ran 𝐼) → (𝑁‘{𝑌}) ⊆ 𝑉) |
40 | 1, 38, 39 | syl2anc 587 |
. . . . . 6
⊢ (𝜑 → (𝑁‘{𝑌}) ⊆ 𝑉) |
41 | | djhcvat42.j |
. . . . . . 7
⊢ ∨ =
((joinH‘𝐾)‘𝑊) |
42 | 5, 6, 14, 15, 41 | djhcl 39070 |
. . . . . 6
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑆 ⊆ 𝑉 ∧ (𝑁‘{𝑌}) ⊆ 𝑉)) → (𝑆 ∨ (𝑁‘{𝑌})) ∈ ran 𝐼) |
43 | 1, 36, 40, 42 | syl12anc 836 |
. . . . 5
⊢ (𝜑 → (𝑆 ∨ (𝑁‘{𝑌})) ∈ ran 𝐼) |
44 | 26, 5, 6, 1, 34, 43 | dihcnvord 38944 |
. . . 4
⊢ (𝜑 → ((◡𝐼‘(𝑁‘{𝑋}))(le‘𝐾)(◡𝐼‘(𝑆 ∨ (𝑁‘{𝑌}))) ↔ (𝑁‘{𝑋}) ⊆ (𝑆 ∨ (𝑁‘{𝑌})))) |
45 | 27, 5, 6, 41, 1, 3,
38 | djhj 39074 |
. . . . 5
⊢ (𝜑 → (◡𝐼‘(𝑆 ∨ (𝑁‘{𝑌}))) = ((◡𝐼‘𝑆)(join‘𝐾)(◡𝐼‘(𝑁‘{𝑌})))) |
46 | 45 | breq2d 5052 |
. . . 4
⊢ (𝜑 → ((◡𝐼‘(𝑁‘{𝑋}))(le‘𝐾)(◡𝐼‘(𝑆 ∨ (𝑁‘{𝑌}))) ↔ (◡𝐼‘(𝑁‘{𝑋}))(le‘𝐾)((◡𝐼‘𝑆)(join‘𝐾)(◡𝐼‘(𝑁‘{𝑌}))))) |
47 | 44, 46 | bitr3d 284 |
. . 3
⊢ (𝜑 → ((𝑁‘{𝑋}) ⊆ (𝑆 ∨ (𝑁‘{𝑌})) ↔ (◡𝐼‘(𝑁‘{𝑋}))(le‘𝐾)((◡𝐼‘𝑆)(join‘𝐾)(◡𝐼‘(𝑁‘{𝑌}))))) |
48 | 32, 47 | anbi12d 634 |
. 2
⊢ (𝜑 → ((𝑆 ≠ { 0 } ∧ (𝑁‘{𝑋}) ⊆ (𝑆 ∨ (𝑁‘{𝑌}))) ↔ ((◡𝐼‘𝑆) ≠ (0.‘𝐾) ∧ (◡𝐼‘(𝑁‘{𝑋}))(le‘𝐾)((◡𝐼‘𝑆)(join‘𝐾)(◡𝐼‘(𝑁‘{𝑌})))))) |
49 | 1 | adantr 484 |
. . . . 5
⊢ ((𝜑 ∧ 𝑧 ∈ (𝑉 ∖ { 0 })) → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻)) |
50 | | eldifi 4027 |
. . . . . 6
⊢ (𝑧 ∈ (𝑉 ∖ { 0 }) → 𝑧 ∈ 𝑉) |
51 | 50 | adantl 485 |
. . . . 5
⊢ ((𝜑 ∧ 𝑧 ∈ (𝑉 ∖ { 0 })) → 𝑧 ∈ 𝑉) |
52 | | eldifsni 4688 |
. . . . . 6
⊢ (𝑧 ∈ (𝑉 ∖ { 0 }) → 𝑧 ≠ 0 ) |
53 | 52 | adantl 485 |
. . . . 5
⊢ ((𝜑 ∧ 𝑧 ∈ (𝑉 ∖ { 0 })) → 𝑧 ≠ 0 ) |
54 | 13, 5, 14, 15, 16, 17, 6 | dihlspsnat 39003 |
. . . . 5
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝑧 ∈ 𝑉 ∧ 𝑧 ≠ 0 ) → (◡𝐼‘(𝑁‘{𝑧})) ∈ (Atoms‘𝐾)) |
55 | 49, 51, 53, 54 | syl3anc 1372 |
. . . 4
⊢ ((𝜑 ∧ 𝑧 ∈ (𝑉 ∖ { 0 })) → (◡𝐼‘(𝑁‘{𝑧})) ∈ (Atoms‘𝐾)) |
56 | 13, 5, 14, 15, 16, 17, 6, 1 | dihatexv2 39009 |
. . . 4
⊢ (𝜑 → (𝑟 ∈ (Atoms‘𝐾) ↔ ∃𝑧 ∈ (𝑉 ∖ { 0 })𝑟 = (◡𝐼‘(𝑁‘{𝑧})))) |
57 | | breq1 5043 |
. . . . . 6
⊢ (𝑟 = (◡𝐼‘(𝑁‘{𝑧})) → (𝑟(le‘𝐾)(◡𝐼‘𝑆) ↔ (◡𝐼‘(𝑁‘{𝑧}))(le‘𝐾)(◡𝐼‘𝑆))) |
58 | | oveq1 7190 |
. . . . . . 7
⊢ (𝑟 = (◡𝐼‘(𝑁‘{𝑧})) → (𝑟(join‘𝐾)(◡𝐼‘(𝑁‘{𝑌}))) = ((◡𝐼‘(𝑁‘{𝑧}))(join‘𝐾)(◡𝐼‘(𝑁‘{𝑌})))) |
59 | 58 | breq2d 5052 |
. . . . . 6
⊢ (𝑟 = (◡𝐼‘(𝑁‘{𝑧})) → ((◡𝐼‘(𝑁‘{𝑋}))(le‘𝐾)(𝑟(join‘𝐾)(◡𝐼‘(𝑁‘{𝑌}))) ↔ (◡𝐼‘(𝑁‘{𝑋}))(le‘𝐾)((◡𝐼‘(𝑁‘{𝑧}))(join‘𝐾)(◡𝐼‘(𝑁‘{𝑌}))))) |
60 | 57, 59 | anbi12d 634 |
. . . . 5
⊢ (𝑟 = (◡𝐼‘(𝑁‘{𝑧})) → ((𝑟(le‘𝐾)(◡𝐼‘𝑆) ∧ (◡𝐼‘(𝑁‘{𝑋}))(le‘𝐾)(𝑟(join‘𝐾)(◡𝐼‘(𝑁‘{𝑌})))) ↔ ((◡𝐼‘(𝑁‘{𝑧}))(le‘𝐾)(◡𝐼‘𝑆) ∧ (◡𝐼‘(𝑁‘{𝑋}))(le‘𝐾)((◡𝐼‘(𝑁‘{𝑧}))(join‘𝐾)(◡𝐼‘(𝑁‘{𝑌})))))) |
61 | 60 | adantl 485 |
. . . 4
⊢ ((𝜑 ∧ 𝑟 = (◡𝐼‘(𝑁‘{𝑧}))) → ((𝑟(le‘𝐾)(◡𝐼‘𝑆) ∧ (◡𝐼‘(𝑁‘{𝑋}))(le‘𝐾)(𝑟(join‘𝐾)(◡𝐼‘(𝑁‘{𝑌})))) ↔ ((◡𝐼‘(𝑁‘{𝑧}))(le‘𝐾)(◡𝐼‘𝑆) ∧ (◡𝐼‘(𝑁‘{𝑋}))(le‘𝐾)((◡𝐼‘(𝑁‘{𝑧}))(join‘𝐾)(◡𝐼‘(𝑁‘{𝑌})))))) |
62 | 55, 56, 61 | rexxfr2d 5288 |
. . 3
⊢ (𝜑 → (∃𝑟 ∈ (Atoms‘𝐾)(𝑟(le‘𝐾)(◡𝐼‘𝑆) ∧ (◡𝐼‘(𝑁‘{𝑋}))(le‘𝐾)(𝑟(join‘𝐾)(◡𝐼‘(𝑁‘{𝑌})))) ↔ ∃𝑧 ∈ (𝑉 ∖ { 0 })((◡𝐼‘(𝑁‘{𝑧}))(le‘𝐾)(◡𝐼‘𝑆) ∧ (◡𝐼‘(𝑁‘{𝑋}))(le‘𝐾)((◡𝐼‘(𝑁‘{𝑧}))(join‘𝐾)(◡𝐼‘(𝑁‘{𝑌})))))) |
63 | 5, 14, 15, 17, 6 | dihlsprn 39001 |
. . . . . . 7
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝑧 ∈ 𝑉) → (𝑁‘{𝑧}) ∈ ran 𝐼) |
64 | 49, 51, 63 | syl2anc 587 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑧 ∈ (𝑉 ∖ { 0 })) → (𝑁‘{𝑧}) ∈ ran 𝐼) |
65 | 3 | adantr 484 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑧 ∈ (𝑉 ∖ { 0 })) → 𝑆 ∈ ran 𝐼) |
66 | 26, 5, 6, 49, 64, 65 | dihcnvord 38944 |
. . . . 5
⊢ ((𝜑 ∧ 𝑧 ∈ (𝑉 ∖ { 0 })) → ((◡𝐼‘(𝑁‘{𝑧}))(le‘𝐾)(◡𝐼‘𝑆) ↔ (𝑁‘{𝑧}) ⊆ 𝑆)) |
67 | 38 | adantr 484 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑧 ∈ (𝑉 ∖ { 0 })) → (𝑁‘{𝑌}) ∈ ran 𝐼) |
68 | 27, 5, 6, 41, 49, 64, 67 | djhj 39074 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑧 ∈ (𝑉 ∖ { 0 })) → (◡𝐼‘((𝑁‘{𝑧}) ∨ (𝑁‘{𝑌}))) = ((◡𝐼‘(𝑁‘{𝑧}))(join‘𝐾)(◡𝐼‘(𝑁‘{𝑌})))) |
69 | 68 | breq2d 5052 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑧 ∈ (𝑉 ∖ { 0 })) → ((◡𝐼‘(𝑁‘{𝑋}))(le‘𝐾)(◡𝐼‘((𝑁‘{𝑧}) ∨ (𝑁‘{𝑌}))) ↔ (◡𝐼‘(𝑁‘{𝑋}))(le‘𝐾)((◡𝐼‘(𝑁‘{𝑧}))(join‘𝐾)(◡𝐼‘(𝑁‘{𝑌}))))) |
70 | 10 | adantr 484 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑧 ∈ (𝑉 ∖ { 0 })) → 𝑋 ∈ 𝑉) |
71 | 49, 70, 33 | syl2anc 587 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑧 ∈ (𝑉 ∖ { 0 })) → (𝑁‘{𝑋}) ∈ ran 𝐼) |
72 | 5, 14, 6, 15 | dihrnss 38948 |
. . . . . . . . 9
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑁‘{𝑧}) ∈ ran 𝐼) → (𝑁‘{𝑧}) ⊆ 𝑉) |
73 | 49, 64, 72 | syl2anc 587 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑧 ∈ (𝑉 ∖ { 0 })) → (𝑁‘{𝑧}) ⊆ 𝑉) |
74 | 40 | adantr 484 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑧 ∈ (𝑉 ∖ { 0 })) → (𝑁‘{𝑌}) ⊆ 𝑉) |
75 | 5, 6, 14, 15, 41 | djhcl 39070 |
. . . . . . . 8
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ ((𝑁‘{𝑧}) ⊆ 𝑉 ∧ (𝑁‘{𝑌}) ⊆ 𝑉)) → ((𝑁‘{𝑧}) ∨ (𝑁‘{𝑌})) ∈ ran 𝐼) |
76 | 49, 73, 74, 75 | syl12anc 836 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑧 ∈ (𝑉 ∖ { 0 })) → ((𝑁‘{𝑧}) ∨ (𝑁‘{𝑌})) ∈ ran 𝐼) |
77 | 26, 5, 6, 49, 71, 76 | dihcnvord 38944 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑧 ∈ (𝑉 ∖ { 0 })) → ((◡𝐼‘(𝑁‘{𝑋}))(le‘𝐾)(◡𝐼‘((𝑁‘{𝑧}) ∨ (𝑁‘{𝑌}))) ↔ (𝑁‘{𝑋}) ⊆ ((𝑁‘{𝑧}) ∨ (𝑁‘{𝑌})))) |
78 | 69, 77 | bitr3d 284 |
. . . . 5
⊢ ((𝜑 ∧ 𝑧 ∈ (𝑉 ∖ { 0 })) → ((◡𝐼‘(𝑁‘{𝑋}))(le‘𝐾)((◡𝐼‘(𝑁‘{𝑧}))(join‘𝐾)(◡𝐼‘(𝑁‘{𝑌}))) ↔ (𝑁‘{𝑋}) ⊆ ((𝑁‘{𝑧}) ∨ (𝑁‘{𝑌})))) |
79 | 66, 78 | anbi12d 634 |
. . . 4
⊢ ((𝜑 ∧ 𝑧 ∈ (𝑉 ∖ { 0 })) → (((◡𝐼‘(𝑁‘{𝑧}))(le‘𝐾)(◡𝐼‘𝑆) ∧ (◡𝐼‘(𝑁‘{𝑋}))(le‘𝐾)((◡𝐼‘(𝑁‘{𝑧}))(join‘𝐾)(◡𝐼‘(𝑁‘{𝑌})))) ↔ ((𝑁‘{𝑧}) ⊆ 𝑆 ∧ (𝑁‘{𝑋}) ⊆ ((𝑁‘{𝑧}) ∨ (𝑁‘{𝑌}))))) |
80 | 79 | rexbidva 3207 |
. . 3
⊢ (𝜑 → (∃𝑧 ∈ (𝑉 ∖ { 0 })((◡𝐼‘(𝑁‘{𝑧}))(le‘𝐾)(◡𝐼‘𝑆) ∧ (◡𝐼‘(𝑁‘{𝑋}))(le‘𝐾)((◡𝐼‘(𝑁‘{𝑧}))(join‘𝐾)(◡𝐼‘(𝑁‘{𝑌})))) ↔ ∃𝑧 ∈ (𝑉 ∖ { 0 })((𝑁‘{𝑧}) ⊆ 𝑆 ∧ (𝑁‘{𝑋}) ⊆ ((𝑁‘{𝑧}) ∨ (𝑁‘{𝑌}))))) |
81 | 62, 80 | bitr2d 283 |
. 2
⊢ (𝜑 → (∃𝑧 ∈ (𝑉 ∖ { 0 })((𝑁‘{𝑧}) ⊆ 𝑆 ∧ (𝑁‘{𝑋}) ⊆ ((𝑁‘{𝑧}) ∨ (𝑁‘{𝑌}))) ↔ ∃𝑟 ∈ (Atoms‘𝐾)(𝑟(le‘𝐾)(◡𝐼‘𝑆) ∧ (◡𝐼‘(𝑁‘{𝑋}))(le‘𝐾)(𝑟(join‘𝐾)(◡𝐼‘(𝑁‘{𝑌})))))) |
82 | 30, 48, 81 | 3imtr4d 297 |
1
⊢ (𝜑 → ((𝑆 ≠ { 0 } ∧ (𝑁‘{𝑋}) ⊆ (𝑆 ∨ (𝑁‘{𝑌}))) → ∃𝑧 ∈ (𝑉 ∖ { 0 })((𝑁‘{𝑧}) ⊆ 𝑆 ∧ (𝑁‘{𝑋}) ⊆ ((𝑁‘{𝑧}) ∨ (𝑁‘{𝑌}))))) |