Step | Hyp | Ref
| Expression |
1 | | eqid 2759 |
. . . . 5
⊢
(LSubSp‘𝑈) =
(LSubSp‘𝑈) |
2 | | dvh3dim.n |
. . . . 5
⊢ 𝑁 = (LSpan‘𝑈) |
3 | | dvh3dim.h |
. . . . . . 7
⊢ 𝐻 = (LHyp‘𝐾) |
4 | | dvh3dim.u |
. . . . . . 7
⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊) |
5 | | dvh3dim.k |
. . . . . . 7
⊢ (𝜑 → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻)) |
6 | 3, 4, 5 | dvhlmod 38671 |
. . . . . 6
⊢ (𝜑 → 𝑈 ∈ LMod) |
7 | 6 | adantr 485 |
. . . . 5
⊢ ((𝜑 ∧ 𝑌 ∈ (𝑁‘{𝑍, 𝑇})) → 𝑈 ∈ LMod) |
8 | | dvh3dim.v |
. . . . . . 7
⊢ 𝑉 = (Base‘𝑈) |
9 | | dvh3dim2.z |
. . . . . . 7
⊢ (𝜑 → 𝑍 ∈ 𝑉) |
10 | | dvh3dim3.t |
. . . . . . 7
⊢ (𝜑 → 𝑇 ∈ 𝑉) |
11 | 8, 1, 2, 6, 9, 10 | lspprcl 19803 |
. . . . . 6
⊢ (𝜑 → (𝑁‘{𝑍, 𝑇}) ∈ (LSubSp‘𝑈)) |
12 | 11 | adantr 485 |
. . . . 5
⊢ ((𝜑 ∧ 𝑌 ∈ (𝑁‘{𝑍, 𝑇})) → (𝑁‘{𝑍, 𝑇}) ∈ (LSubSp‘𝑈)) |
13 | | simpr 489 |
. . . . 5
⊢ ((𝜑 ∧ 𝑌 ∈ (𝑁‘{𝑍, 𝑇})) → 𝑌 ∈ (𝑁‘{𝑍, 𝑇})) |
14 | 8, 2, 6, 9, 10 | lspprid2 19823 |
. . . . . 6
⊢ (𝜑 → 𝑇 ∈ (𝑁‘{𝑍, 𝑇})) |
15 | 14 | adantr 485 |
. . . . 5
⊢ ((𝜑 ∧ 𝑌 ∈ (𝑁‘{𝑍, 𝑇})) → 𝑇 ∈ (𝑁‘{𝑍, 𝑇})) |
16 | 1, 2, 7, 12, 13, 15 | lspprss 19817 |
. . . 4
⊢ ((𝜑 ∧ 𝑌 ∈ (𝑁‘{𝑍, 𝑇})) → (𝑁‘{𝑌, 𝑇}) ⊆ (𝑁‘{𝑍, 𝑇})) |
17 | | sspss 4001 |
. . . 4
⊢ ((𝑁‘{𝑌, 𝑇}) ⊆ (𝑁‘{𝑍, 𝑇}) ↔ ((𝑁‘{𝑌, 𝑇}) ⊊ (𝑁‘{𝑍, 𝑇}) ∨ (𝑁‘{𝑌, 𝑇}) = (𝑁‘{𝑍, 𝑇}))) |
18 | 16, 17 | sylib 221 |
. . 3
⊢ ((𝜑 ∧ 𝑌 ∈ (𝑁‘{𝑍, 𝑇})) → ((𝑁‘{𝑌, 𝑇}) ⊊ (𝑁‘{𝑍, 𝑇}) ∨ (𝑁‘{𝑌, 𝑇}) = (𝑁‘{𝑍, 𝑇}))) |
19 | 3, 4, 5 | dvhlvec 38670 |
. . . . . . 7
⊢ (𝜑 → 𝑈 ∈ LVec) |
20 | 19 | adantr 485 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑁‘{𝑌, 𝑇}) ⊊ (𝑁‘{𝑍, 𝑇})) → 𝑈 ∈ LVec) |
21 | | dvh3dim.y |
. . . . . . . 8
⊢ (𝜑 → 𝑌 ∈ 𝑉) |
22 | 8, 1, 2, 6, 21, 10 | lspprcl 19803 |
. . . . . . 7
⊢ (𝜑 → (𝑁‘{𝑌, 𝑇}) ∈ (LSubSp‘𝑈)) |
23 | 22 | adantr 485 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑁‘{𝑌, 𝑇}) ⊊ (𝑁‘{𝑍, 𝑇})) → (𝑁‘{𝑌, 𝑇}) ∈ (LSubSp‘𝑈)) |
24 | 9 | adantr 485 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑁‘{𝑌, 𝑇}) ⊊ (𝑁‘{𝑍, 𝑇})) → 𝑍 ∈ 𝑉) |
25 | 10 | adantr 485 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑁‘{𝑌, 𝑇}) ⊊ (𝑁‘{𝑍, 𝑇})) → 𝑇 ∈ 𝑉) |
26 | | simpr 489 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑁‘{𝑌, 𝑇}) ⊊ (𝑁‘{𝑍, 𝑇})) → (𝑁‘{𝑌, 𝑇}) ⊊ (𝑁‘{𝑍, 𝑇})) |
27 | 8, 1, 2, 20, 23, 24, 25, 26 | lspprat 19978 |
. . . . 5
⊢ ((𝜑 ∧ (𝑁‘{𝑌, 𝑇}) ⊊ (𝑁‘{𝑍, 𝑇})) → ∃𝑤 ∈ 𝑉 (𝑁‘{𝑌, 𝑇}) = (𝑁‘{𝑤})) |
28 | 5 | 3ad2ant1 1131 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑤 ∈ 𝑉 ∧ (𝑁‘{𝑌, 𝑇}) = (𝑁‘{𝑤})) → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻)) |
29 | | simp2 1135 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑤 ∈ 𝑉 ∧ (𝑁‘{𝑌, 𝑇}) = (𝑁‘{𝑤})) → 𝑤 ∈ 𝑉) |
30 | | dvh3dim.x |
. . . . . . . . . 10
⊢ (𝜑 → 𝑋 ∈ 𝑉) |
31 | 30 | 3ad2ant1 1131 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑤 ∈ 𝑉 ∧ (𝑁‘{𝑌, 𝑇}) = (𝑁‘{𝑤})) → 𝑋 ∈ 𝑉) |
32 | 9 | 3ad2ant1 1131 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑤 ∈ 𝑉 ∧ (𝑁‘{𝑌, 𝑇}) = (𝑁‘{𝑤})) → 𝑍 ∈ 𝑉) |
33 | 3, 4, 8, 2, 28, 29, 31, 32 | dvh3dim2 39009 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑤 ∈ 𝑉 ∧ (𝑁‘{𝑌, 𝑇}) = (𝑁‘{𝑤})) → ∃𝑧 ∈ 𝑉 (¬ 𝑧 ∈ (𝑁‘{𝑤, 𝑋}) ∧ ¬ 𝑧 ∈ (𝑁‘{𝑤, 𝑍}))) |
34 | 6 | 3ad2ant1 1131 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑤 ∈ 𝑉 ∧ (𝑁‘{𝑌, 𝑇}) = (𝑁‘{𝑤})) → 𝑈 ∈ LMod) |
35 | 1 | lsssssubg 19783 |
. . . . . . . . . . . . . . 15
⊢ (𝑈 ∈ LMod →
(LSubSp‘𝑈) ⊆
(SubGrp‘𝑈)) |
36 | 34, 35 | syl 17 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑤 ∈ 𝑉 ∧ (𝑁‘{𝑌, 𝑇}) = (𝑁‘{𝑤})) → (LSubSp‘𝑈) ⊆ (SubGrp‘𝑈)) |
37 | 8, 1, 2 | lspsncl 19802 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑈 ∈ LMod ∧ 𝑋 ∈ 𝑉) → (𝑁‘{𝑋}) ∈ (LSubSp‘𝑈)) |
38 | 6, 30, 37 | syl2anc 588 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → (𝑁‘{𝑋}) ∈ (LSubSp‘𝑈)) |
39 | 38 | 3ad2ant1 1131 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑤 ∈ 𝑉 ∧ (𝑁‘{𝑌, 𝑇}) = (𝑁‘{𝑤})) → (𝑁‘{𝑋}) ∈ (LSubSp‘𝑈)) |
40 | 36, 39 | sseldd 3889 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑤 ∈ 𝑉 ∧ (𝑁‘{𝑌, 𝑇}) = (𝑁‘{𝑤})) → (𝑁‘{𝑋}) ∈ (SubGrp‘𝑈)) |
41 | 8, 1, 2 | lspsncl 19802 |
. . . . . . . . . . . . . . 15
⊢ ((𝑈 ∈ LMod ∧ 𝑤 ∈ 𝑉) → (𝑁‘{𝑤}) ∈ (LSubSp‘𝑈)) |
42 | 34, 29, 41 | syl2anc 588 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑤 ∈ 𝑉 ∧ (𝑁‘{𝑌, 𝑇}) = (𝑁‘{𝑤})) → (𝑁‘{𝑤}) ∈ (LSubSp‘𝑈)) |
43 | 36, 42 | sseldd 3889 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑤 ∈ 𝑉 ∧ (𝑁‘{𝑌, 𝑇}) = (𝑁‘{𝑤})) → (𝑁‘{𝑤}) ∈ (SubGrp‘𝑈)) |
44 | | prssi 4704 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑌 ∈ 𝑉 ∧ 𝑇 ∈ 𝑉) → {𝑌, 𝑇} ⊆ 𝑉) |
45 | 21, 10, 44 | syl2anc 588 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → {𝑌, 𝑇} ⊆ 𝑉) |
46 | | snsspr1 4697 |
. . . . . . . . . . . . . . . . 17
⊢ {𝑌} ⊆ {𝑌, 𝑇} |
47 | 46 | a1i 11 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → {𝑌} ⊆ {𝑌, 𝑇}) |
48 | 8, 2 | lspss 19809 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑈 ∈ LMod ∧ {𝑌, 𝑇} ⊆ 𝑉 ∧ {𝑌} ⊆ {𝑌, 𝑇}) → (𝑁‘{𝑌}) ⊆ (𝑁‘{𝑌, 𝑇})) |
49 | 6, 45, 47, 48 | syl3anc 1369 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → (𝑁‘{𝑌}) ⊆ (𝑁‘{𝑌, 𝑇})) |
50 | 49 | 3ad2ant1 1131 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑤 ∈ 𝑉 ∧ (𝑁‘{𝑌, 𝑇}) = (𝑁‘{𝑤})) → (𝑁‘{𝑌}) ⊆ (𝑁‘{𝑌, 𝑇})) |
51 | | simp3 1136 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑤 ∈ 𝑉 ∧ (𝑁‘{𝑌, 𝑇}) = (𝑁‘{𝑤})) → (𝑁‘{𝑌, 𝑇}) = (𝑁‘{𝑤})) |
52 | 50, 51 | sseqtrd 3928 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑤 ∈ 𝑉 ∧ (𝑁‘{𝑌, 𝑇}) = (𝑁‘{𝑤})) → (𝑁‘{𝑌}) ⊆ (𝑁‘{𝑤})) |
53 | | eqid 2759 |
. . . . . . . . . . . . . 14
⊢
(LSSum‘𝑈) =
(LSSum‘𝑈) |
54 | 53 | lsmless2 18838 |
. . . . . . . . . . . . 13
⊢ (((𝑁‘{𝑋}) ∈ (SubGrp‘𝑈) ∧ (𝑁‘{𝑤}) ∈ (SubGrp‘𝑈) ∧ (𝑁‘{𝑌}) ⊆ (𝑁‘{𝑤})) → ((𝑁‘{𝑋})(LSSum‘𝑈)(𝑁‘{𝑌})) ⊆ ((𝑁‘{𝑋})(LSSum‘𝑈)(𝑁‘{𝑤}))) |
55 | 40, 43, 52, 54 | syl3anc 1369 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑤 ∈ 𝑉 ∧ (𝑁‘{𝑌, 𝑇}) = (𝑁‘{𝑤})) → ((𝑁‘{𝑋})(LSSum‘𝑈)(𝑁‘{𝑌})) ⊆ ((𝑁‘{𝑋})(LSSum‘𝑈)(𝑁‘{𝑤}))) |
56 | 8, 2, 53, 6, 30, 21 | lsmpr 19914 |
. . . . . . . . . . . . 13
⊢ (𝜑 → (𝑁‘{𝑋, 𝑌}) = ((𝑁‘{𝑋})(LSSum‘𝑈)(𝑁‘{𝑌}))) |
57 | 56 | 3ad2ant1 1131 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑤 ∈ 𝑉 ∧ (𝑁‘{𝑌, 𝑇}) = (𝑁‘{𝑤})) → (𝑁‘{𝑋, 𝑌}) = ((𝑁‘{𝑋})(LSSum‘𝑈)(𝑁‘{𝑌}))) |
58 | | prcom 4618 |
. . . . . . . . . . . . . 14
⊢ {𝑤, 𝑋} = {𝑋, 𝑤} |
59 | 58 | fveq2i 6654 |
. . . . . . . . . . . . 13
⊢ (𝑁‘{𝑤, 𝑋}) = (𝑁‘{𝑋, 𝑤}) |
60 | 8, 2, 53, 34, 31, 29 | lsmpr 19914 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑤 ∈ 𝑉 ∧ (𝑁‘{𝑌, 𝑇}) = (𝑁‘{𝑤})) → (𝑁‘{𝑋, 𝑤}) = ((𝑁‘{𝑋})(LSSum‘𝑈)(𝑁‘{𝑤}))) |
61 | 59, 60 | syl5eq 2806 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑤 ∈ 𝑉 ∧ (𝑁‘{𝑌, 𝑇}) = (𝑁‘{𝑤})) → (𝑁‘{𝑤, 𝑋}) = ((𝑁‘{𝑋})(LSSum‘𝑈)(𝑁‘{𝑤}))) |
62 | 55, 57, 61 | 3sstr4d 3935 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑤 ∈ 𝑉 ∧ (𝑁‘{𝑌, 𝑇}) = (𝑁‘{𝑤})) → (𝑁‘{𝑋, 𝑌}) ⊆ (𝑁‘{𝑤, 𝑋})) |
63 | 62 | ssneld 3890 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑤 ∈ 𝑉 ∧ (𝑁‘{𝑌, 𝑇}) = (𝑁‘{𝑤})) → (¬ 𝑧 ∈ (𝑁‘{𝑤, 𝑋}) → ¬ 𝑧 ∈ (𝑁‘{𝑋, 𝑌}))) |
64 | 8, 1, 2 | lspsncl 19802 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑈 ∈ LMod ∧ 𝑍 ∈ 𝑉) → (𝑁‘{𝑍}) ∈ (LSubSp‘𝑈)) |
65 | 6, 9, 64 | syl2anc 588 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → (𝑁‘{𝑍}) ∈ (LSubSp‘𝑈)) |
66 | 65 | 3ad2ant1 1131 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑤 ∈ 𝑉 ∧ (𝑁‘{𝑌, 𝑇}) = (𝑁‘{𝑤})) → (𝑁‘{𝑍}) ∈ (LSubSp‘𝑈)) |
67 | 36, 66 | sseldd 3889 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑤 ∈ 𝑉 ∧ (𝑁‘{𝑌, 𝑇}) = (𝑁‘{𝑤})) → (𝑁‘{𝑍}) ∈ (SubGrp‘𝑈)) |
68 | | snsspr2 4698 |
. . . . . . . . . . . . . . . . 17
⊢ {𝑇} ⊆ {𝑌, 𝑇} |
69 | 68 | a1i 11 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → {𝑇} ⊆ {𝑌, 𝑇}) |
70 | 8, 2 | lspss 19809 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑈 ∈ LMod ∧ {𝑌, 𝑇} ⊆ 𝑉 ∧ {𝑇} ⊆ {𝑌, 𝑇}) → (𝑁‘{𝑇}) ⊆ (𝑁‘{𝑌, 𝑇})) |
71 | 6, 45, 69, 70 | syl3anc 1369 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → (𝑁‘{𝑇}) ⊆ (𝑁‘{𝑌, 𝑇})) |
72 | 71 | 3ad2ant1 1131 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑤 ∈ 𝑉 ∧ (𝑁‘{𝑌, 𝑇}) = (𝑁‘{𝑤})) → (𝑁‘{𝑇}) ⊆ (𝑁‘{𝑌, 𝑇})) |
73 | 72, 51 | sseqtrd 3928 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑤 ∈ 𝑉 ∧ (𝑁‘{𝑌, 𝑇}) = (𝑁‘{𝑤})) → (𝑁‘{𝑇}) ⊆ (𝑁‘{𝑤})) |
74 | 53 | lsmless2 18838 |
. . . . . . . . . . . . 13
⊢ (((𝑁‘{𝑍}) ∈ (SubGrp‘𝑈) ∧ (𝑁‘{𝑤}) ∈ (SubGrp‘𝑈) ∧ (𝑁‘{𝑇}) ⊆ (𝑁‘{𝑤})) → ((𝑁‘{𝑍})(LSSum‘𝑈)(𝑁‘{𝑇})) ⊆ ((𝑁‘{𝑍})(LSSum‘𝑈)(𝑁‘{𝑤}))) |
75 | 67, 43, 73, 74 | syl3anc 1369 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑤 ∈ 𝑉 ∧ (𝑁‘{𝑌, 𝑇}) = (𝑁‘{𝑤})) → ((𝑁‘{𝑍})(LSSum‘𝑈)(𝑁‘{𝑇})) ⊆ ((𝑁‘{𝑍})(LSSum‘𝑈)(𝑁‘{𝑤}))) |
76 | 8, 2, 53, 6, 9, 10 | lsmpr 19914 |
. . . . . . . . . . . . 13
⊢ (𝜑 → (𝑁‘{𝑍, 𝑇}) = ((𝑁‘{𝑍})(LSSum‘𝑈)(𝑁‘{𝑇}))) |
77 | 76 | 3ad2ant1 1131 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑤 ∈ 𝑉 ∧ (𝑁‘{𝑌, 𝑇}) = (𝑁‘{𝑤})) → (𝑁‘{𝑍, 𝑇}) = ((𝑁‘{𝑍})(LSSum‘𝑈)(𝑁‘{𝑇}))) |
78 | | prcom 4618 |
. . . . . . . . . . . . . 14
⊢ {𝑤, 𝑍} = {𝑍, 𝑤} |
79 | 78 | fveq2i 6654 |
. . . . . . . . . . . . 13
⊢ (𝑁‘{𝑤, 𝑍}) = (𝑁‘{𝑍, 𝑤}) |
80 | 8, 2, 53, 34, 32, 29 | lsmpr 19914 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑤 ∈ 𝑉 ∧ (𝑁‘{𝑌, 𝑇}) = (𝑁‘{𝑤})) → (𝑁‘{𝑍, 𝑤}) = ((𝑁‘{𝑍})(LSSum‘𝑈)(𝑁‘{𝑤}))) |
81 | 79, 80 | syl5eq 2806 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑤 ∈ 𝑉 ∧ (𝑁‘{𝑌, 𝑇}) = (𝑁‘{𝑤})) → (𝑁‘{𝑤, 𝑍}) = ((𝑁‘{𝑍})(LSSum‘𝑈)(𝑁‘{𝑤}))) |
82 | 75, 77, 81 | 3sstr4d 3935 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑤 ∈ 𝑉 ∧ (𝑁‘{𝑌, 𝑇}) = (𝑁‘{𝑤})) → (𝑁‘{𝑍, 𝑇}) ⊆ (𝑁‘{𝑤, 𝑍})) |
83 | 82 | ssneld 3890 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑤 ∈ 𝑉 ∧ (𝑁‘{𝑌, 𝑇}) = (𝑁‘{𝑤})) → (¬ 𝑧 ∈ (𝑁‘{𝑤, 𝑍}) → ¬ 𝑧 ∈ (𝑁‘{𝑍, 𝑇}))) |
84 | 63, 83 | anim12d 612 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑤 ∈ 𝑉 ∧ (𝑁‘{𝑌, 𝑇}) = (𝑁‘{𝑤})) → ((¬ 𝑧 ∈ (𝑁‘{𝑤, 𝑋}) ∧ ¬ 𝑧 ∈ (𝑁‘{𝑤, 𝑍})) → (¬ 𝑧 ∈ (𝑁‘{𝑋, 𝑌}) ∧ ¬ 𝑧 ∈ (𝑁‘{𝑍, 𝑇})))) |
85 | 84 | reximdv 3195 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑤 ∈ 𝑉 ∧ (𝑁‘{𝑌, 𝑇}) = (𝑁‘{𝑤})) → (∃𝑧 ∈ 𝑉 (¬ 𝑧 ∈ (𝑁‘{𝑤, 𝑋}) ∧ ¬ 𝑧 ∈ (𝑁‘{𝑤, 𝑍})) → ∃𝑧 ∈ 𝑉 (¬ 𝑧 ∈ (𝑁‘{𝑋, 𝑌}) ∧ ¬ 𝑧 ∈ (𝑁‘{𝑍, 𝑇})))) |
86 | 33, 85 | mpd 15 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑤 ∈ 𝑉 ∧ (𝑁‘{𝑌, 𝑇}) = (𝑁‘{𝑤})) → ∃𝑧 ∈ 𝑉 (¬ 𝑧 ∈ (𝑁‘{𝑋, 𝑌}) ∧ ¬ 𝑧 ∈ (𝑁‘{𝑍, 𝑇}))) |
87 | 86 | rexlimdv3a 3208 |
. . . . . 6
⊢ (𝜑 → (∃𝑤 ∈ 𝑉 (𝑁‘{𝑌, 𝑇}) = (𝑁‘{𝑤}) → ∃𝑧 ∈ 𝑉 (¬ 𝑧 ∈ (𝑁‘{𝑋, 𝑌}) ∧ ¬ 𝑧 ∈ (𝑁‘{𝑍, 𝑇})))) |
88 | 87 | adantr 485 |
. . . . 5
⊢ ((𝜑 ∧ (𝑁‘{𝑌, 𝑇}) ⊊ (𝑁‘{𝑍, 𝑇})) → (∃𝑤 ∈ 𝑉 (𝑁‘{𝑌, 𝑇}) = (𝑁‘{𝑤}) → ∃𝑧 ∈ 𝑉 (¬ 𝑧 ∈ (𝑁‘{𝑋, 𝑌}) ∧ ¬ 𝑧 ∈ (𝑁‘{𝑍, 𝑇})))) |
89 | 27, 88 | mpd 15 |
. . . 4
⊢ ((𝜑 ∧ (𝑁‘{𝑌, 𝑇}) ⊊ (𝑁‘{𝑍, 𝑇})) → ∃𝑧 ∈ 𝑉 (¬ 𝑧 ∈ (𝑁‘{𝑋, 𝑌}) ∧ ¬ 𝑧 ∈ (𝑁‘{𝑍, 𝑇}))) |
90 | 3, 4, 8, 2, 5, 21,
30, 10 | dvh3dim2 39009 |
. . . . . 6
⊢ (𝜑 → ∃𝑧 ∈ 𝑉 (¬ 𝑧 ∈ (𝑁‘{𝑌, 𝑋}) ∧ ¬ 𝑧 ∈ (𝑁‘{𝑌, 𝑇}))) |
91 | 90 | adantr 485 |
. . . . 5
⊢ ((𝜑 ∧ (𝑁‘{𝑌, 𝑇}) = (𝑁‘{𝑍, 𝑇})) → ∃𝑧 ∈ 𝑉 (¬ 𝑧 ∈ (𝑁‘{𝑌, 𝑋}) ∧ ¬ 𝑧 ∈ (𝑁‘{𝑌, 𝑇}))) |
92 | | simpr 489 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑁‘{𝑌, 𝑇}) = (𝑁‘{𝑍, 𝑇})) → (𝑁‘{𝑌, 𝑇}) = (𝑁‘{𝑍, 𝑇})) |
93 | | prcom 4618 |
. . . . . . . . . . . 12
⊢ {𝑌, 𝑋} = {𝑋, 𝑌} |
94 | 93 | fveq2i 6654 |
. . . . . . . . . . 11
⊢ (𝑁‘{𝑌, 𝑋}) = (𝑁‘{𝑋, 𝑌}) |
95 | 94 | eleq2i 2842 |
. . . . . . . . . 10
⊢ (𝑧 ∈ (𝑁‘{𝑌, 𝑋}) ↔ 𝑧 ∈ (𝑁‘{𝑋, 𝑌})) |
96 | 95 | notbii 324 |
. . . . . . . . 9
⊢ (¬
𝑧 ∈ (𝑁‘{𝑌, 𝑋}) ↔ ¬ 𝑧 ∈ (𝑁‘{𝑋, 𝑌})) |
97 | 96 | a1i 11 |
. . . . . . . 8
⊢ ((𝑁‘{𝑌, 𝑇}) = (𝑁‘{𝑍, 𝑇}) → (¬ 𝑧 ∈ (𝑁‘{𝑌, 𝑋}) ↔ ¬ 𝑧 ∈ (𝑁‘{𝑋, 𝑌}))) |
98 | | eleq2 2839 |
. . . . . . . . 9
⊢ ((𝑁‘{𝑌, 𝑇}) = (𝑁‘{𝑍, 𝑇}) → (𝑧 ∈ (𝑁‘{𝑌, 𝑇}) ↔ 𝑧 ∈ (𝑁‘{𝑍, 𝑇}))) |
99 | 98 | notbid 322 |
. . . . . . . 8
⊢ ((𝑁‘{𝑌, 𝑇}) = (𝑁‘{𝑍, 𝑇}) → (¬ 𝑧 ∈ (𝑁‘{𝑌, 𝑇}) ↔ ¬ 𝑧 ∈ (𝑁‘{𝑍, 𝑇}))) |
100 | 97, 99 | anbi12d 634 |
. . . . . . 7
⊢ ((𝑁‘{𝑌, 𝑇}) = (𝑁‘{𝑍, 𝑇}) → ((¬ 𝑧 ∈ (𝑁‘{𝑌, 𝑋}) ∧ ¬ 𝑧 ∈ (𝑁‘{𝑌, 𝑇})) ↔ (¬ 𝑧 ∈ (𝑁‘{𝑋, 𝑌}) ∧ ¬ 𝑧 ∈ (𝑁‘{𝑍, 𝑇})))) |
101 | 92, 100 | syl 17 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑁‘{𝑌, 𝑇}) = (𝑁‘{𝑍, 𝑇})) → ((¬ 𝑧 ∈ (𝑁‘{𝑌, 𝑋}) ∧ ¬ 𝑧 ∈ (𝑁‘{𝑌, 𝑇})) ↔ (¬ 𝑧 ∈ (𝑁‘{𝑋, 𝑌}) ∧ ¬ 𝑧 ∈ (𝑁‘{𝑍, 𝑇})))) |
102 | 101 | rexbidv 3219 |
. . . . 5
⊢ ((𝜑 ∧ (𝑁‘{𝑌, 𝑇}) = (𝑁‘{𝑍, 𝑇})) → (∃𝑧 ∈ 𝑉 (¬ 𝑧 ∈ (𝑁‘{𝑌, 𝑋}) ∧ ¬ 𝑧 ∈ (𝑁‘{𝑌, 𝑇})) ↔ ∃𝑧 ∈ 𝑉 (¬ 𝑧 ∈ (𝑁‘{𝑋, 𝑌}) ∧ ¬ 𝑧 ∈ (𝑁‘{𝑍, 𝑇})))) |
103 | 91, 102 | mpbid 235 |
. . . 4
⊢ ((𝜑 ∧ (𝑁‘{𝑌, 𝑇}) = (𝑁‘{𝑍, 𝑇})) → ∃𝑧 ∈ 𝑉 (¬ 𝑧 ∈ (𝑁‘{𝑋, 𝑌}) ∧ ¬ 𝑧 ∈ (𝑁‘{𝑍, 𝑇}))) |
104 | 89, 103 | jaodan 956 |
. . 3
⊢ ((𝜑 ∧ ((𝑁‘{𝑌, 𝑇}) ⊊ (𝑁‘{𝑍, 𝑇}) ∨ (𝑁‘{𝑌, 𝑇}) = (𝑁‘{𝑍, 𝑇}))) → ∃𝑧 ∈ 𝑉 (¬ 𝑧 ∈ (𝑁‘{𝑋, 𝑌}) ∧ ¬ 𝑧 ∈ (𝑁‘{𝑍, 𝑇}))) |
105 | 18, 104 | syldan 595 |
. 2
⊢ ((𝜑 ∧ 𝑌 ∈ (𝑁‘{𝑍, 𝑇})) → ∃𝑧 ∈ 𝑉 (¬ 𝑧 ∈ (𝑁‘{𝑋, 𝑌}) ∧ ¬ 𝑧 ∈ (𝑁‘{𝑍, 𝑇}))) |
106 | 3, 4, 8, 2, 5, 21,
30, 10 | dvh3dim2 39009 |
. . . 4
⊢ (𝜑 → ∃𝑤 ∈ 𝑉 (¬ 𝑤 ∈ (𝑁‘{𝑌, 𝑋}) ∧ ¬ 𝑤 ∈ (𝑁‘{𝑌, 𝑇}))) |
107 | 106 | adantr 485 |
. . 3
⊢ ((𝜑 ∧ ¬ 𝑌 ∈ (𝑁‘{𝑍, 𝑇})) → ∃𝑤 ∈ 𝑉 (¬ 𝑤 ∈ (𝑁‘{𝑌, 𝑋}) ∧ ¬ 𝑤 ∈ (𝑁‘{𝑌, 𝑇}))) |
108 | | simpl1l 1222 |
. . . . . . . 8
⊢ ((((𝜑 ∧ ¬ 𝑌 ∈ (𝑁‘{𝑍, 𝑇})) ∧ 𝑤 ∈ 𝑉 ∧ (¬ 𝑤 ∈ (𝑁‘{𝑌, 𝑋}) ∧ ¬ 𝑤 ∈ (𝑁‘{𝑌, 𝑇}))) ∧ 𝑤 ∈ (𝑁‘{𝑍, 𝑇})) → 𝜑) |
109 | 108, 6 | syl 17 |
. . . . . . 7
⊢ ((((𝜑 ∧ ¬ 𝑌 ∈ (𝑁‘{𝑍, 𝑇})) ∧ 𝑤 ∈ 𝑉 ∧ (¬ 𝑤 ∈ (𝑁‘{𝑌, 𝑋}) ∧ ¬ 𝑤 ∈ (𝑁‘{𝑌, 𝑇}))) ∧ 𝑤 ∈ (𝑁‘{𝑍, 𝑇})) → 𝑈 ∈ LMod) |
110 | | simpl2 1190 |
. . . . . . 7
⊢ ((((𝜑 ∧ ¬ 𝑌 ∈ (𝑁‘{𝑍, 𝑇})) ∧ 𝑤 ∈ 𝑉 ∧ (¬ 𝑤 ∈ (𝑁‘{𝑌, 𝑋}) ∧ ¬ 𝑤 ∈ (𝑁‘{𝑌, 𝑇}))) ∧ 𝑤 ∈ (𝑁‘{𝑍, 𝑇})) → 𝑤 ∈ 𝑉) |
111 | 108, 21 | syl 17 |
. . . . . . 7
⊢ ((((𝜑 ∧ ¬ 𝑌 ∈ (𝑁‘{𝑍, 𝑇})) ∧ 𝑤 ∈ 𝑉 ∧ (¬ 𝑤 ∈ (𝑁‘{𝑌, 𝑋}) ∧ ¬ 𝑤 ∈ (𝑁‘{𝑌, 𝑇}))) ∧ 𝑤 ∈ (𝑁‘{𝑍, 𝑇})) → 𝑌 ∈ 𝑉) |
112 | | eqid 2759 |
. . . . . . . 8
⊢
(+g‘𝑈) = (+g‘𝑈) |
113 | 8, 112 | lmodvacl 19701 |
. . . . . . 7
⊢ ((𝑈 ∈ LMod ∧ 𝑤 ∈ 𝑉 ∧ 𝑌 ∈ 𝑉) → (𝑤(+g‘𝑈)𝑌) ∈ 𝑉) |
114 | 109, 110,
111, 113 | syl3anc 1369 |
. . . . . 6
⊢ ((((𝜑 ∧ ¬ 𝑌 ∈ (𝑁‘{𝑍, 𝑇})) ∧ 𝑤 ∈ 𝑉 ∧ (¬ 𝑤 ∈ (𝑁‘{𝑌, 𝑋}) ∧ ¬ 𝑤 ∈ (𝑁‘{𝑌, 𝑇}))) ∧ 𝑤 ∈ (𝑁‘{𝑍, 𝑇})) → (𝑤(+g‘𝑈)𝑌) ∈ 𝑉) |
115 | 8, 1, 2, 6, 30, 21 | lspprcl 19803 |
. . . . . . . 8
⊢ (𝜑 → (𝑁‘{𝑋, 𝑌}) ∈ (LSubSp‘𝑈)) |
116 | 108, 115 | syl 17 |
. . . . . . 7
⊢ ((((𝜑 ∧ ¬ 𝑌 ∈ (𝑁‘{𝑍, 𝑇})) ∧ 𝑤 ∈ 𝑉 ∧ (¬ 𝑤 ∈ (𝑁‘{𝑌, 𝑋}) ∧ ¬ 𝑤 ∈ (𝑁‘{𝑌, 𝑇}))) ∧ 𝑤 ∈ (𝑁‘{𝑍, 𝑇})) → (𝑁‘{𝑋, 𝑌}) ∈ (LSubSp‘𝑈)) |
117 | 8, 2, 6, 30, 21 | lspprid2 19823 |
. . . . . . . 8
⊢ (𝜑 → 𝑌 ∈ (𝑁‘{𝑋, 𝑌})) |
118 | 108, 117 | syl 17 |
. . . . . . 7
⊢ ((((𝜑 ∧ ¬ 𝑌 ∈ (𝑁‘{𝑍, 𝑇})) ∧ 𝑤 ∈ 𝑉 ∧ (¬ 𝑤 ∈ (𝑁‘{𝑌, 𝑋}) ∧ ¬ 𝑤 ∈ (𝑁‘{𝑌, 𝑇}))) ∧ 𝑤 ∈ (𝑁‘{𝑍, 𝑇})) → 𝑌 ∈ (𝑁‘{𝑋, 𝑌})) |
119 | | simpl3l 1226 |
. . . . . . . 8
⊢ ((((𝜑 ∧ ¬ 𝑌 ∈ (𝑁‘{𝑍, 𝑇})) ∧ 𝑤 ∈ 𝑉 ∧ (¬ 𝑤 ∈ (𝑁‘{𝑌, 𝑋}) ∧ ¬ 𝑤 ∈ (𝑁‘{𝑌, 𝑇}))) ∧ 𝑤 ∈ (𝑁‘{𝑍, 𝑇})) → ¬ 𝑤 ∈ (𝑁‘{𝑌, 𝑋})) |
120 | 94 | eleq2i 2842 |
. . . . . . . 8
⊢ (𝑤 ∈ (𝑁‘{𝑌, 𝑋}) ↔ 𝑤 ∈ (𝑁‘{𝑋, 𝑌})) |
121 | 119, 120 | sylnib 332 |
. . . . . . 7
⊢ ((((𝜑 ∧ ¬ 𝑌 ∈ (𝑁‘{𝑍, 𝑇})) ∧ 𝑤 ∈ 𝑉 ∧ (¬ 𝑤 ∈ (𝑁‘{𝑌, 𝑋}) ∧ ¬ 𝑤 ∈ (𝑁‘{𝑌, 𝑇}))) ∧ 𝑤 ∈ (𝑁‘{𝑍, 𝑇})) → ¬ 𝑤 ∈ (𝑁‘{𝑋, 𝑌})) |
122 | 8, 112, 1, 109, 116, 118, 110, 121 | lssvancl2 19770 |
. . . . . 6
⊢ ((((𝜑 ∧ ¬ 𝑌 ∈ (𝑁‘{𝑍, 𝑇})) ∧ 𝑤 ∈ 𝑉 ∧ (¬ 𝑤 ∈ (𝑁‘{𝑌, 𝑋}) ∧ ¬ 𝑤 ∈ (𝑁‘{𝑌, 𝑇}))) ∧ 𝑤 ∈ (𝑁‘{𝑍, 𝑇})) → ¬ (𝑤(+g‘𝑈)𝑌) ∈ (𝑁‘{𝑋, 𝑌})) |
123 | 108, 11 | syl 17 |
. . . . . . 7
⊢ ((((𝜑 ∧ ¬ 𝑌 ∈ (𝑁‘{𝑍, 𝑇})) ∧ 𝑤 ∈ 𝑉 ∧ (¬ 𝑤 ∈ (𝑁‘{𝑌, 𝑋}) ∧ ¬ 𝑤 ∈ (𝑁‘{𝑌, 𝑇}))) ∧ 𝑤 ∈ (𝑁‘{𝑍, 𝑇})) → (𝑁‘{𝑍, 𝑇}) ∈ (LSubSp‘𝑈)) |
124 | | simpr 489 |
. . . . . . 7
⊢ ((((𝜑 ∧ ¬ 𝑌 ∈ (𝑁‘{𝑍, 𝑇})) ∧ 𝑤 ∈ 𝑉 ∧ (¬ 𝑤 ∈ (𝑁‘{𝑌, 𝑋}) ∧ ¬ 𝑤 ∈ (𝑁‘{𝑌, 𝑇}))) ∧ 𝑤 ∈ (𝑁‘{𝑍, 𝑇})) → 𝑤 ∈ (𝑁‘{𝑍, 𝑇})) |
125 | | simpl1r 1223 |
. . . . . . 7
⊢ ((((𝜑 ∧ ¬ 𝑌 ∈ (𝑁‘{𝑍, 𝑇})) ∧ 𝑤 ∈ 𝑉 ∧ (¬ 𝑤 ∈ (𝑁‘{𝑌, 𝑋}) ∧ ¬ 𝑤 ∈ (𝑁‘{𝑌, 𝑇}))) ∧ 𝑤 ∈ (𝑁‘{𝑍, 𝑇})) → ¬ 𝑌 ∈ (𝑁‘{𝑍, 𝑇})) |
126 | 8, 112, 1, 109, 123, 124, 111, 125 | lssvancl1 19769 |
. . . . . 6
⊢ ((((𝜑 ∧ ¬ 𝑌 ∈ (𝑁‘{𝑍, 𝑇})) ∧ 𝑤 ∈ 𝑉 ∧ (¬ 𝑤 ∈ (𝑁‘{𝑌, 𝑋}) ∧ ¬ 𝑤 ∈ (𝑁‘{𝑌, 𝑇}))) ∧ 𝑤 ∈ (𝑁‘{𝑍, 𝑇})) → ¬ (𝑤(+g‘𝑈)𝑌) ∈ (𝑁‘{𝑍, 𝑇})) |
127 | | eleq1 2838 |
. . . . . . . . 9
⊢ (𝑧 = (𝑤(+g‘𝑈)𝑌) → (𝑧 ∈ (𝑁‘{𝑋, 𝑌}) ↔ (𝑤(+g‘𝑈)𝑌) ∈ (𝑁‘{𝑋, 𝑌}))) |
128 | 127 | notbid 322 |
. . . . . . . 8
⊢ (𝑧 = (𝑤(+g‘𝑈)𝑌) → (¬ 𝑧 ∈ (𝑁‘{𝑋, 𝑌}) ↔ ¬ (𝑤(+g‘𝑈)𝑌) ∈ (𝑁‘{𝑋, 𝑌}))) |
129 | | eleq1 2838 |
. . . . . . . . 9
⊢ (𝑧 = (𝑤(+g‘𝑈)𝑌) → (𝑧 ∈ (𝑁‘{𝑍, 𝑇}) ↔ (𝑤(+g‘𝑈)𝑌) ∈ (𝑁‘{𝑍, 𝑇}))) |
130 | 129 | notbid 322 |
. . . . . . . 8
⊢ (𝑧 = (𝑤(+g‘𝑈)𝑌) → (¬ 𝑧 ∈ (𝑁‘{𝑍, 𝑇}) ↔ ¬ (𝑤(+g‘𝑈)𝑌) ∈ (𝑁‘{𝑍, 𝑇}))) |
131 | 128, 130 | anbi12d 634 |
. . . . . . 7
⊢ (𝑧 = (𝑤(+g‘𝑈)𝑌) → ((¬ 𝑧 ∈ (𝑁‘{𝑋, 𝑌}) ∧ ¬ 𝑧 ∈ (𝑁‘{𝑍, 𝑇})) ↔ (¬ (𝑤(+g‘𝑈)𝑌) ∈ (𝑁‘{𝑋, 𝑌}) ∧ ¬ (𝑤(+g‘𝑈)𝑌) ∈ (𝑁‘{𝑍, 𝑇})))) |
132 | 131 | rspcev 3539 |
. . . . . 6
⊢ (((𝑤(+g‘𝑈)𝑌) ∈ 𝑉 ∧ (¬ (𝑤(+g‘𝑈)𝑌) ∈ (𝑁‘{𝑋, 𝑌}) ∧ ¬ (𝑤(+g‘𝑈)𝑌) ∈ (𝑁‘{𝑍, 𝑇}))) → ∃𝑧 ∈ 𝑉 (¬ 𝑧 ∈ (𝑁‘{𝑋, 𝑌}) ∧ ¬ 𝑧 ∈ (𝑁‘{𝑍, 𝑇}))) |
133 | 114, 122,
126, 132 | syl12anc 836 |
. . . . 5
⊢ ((((𝜑 ∧ ¬ 𝑌 ∈ (𝑁‘{𝑍, 𝑇})) ∧ 𝑤 ∈ 𝑉 ∧ (¬ 𝑤 ∈ (𝑁‘{𝑌, 𝑋}) ∧ ¬ 𝑤 ∈ (𝑁‘{𝑌, 𝑇}))) ∧ 𝑤 ∈ (𝑁‘{𝑍, 𝑇})) → ∃𝑧 ∈ 𝑉 (¬ 𝑧 ∈ (𝑁‘{𝑋, 𝑌}) ∧ ¬ 𝑧 ∈ (𝑁‘{𝑍, 𝑇}))) |
134 | | simpl2 1190 |
. . . . . 6
⊢ ((((𝜑 ∧ ¬ 𝑌 ∈ (𝑁‘{𝑍, 𝑇})) ∧ 𝑤 ∈ 𝑉 ∧ (¬ 𝑤 ∈ (𝑁‘{𝑌, 𝑋}) ∧ ¬ 𝑤 ∈ (𝑁‘{𝑌, 𝑇}))) ∧ ¬ 𝑤 ∈ (𝑁‘{𝑍, 𝑇})) → 𝑤 ∈ 𝑉) |
135 | | simpl3l 1226 |
. . . . . . 7
⊢ ((((𝜑 ∧ ¬ 𝑌 ∈ (𝑁‘{𝑍, 𝑇})) ∧ 𝑤 ∈ 𝑉 ∧ (¬ 𝑤 ∈ (𝑁‘{𝑌, 𝑋}) ∧ ¬ 𝑤 ∈ (𝑁‘{𝑌, 𝑇}))) ∧ ¬ 𝑤 ∈ (𝑁‘{𝑍, 𝑇})) → ¬ 𝑤 ∈ (𝑁‘{𝑌, 𝑋})) |
136 | 135, 120 | sylnib 332 |
. . . . . 6
⊢ ((((𝜑 ∧ ¬ 𝑌 ∈ (𝑁‘{𝑍, 𝑇})) ∧ 𝑤 ∈ 𝑉 ∧ (¬ 𝑤 ∈ (𝑁‘{𝑌, 𝑋}) ∧ ¬ 𝑤 ∈ (𝑁‘{𝑌, 𝑇}))) ∧ ¬ 𝑤 ∈ (𝑁‘{𝑍, 𝑇})) → ¬ 𝑤 ∈ (𝑁‘{𝑋, 𝑌})) |
137 | | simpr 489 |
. . . . . 6
⊢ ((((𝜑 ∧ ¬ 𝑌 ∈ (𝑁‘{𝑍, 𝑇})) ∧ 𝑤 ∈ 𝑉 ∧ (¬ 𝑤 ∈ (𝑁‘{𝑌, 𝑋}) ∧ ¬ 𝑤 ∈ (𝑁‘{𝑌, 𝑇}))) ∧ ¬ 𝑤 ∈ (𝑁‘{𝑍, 𝑇})) → ¬ 𝑤 ∈ (𝑁‘{𝑍, 𝑇})) |
138 | | eleq1 2838 |
. . . . . . . . 9
⊢ (𝑧 = 𝑤 → (𝑧 ∈ (𝑁‘{𝑋, 𝑌}) ↔ 𝑤 ∈ (𝑁‘{𝑋, 𝑌}))) |
139 | 138 | notbid 322 |
. . . . . . . 8
⊢ (𝑧 = 𝑤 → (¬ 𝑧 ∈ (𝑁‘{𝑋, 𝑌}) ↔ ¬ 𝑤 ∈ (𝑁‘{𝑋, 𝑌}))) |
140 | | eleq1 2838 |
. . . . . . . . 9
⊢ (𝑧 = 𝑤 → (𝑧 ∈ (𝑁‘{𝑍, 𝑇}) ↔ 𝑤 ∈ (𝑁‘{𝑍, 𝑇}))) |
141 | 140 | notbid 322 |
. . . . . . . 8
⊢ (𝑧 = 𝑤 → (¬ 𝑧 ∈ (𝑁‘{𝑍, 𝑇}) ↔ ¬ 𝑤 ∈ (𝑁‘{𝑍, 𝑇}))) |
142 | 139, 141 | anbi12d 634 |
. . . . . . 7
⊢ (𝑧 = 𝑤 → ((¬ 𝑧 ∈ (𝑁‘{𝑋, 𝑌}) ∧ ¬ 𝑧 ∈ (𝑁‘{𝑍, 𝑇})) ↔ (¬ 𝑤 ∈ (𝑁‘{𝑋, 𝑌}) ∧ ¬ 𝑤 ∈ (𝑁‘{𝑍, 𝑇})))) |
143 | 142 | rspcev 3539 |
. . . . . 6
⊢ ((𝑤 ∈ 𝑉 ∧ (¬ 𝑤 ∈ (𝑁‘{𝑋, 𝑌}) ∧ ¬ 𝑤 ∈ (𝑁‘{𝑍, 𝑇}))) → ∃𝑧 ∈ 𝑉 (¬ 𝑧 ∈ (𝑁‘{𝑋, 𝑌}) ∧ ¬ 𝑧 ∈ (𝑁‘{𝑍, 𝑇}))) |
144 | 134, 136,
137, 143 | syl12anc 836 |
. . . . 5
⊢ ((((𝜑 ∧ ¬ 𝑌 ∈ (𝑁‘{𝑍, 𝑇})) ∧ 𝑤 ∈ 𝑉 ∧ (¬ 𝑤 ∈ (𝑁‘{𝑌, 𝑋}) ∧ ¬ 𝑤 ∈ (𝑁‘{𝑌, 𝑇}))) ∧ ¬ 𝑤 ∈ (𝑁‘{𝑍, 𝑇})) → ∃𝑧 ∈ 𝑉 (¬ 𝑧 ∈ (𝑁‘{𝑋, 𝑌}) ∧ ¬ 𝑧 ∈ (𝑁‘{𝑍, 𝑇}))) |
145 | 133, 144 | pm2.61dan 813 |
. . . 4
⊢ (((𝜑 ∧ ¬ 𝑌 ∈ (𝑁‘{𝑍, 𝑇})) ∧ 𝑤 ∈ 𝑉 ∧ (¬ 𝑤 ∈ (𝑁‘{𝑌, 𝑋}) ∧ ¬ 𝑤 ∈ (𝑁‘{𝑌, 𝑇}))) → ∃𝑧 ∈ 𝑉 (¬ 𝑧 ∈ (𝑁‘{𝑋, 𝑌}) ∧ ¬ 𝑧 ∈ (𝑁‘{𝑍, 𝑇}))) |
146 | 145 | rexlimdv3a 3208 |
. . 3
⊢ ((𝜑 ∧ ¬ 𝑌 ∈ (𝑁‘{𝑍, 𝑇})) → (∃𝑤 ∈ 𝑉 (¬ 𝑤 ∈ (𝑁‘{𝑌, 𝑋}) ∧ ¬ 𝑤 ∈ (𝑁‘{𝑌, 𝑇})) → ∃𝑧 ∈ 𝑉 (¬ 𝑧 ∈ (𝑁‘{𝑋, 𝑌}) ∧ ¬ 𝑧 ∈ (𝑁‘{𝑍, 𝑇})))) |
147 | 107, 146 | mpd 15 |
. 2
⊢ ((𝜑 ∧ ¬ 𝑌 ∈ (𝑁‘{𝑍, 𝑇})) → ∃𝑧 ∈ 𝑉 (¬ 𝑧 ∈ (𝑁‘{𝑋, 𝑌}) ∧ ¬ 𝑧 ∈ (𝑁‘{𝑍, 𝑇}))) |
148 | 105, 147 | pm2.61dan 813 |
1
⊢ (𝜑 → ∃𝑧 ∈ 𝑉 (¬ 𝑧 ∈ (𝑁‘{𝑋, 𝑌}) ∧ ¬ 𝑧 ∈ (𝑁‘{𝑍, 𝑇}))) |