Step | Hyp | Ref
| Expression |
1 | | dihatexv.k |
. . . . . . . . 9
⊢ (𝜑 → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻)) |
2 | 1 | ad2antrr 762 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑄 ∈ 𝐴) ∧ 𝑄(le‘𝐾)𝑊) → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻)) |
3 | | simplr 792 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑄 ∈ 𝐴) ∧ 𝑄(le‘𝐾)𝑊) → 𝑄 ∈ 𝐴) |
4 | | simpr 477 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑄 ∈ 𝐴) ∧ 𝑄(le‘𝐾)𝑊) → 𝑄(le‘𝐾)𝑊) |
5 | | dihatexv.b |
. . . . . . . . 9
⊢ 𝐵 = (Base‘𝐾) |
6 | | eqid 2622 |
. . . . . . . . 9
⊢
(le‘𝐾) =
(le‘𝐾) |
7 | | dihatexv.a |
. . . . . . . . 9
⊢ 𝐴 = (Atoms‘𝐾) |
8 | | dihatexv.h |
. . . . . . . . 9
⊢ 𝐻 = (LHyp‘𝐾) |
9 | | eqid 2622 |
. . . . . . . . 9
⊢
((LTrn‘𝐾)‘𝑊) = ((LTrn‘𝐾)‘𝑊) |
10 | | eqid 2622 |
. . . . . . . . 9
⊢ (𝑓 ∈ ((LTrn‘𝐾)‘𝑊) ↦ ( I ↾ 𝐵)) = (𝑓 ∈ ((LTrn‘𝐾)‘𝑊) ↦ ( I ↾ 𝐵)) |
11 | | dihatexv.u |
. . . . . . . . 9
⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊) |
12 | | dihatexv.i |
. . . . . . . . 9
⊢ 𝐼 = ((DIsoH‘𝐾)‘𝑊) |
13 | | dihatexv.n |
. . . . . . . . 9
⊢ 𝑁 = (LSpan‘𝑈) |
14 | 5, 6, 7, 8, 9, 10,
11, 12, 13 | dih1dimb2 36530 |
. . . . . . . 8
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑄 ∈ 𝐴 ∧ 𝑄(le‘𝐾)𝑊)) → ∃𝑔 ∈ ((LTrn‘𝐾)‘𝑊)(𝑔 ≠ ( I ↾ 𝐵) ∧ (𝐼‘𝑄) = (𝑁‘{〈𝑔, (𝑓 ∈ ((LTrn‘𝐾)‘𝑊) ↦ ( I ↾ 𝐵))〉}))) |
15 | 2, 3, 4, 14 | syl12anc 1324 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑄 ∈ 𝐴) ∧ 𝑄(le‘𝐾)𝑊) → ∃𝑔 ∈ ((LTrn‘𝐾)‘𝑊)(𝑔 ≠ ( I ↾ 𝐵) ∧ (𝐼‘𝑄) = (𝑁‘{〈𝑔, (𝑓 ∈ ((LTrn‘𝐾)‘𝑊) ↦ ( I ↾ 𝐵))〉}))) |
16 | 1 | ad3antrrr 766 |
. . . . . . . . . . . 12
⊢ ((((𝜑 ∧ 𝑄 ∈ 𝐴) ∧ 𝑄(le‘𝐾)𝑊) ∧ 𝑔 ∈ ((LTrn‘𝐾)‘𝑊)) → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻)) |
17 | | simpr 477 |
. . . . . . . . . . . 12
⊢ ((((𝜑 ∧ 𝑄 ∈ 𝐴) ∧ 𝑄(le‘𝐾)𝑊) ∧ 𝑔 ∈ ((LTrn‘𝐾)‘𝑊)) → 𝑔 ∈ ((LTrn‘𝐾)‘𝑊)) |
18 | | eqid 2622 |
. . . . . . . . . . . . . 14
⊢
((TEndo‘𝐾)‘𝑊) = ((TEndo‘𝐾)‘𝑊) |
19 | 5, 8, 9, 18, 10 | tendo0cl 36078 |
. . . . . . . . . . . . 13
⊢ ((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) → (𝑓 ∈ ((LTrn‘𝐾)‘𝑊) ↦ ( I ↾ 𝐵)) ∈ ((TEndo‘𝐾)‘𝑊)) |
20 | 16, 19 | syl 17 |
. . . . . . . . . . . 12
⊢ ((((𝜑 ∧ 𝑄 ∈ 𝐴) ∧ 𝑄(le‘𝐾)𝑊) ∧ 𝑔 ∈ ((LTrn‘𝐾)‘𝑊)) → (𝑓 ∈ ((LTrn‘𝐾)‘𝑊) ↦ ( I ↾ 𝐵)) ∈ ((TEndo‘𝐾)‘𝑊)) |
21 | | dihatexv.v |
. . . . . . . . . . . . 13
⊢ 𝑉 = (Base‘𝑈) |
22 | 8, 9, 18, 11, 21 | dvhelvbasei 36377 |
. . . . . . . . . . . 12
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑔 ∈ ((LTrn‘𝐾)‘𝑊) ∧ (𝑓 ∈ ((LTrn‘𝐾)‘𝑊) ↦ ( I ↾ 𝐵)) ∈ ((TEndo‘𝐾)‘𝑊))) → 〈𝑔, (𝑓 ∈ ((LTrn‘𝐾)‘𝑊) ↦ ( I ↾ 𝐵))〉 ∈ 𝑉) |
23 | 16, 17, 20, 22 | syl12anc 1324 |
. . . . . . . . . . 11
⊢ ((((𝜑 ∧ 𝑄 ∈ 𝐴) ∧ 𝑄(le‘𝐾)𝑊) ∧ 𝑔 ∈ ((LTrn‘𝐾)‘𝑊)) → 〈𝑔, (𝑓 ∈ ((LTrn‘𝐾)‘𝑊) ↦ ( I ↾ 𝐵))〉 ∈ 𝑉) |
24 | | sneq 4187 |
. . . . . . . . . . . . . 14
⊢ (𝑥 = 〈𝑔, (𝑓 ∈ ((LTrn‘𝐾)‘𝑊) ↦ ( I ↾ 𝐵))〉 → {𝑥} = {〈𝑔, (𝑓 ∈ ((LTrn‘𝐾)‘𝑊) ↦ ( I ↾ 𝐵))〉}) |
25 | 24 | fveq2d 6195 |
. . . . . . . . . . . . 13
⊢ (𝑥 = 〈𝑔, (𝑓 ∈ ((LTrn‘𝐾)‘𝑊) ↦ ( I ↾ 𝐵))〉 → (𝑁‘{𝑥}) = (𝑁‘{〈𝑔, (𝑓 ∈ ((LTrn‘𝐾)‘𝑊) ↦ ( I ↾ 𝐵))〉})) |
26 | 25 | eqeq2d 2632 |
. . . . . . . . . . . 12
⊢ (𝑥 = 〈𝑔, (𝑓 ∈ ((LTrn‘𝐾)‘𝑊) ↦ ( I ↾ 𝐵))〉 → ((𝐼‘𝑄) = (𝑁‘{𝑥}) ↔ (𝐼‘𝑄) = (𝑁‘{〈𝑔, (𝑓 ∈ ((LTrn‘𝐾)‘𝑊) ↦ ( I ↾ 𝐵))〉}))) |
27 | 26 | rspcev 3309 |
. . . . . . . . . . 11
⊢
((〈𝑔, (𝑓 ∈ ((LTrn‘𝐾)‘𝑊) ↦ ( I ↾ 𝐵))〉 ∈ 𝑉 ∧ (𝐼‘𝑄) = (𝑁‘{〈𝑔, (𝑓 ∈ ((LTrn‘𝐾)‘𝑊) ↦ ( I ↾ 𝐵))〉})) → ∃𝑥 ∈ 𝑉 (𝐼‘𝑄) = (𝑁‘{𝑥})) |
28 | 23, 27 | sylan 488 |
. . . . . . . . . 10
⊢
(((((𝜑 ∧ 𝑄 ∈ 𝐴) ∧ 𝑄(le‘𝐾)𝑊) ∧ 𝑔 ∈ ((LTrn‘𝐾)‘𝑊)) ∧ (𝐼‘𝑄) = (𝑁‘{〈𝑔, (𝑓 ∈ ((LTrn‘𝐾)‘𝑊) ↦ ( I ↾ 𝐵))〉})) → ∃𝑥 ∈ 𝑉 (𝐼‘𝑄) = (𝑁‘{𝑥})) |
29 | 28 | ex 450 |
. . . . . . . . 9
⊢ ((((𝜑 ∧ 𝑄 ∈ 𝐴) ∧ 𝑄(le‘𝐾)𝑊) ∧ 𝑔 ∈ ((LTrn‘𝐾)‘𝑊)) → ((𝐼‘𝑄) = (𝑁‘{〈𝑔, (𝑓 ∈ ((LTrn‘𝐾)‘𝑊) ↦ ( I ↾ 𝐵))〉}) → ∃𝑥 ∈ 𝑉 (𝐼‘𝑄) = (𝑁‘{𝑥}))) |
30 | 29 | adantld 483 |
. . . . . . . 8
⊢ ((((𝜑 ∧ 𝑄 ∈ 𝐴) ∧ 𝑄(le‘𝐾)𝑊) ∧ 𝑔 ∈ ((LTrn‘𝐾)‘𝑊)) → ((𝑔 ≠ ( I ↾ 𝐵) ∧ (𝐼‘𝑄) = (𝑁‘{〈𝑔, (𝑓 ∈ ((LTrn‘𝐾)‘𝑊) ↦ ( I ↾ 𝐵))〉})) → ∃𝑥 ∈ 𝑉 (𝐼‘𝑄) = (𝑁‘{𝑥}))) |
31 | 30 | rexlimdva 3031 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑄 ∈ 𝐴) ∧ 𝑄(le‘𝐾)𝑊) → (∃𝑔 ∈ ((LTrn‘𝐾)‘𝑊)(𝑔 ≠ ( I ↾ 𝐵) ∧ (𝐼‘𝑄) = (𝑁‘{〈𝑔, (𝑓 ∈ ((LTrn‘𝐾)‘𝑊) ↦ ( I ↾ 𝐵))〉})) → ∃𝑥 ∈ 𝑉 (𝐼‘𝑄) = (𝑁‘{𝑥}))) |
32 | 15, 31 | mpd 15 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑄 ∈ 𝐴) ∧ 𝑄(le‘𝐾)𝑊) → ∃𝑥 ∈ 𝑉 (𝐼‘𝑄) = (𝑁‘{𝑥})) |
33 | 1 | ad2antrr 762 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑄 ∈ 𝐴) ∧ ¬ 𝑄(le‘𝐾)𝑊) → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻)) |
34 | | eqid 2622 |
. . . . . . . . . . 11
⊢
((oc‘𝐾)‘𝑊) = ((oc‘𝐾)‘𝑊) |
35 | 6, 7, 8, 34 | lhpocnel2 35305 |
. . . . . . . . . 10
⊢ ((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) → (((oc‘𝐾)‘𝑊) ∈ 𝐴 ∧ ¬ ((oc‘𝐾)‘𝑊)(le‘𝐾)𝑊)) |
36 | 33, 35 | syl 17 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑄 ∈ 𝐴) ∧ ¬ 𝑄(le‘𝐾)𝑊) → (((oc‘𝐾)‘𝑊) ∈ 𝐴 ∧ ¬ ((oc‘𝐾)‘𝑊)(le‘𝐾)𝑊)) |
37 | | simplr 792 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑄 ∈ 𝐴) ∧ ¬ 𝑄(le‘𝐾)𝑊) → 𝑄 ∈ 𝐴) |
38 | | simpr 477 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑄 ∈ 𝐴) ∧ ¬ 𝑄(le‘𝐾)𝑊) → ¬ 𝑄(le‘𝐾)𝑊) |
39 | | eqid 2622 |
. . . . . . . . . 10
⊢
(℩𝑓
∈ ((LTrn‘𝐾)‘𝑊)(𝑓‘((oc‘𝐾)‘𝑊)) = 𝑄) = (℩𝑓 ∈ ((LTrn‘𝐾)‘𝑊)(𝑓‘((oc‘𝐾)‘𝑊)) = 𝑄) |
40 | 6, 7, 8, 9, 39 | ltrniotacl 35867 |
. . . . . . . . 9
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (((oc‘𝐾)‘𝑊) ∈ 𝐴 ∧ ¬ ((oc‘𝐾)‘𝑊)(le‘𝐾)𝑊) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄(le‘𝐾)𝑊)) → (℩𝑓 ∈ ((LTrn‘𝐾)‘𝑊)(𝑓‘((oc‘𝐾)‘𝑊)) = 𝑄) ∈ ((LTrn‘𝐾)‘𝑊)) |
41 | 33, 36, 37, 38, 40 | syl112anc 1330 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑄 ∈ 𝐴) ∧ ¬ 𝑄(le‘𝐾)𝑊) → (℩𝑓 ∈ ((LTrn‘𝐾)‘𝑊)(𝑓‘((oc‘𝐾)‘𝑊)) = 𝑄) ∈ ((LTrn‘𝐾)‘𝑊)) |
42 | 8, 9, 18 | tendoidcl 36057 |
. . . . . . . . 9
⊢ ((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) → ( I ↾ ((LTrn‘𝐾)‘𝑊)) ∈ ((TEndo‘𝐾)‘𝑊)) |
43 | 33, 42 | syl 17 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑄 ∈ 𝐴) ∧ ¬ 𝑄(le‘𝐾)𝑊) → ( I ↾ ((LTrn‘𝐾)‘𝑊)) ∈ ((TEndo‘𝐾)‘𝑊)) |
44 | 8, 9, 18, 11, 21 | dvhelvbasei 36377 |
. . . . . . . 8
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ ((℩𝑓 ∈ ((LTrn‘𝐾)‘𝑊)(𝑓‘((oc‘𝐾)‘𝑊)) = 𝑄) ∈ ((LTrn‘𝐾)‘𝑊) ∧ ( I ↾ ((LTrn‘𝐾)‘𝑊)) ∈ ((TEndo‘𝐾)‘𝑊))) → 〈(℩𝑓 ∈ ((LTrn‘𝐾)‘𝑊)(𝑓‘((oc‘𝐾)‘𝑊)) = 𝑄), ( I ↾ ((LTrn‘𝐾)‘𝑊))〉 ∈ 𝑉) |
45 | 33, 41, 43, 44 | syl12anc 1324 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑄 ∈ 𝐴) ∧ ¬ 𝑄(le‘𝐾)𝑊) → 〈(℩𝑓 ∈ ((LTrn‘𝐾)‘𝑊)(𝑓‘((oc‘𝐾)‘𝑊)) = 𝑄), ( I ↾ ((LTrn‘𝐾)‘𝑊))〉 ∈ 𝑉) |
46 | 6, 7, 8, 34, 9, 12, 11, 13, 39 | dih1dimc 36531 |
. . . . . . . 8
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄(le‘𝐾)𝑊)) → (𝐼‘𝑄) = (𝑁‘{〈(℩𝑓 ∈ ((LTrn‘𝐾)‘𝑊)(𝑓‘((oc‘𝐾)‘𝑊)) = 𝑄), ( I ↾ ((LTrn‘𝐾)‘𝑊))〉})) |
47 | 33, 37, 38, 46 | syl12anc 1324 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑄 ∈ 𝐴) ∧ ¬ 𝑄(le‘𝐾)𝑊) → (𝐼‘𝑄) = (𝑁‘{〈(℩𝑓 ∈ ((LTrn‘𝐾)‘𝑊)(𝑓‘((oc‘𝐾)‘𝑊)) = 𝑄), ( I ↾ ((LTrn‘𝐾)‘𝑊))〉})) |
48 | | sneq 4187 |
. . . . . . . . . 10
⊢ (𝑥 = 〈(℩𝑓 ∈ ((LTrn‘𝐾)‘𝑊)(𝑓‘((oc‘𝐾)‘𝑊)) = 𝑄), ( I ↾ ((LTrn‘𝐾)‘𝑊))〉 → {𝑥} = {〈(℩𝑓 ∈ ((LTrn‘𝐾)‘𝑊)(𝑓‘((oc‘𝐾)‘𝑊)) = 𝑄), ( I ↾ ((LTrn‘𝐾)‘𝑊))〉}) |
49 | 48 | fveq2d 6195 |
. . . . . . . . 9
⊢ (𝑥 = 〈(℩𝑓 ∈ ((LTrn‘𝐾)‘𝑊)(𝑓‘((oc‘𝐾)‘𝑊)) = 𝑄), ( I ↾ ((LTrn‘𝐾)‘𝑊))〉 → (𝑁‘{𝑥}) = (𝑁‘{〈(℩𝑓 ∈ ((LTrn‘𝐾)‘𝑊)(𝑓‘((oc‘𝐾)‘𝑊)) = 𝑄), ( I ↾ ((LTrn‘𝐾)‘𝑊))〉})) |
50 | 49 | eqeq2d 2632 |
. . . . . . . 8
⊢ (𝑥 = 〈(℩𝑓 ∈ ((LTrn‘𝐾)‘𝑊)(𝑓‘((oc‘𝐾)‘𝑊)) = 𝑄), ( I ↾ ((LTrn‘𝐾)‘𝑊))〉 → ((𝐼‘𝑄) = (𝑁‘{𝑥}) ↔ (𝐼‘𝑄) = (𝑁‘{〈(℩𝑓 ∈ ((LTrn‘𝐾)‘𝑊)(𝑓‘((oc‘𝐾)‘𝑊)) = 𝑄), ( I ↾ ((LTrn‘𝐾)‘𝑊))〉}))) |
51 | 50 | rspcev 3309 |
. . . . . . 7
⊢
((〈(℩𝑓 ∈ ((LTrn‘𝐾)‘𝑊)(𝑓‘((oc‘𝐾)‘𝑊)) = 𝑄), ( I ↾ ((LTrn‘𝐾)‘𝑊))〉 ∈ 𝑉 ∧ (𝐼‘𝑄) = (𝑁‘{〈(℩𝑓 ∈ ((LTrn‘𝐾)‘𝑊)(𝑓‘((oc‘𝐾)‘𝑊)) = 𝑄), ( I ↾ ((LTrn‘𝐾)‘𝑊))〉})) → ∃𝑥 ∈ 𝑉 (𝐼‘𝑄) = (𝑁‘{𝑥})) |
52 | 45, 47, 51 | syl2anc 693 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑄 ∈ 𝐴) ∧ ¬ 𝑄(le‘𝐾)𝑊) → ∃𝑥 ∈ 𝑉 (𝐼‘𝑄) = (𝑁‘{𝑥})) |
53 | 32, 52 | pm2.61dan 832 |
. . . . 5
⊢ ((𝜑 ∧ 𝑄 ∈ 𝐴) → ∃𝑥 ∈ 𝑉 (𝐼‘𝑄) = (𝑁‘{𝑥})) |
54 | 1 | simpld 475 |
. . . . . . . . . . . 12
⊢ (𝜑 → 𝐾 ∈ HL) |
55 | 54 | ad3antrrr 766 |
. . . . . . . . . . 11
⊢ ((((𝜑 ∧ 𝑄 ∈ 𝐴) ∧ 𝑥 ∈ 𝑉) ∧ (𝐼‘𝑄) = (𝑁‘{𝑥})) → 𝐾 ∈ HL) |
56 | | hlatl 34647 |
. . . . . . . . . . 11
⊢ (𝐾 ∈ HL → 𝐾 ∈ AtLat) |
57 | 55, 56 | syl 17 |
. . . . . . . . . 10
⊢ ((((𝜑 ∧ 𝑄 ∈ 𝐴) ∧ 𝑥 ∈ 𝑉) ∧ (𝐼‘𝑄) = (𝑁‘{𝑥})) → 𝐾 ∈ AtLat) |
58 | | simpllr 799 |
. . . . . . . . . 10
⊢ ((((𝜑 ∧ 𝑄 ∈ 𝐴) ∧ 𝑥 ∈ 𝑉) ∧ (𝐼‘𝑄) = (𝑁‘{𝑥})) → 𝑄 ∈ 𝐴) |
59 | | eqid 2622 |
. . . . . . . . . . 11
⊢
(0.‘𝐾) =
(0.‘𝐾) |
60 | 59, 7 | atn0 34595 |
. . . . . . . . . 10
⊢ ((𝐾 ∈ AtLat ∧ 𝑄 ∈ 𝐴) → 𝑄 ≠ (0.‘𝐾)) |
61 | 57, 58, 60 | syl2anc 693 |
. . . . . . . . 9
⊢ ((((𝜑 ∧ 𝑄 ∈ 𝐴) ∧ 𝑥 ∈ 𝑉) ∧ (𝐼‘𝑄) = (𝑁‘{𝑥})) → 𝑄 ≠ (0.‘𝐾)) |
62 | | sneq 4187 |
. . . . . . . . . . . . . . . 16
⊢ (𝑥 = 0 → {𝑥} = { 0 }) |
63 | 62 | fveq2d 6195 |
. . . . . . . . . . . . . . 15
⊢ (𝑥 = 0 → (𝑁‘{𝑥}) = (𝑁‘{ 0 })) |
64 | 63 | 3ad2ant3 1084 |
. . . . . . . . . . . . . 14
⊢ ((((𝜑 ∧ 𝑄 ∈ 𝐴) ∧ 𝑥 ∈ 𝑉) ∧ (𝐼‘𝑄) = (𝑁‘{𝑥}) ∧ 𝑥 = 0 ) → (𝑁‘{𝑥}) = (𝑁‘{ 0 })) |
65 | | simp1ll 1124 |
. . . . . . . . . . . . . . 15
⊢ ((((𝜑 ∧ 𝑄 ∈ 𝐴) ∧ 𝑥 ∈ 𝑉) ∧ (𝐼‘𝑄) = (𝑁‘{𝑥}) ∧ 𝑥 = 0 ) → 𝜑) |
66 | 8, 11, 1 | dvhlmod 36399 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → 𝑈 ∈ LMod) |
67 | | dihatexv.o |
. . . . . . . . . . . . . . . 16
⊢ 0 =
(0g‘𝑈) |
68 | 67, 13 | lspsn0 19008 |
. . . . . . . . . . . . . . 15
⊢ (𝑈 ∈ LMod → (𝑁‘{ 0 }) = { 0 }) |
69 | 65, 66, 68 | 3syl 18 |
. . . . . . . . . . . . . 14
⊢ ((((𝜑 ∧ 𝑄 ∈ 𝐴) ∧ 𝑥 ∈ 𝑉) ∧ (𝐼‘𝑄) = (𝑁‘{𝑥}) ∧ 𝑥 = 0 ) → (𝑁‘{ 0 }) = { 0 }) |
70 | 64, 69 | eqtrd 2656 |
. . . . . . . . . . . . 13
⊢ ((((𝜑 ∧ 𝑄 ∈ 𝐴) ∧ 𝑥 ∈ 𝑉) ∧ (𝐼‘𝑄) = (𝑁‘{𝑥}) ∧ 𝑥 = 0 ) → (𝑁‘{𝑥}) = { 0 }) |
71 | | simp2 1062 |
. . . . . . . . . . . . 13
⊢ ((((𝜑 ∧ 𝑄 ∈ 𝐴) ∧ 𝑥 ∈ 𝑉) ∧ (𝐼‘𝑄) = (𝑁‘{𝑥}) ∧ 𝑥 = 0 ) → (𝐼‘𝑄) = (𝑁‘{𝑥})) |
72 | 59, 8, 12, 11, 67 | dih0 36569 |
. . . . . . . . . . . . . 14
⊢ ((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) → (𝐼‘(0.‘𝐾)) = { 0 }) |
73 | 65, 1, 72 | 3syl 18 |
. . . . . . . . . . . . 13
⊢ ((((𝜑 ∧ 𝑄 ∈ 𝐴) ∧ 𝑥 ∈ 𝑉) ∧ (𝐼‘𝑄) = (𝑁‘{𝑥}) ∧ 𝑥 = 0 ) → (𝐼‘(0.‘𝐾)) = { 0 }) |
74 | 70, 71, 73 | 3eqtr4d 2666 |
. . . . . . . . . . . 12
⊢ ((((𝜑 ∧ 𝑄 ∈ 𝐴) ∧ 𝑥 ∈ 𝑉) ∧ (𝐼‘𝑄) = (𝑁‘{𝑥}) ∧ 𝑥 = 0 ) → (𝐼‘𝑄) = (𝐼‘(0.‘𝐾))) |
75 | 65, 1 | syl 17 |
. . . . . . . . . . . . 13
⊢ ((((𝜑 ∧ 𝑄 ∈ 𝐴) ∧ 𝑥 ∈ 𝑉) ∧ (𝐼‘𝑄) = (𝑁‘{𝑥}) ∧ 𝑥 = 0 ) → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻)) |
76 | | dihatexv.q |
. . . . . . . . . . . . . 14
⊢ (𝜑 → 𝑄 ∈ 𝐵) |
77 | 65, 76 | syl 17 |
. . . . . . . . . . . . 13
⊢ ((((𝜑 ∧ 𝑄 ∈ 𝐴) ∧ 𝑥 ∈ 𝑉) ∧ (𝐼‘𝑄) = (𝑁‘{𝑥}) ∧ 𝑥 = 0 ) → 𝑄 ∈ 𝐵) |
78 | 65, 54 | syl 17 |
. . . . . . . . . . . . . 14
⊢ ((((𝜑 ∧ 𝑄 ∈ 𝐴) ∧ 𝑥 ∈ 𝑉) ∧ (𝐼‘𝑄) = (𝑁‘{𝑥}) ∧ 𝑥 = 0 ) → 𝐾 ∈ HL) |
79 | | hlop 34649 |
. . . . . . . . . . . . . 14
⊢ (𝐾 ∈ HL → 𝐾 ∈ OP) |
80 | 5, 59 | op0cl 34471 |
. . . . . . . . . . . . . 14
⊢ (𝐾 ∈ OP →
(0.‘𝐾) ∈ 𝐵) |
81 | 78, 79, 80 | 3syl 18 |
. . . . . . . . . . . . 13
⊢ ((((𝜑 ∧ 𝑄 ∈ 𝐴) ∧ 𝑥 ∈ 𝑉) ∧ (𝐼‘𝑄) = (𝑁‘{𝑥}) ∧ 𝑥 = 0 ) → (0.‘𝐾) ∈ 𝐵) |
82 | 5, 8, 12 | dih11 36554 |
. . . . . . . . . . . . 13
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝑄 ∈ 𝐵 ∧ (0.‘𝐾) ∈ 𝐵) → ((𝐼‘𝑄) = (𝐼‘(0.‘𝐾)) ↔ 𝑄 = (0.‘𝐾))) |
83 | 75, 77, 81, 82 | syl3anc 1326 |
. . . . . . . . . . . 12
⊢ ((((𝜑 ∧ 𝑄 ∈ 𝐴) ∧ 𝑥 ∈ 𝑉) ∧ (𝐼‘𝑄) = (𝑁‘{𝑥}) ∧ 𝑥 = 0 ) → ((𝐼‘𝑄) = (𝐼‘(0.‘𝐾)) ↔ 𝑄 = (0.‘𝐾))) |
84 | 74, 83 | mpbid 222 |
. . . . . . . . . . 11
⊢ ((((𝜑 ∧ 𝑄 ∈ 𝐴) ∧ 𝑥 ∈ 𝑉) ∧ (𝐼‘𝑄) = (𝑁‘{𝑥}) ∧ 𝑥 = 0 ) → 𝑄 = (0.‘𝐾)) |
85 | 84 | 3expia 1267 |
. . . . . . . . . 10
⊢ ((((𝜑 ∧ 𝑄 ∈ 𝐴) ∧ 𝑥 ∈ 𝑉) ∧ (𝐼‘𝑄) = (𝑁‘{𝑥})) → (𝑥 = 0 → 𝑄 = (0.‘𝐾))) |
86 | 85 | necon3d 2815 |
. . . . . . . . 9
⊢ ((((𝜑 ∧ 𝑄 ∈ 𝐴) ∧ 𝑥 ∈ 𝑉) ∧ (𝐼‘𝑄) = (𝑁‘{𝑥})) → (𝑄 ≠ (0.‘𝐾) → 𝑥 ≠ 0 )) |
87 | 61, 86 | mpd 15 |
. . . . . . . 8
⊢ ((((𝜑 ∧ 𝑄 ∈ 𝐴) ∧ 𝑥 ∈ 𝑉) ∧ (𝐼‘𝑄) = (𝑁‘{𝑥})) → 𝑥 ≠ 0 ) |
88 | 87 | ex 450 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑄 ∈ 𝐴) ∧ 𝑥 ∈ 𝑉) → ((𝐼‘𝑄) = (𝑁‘{𝑥}) → 𝑥 ≠ 0 )) |
89 | 88 | ancrd 577 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑄 ∈ 𝐴) ∧ 𝑥 ∈ 𝑉) → ((𝐼‘𝑄) = (𝑁‘{𝑥}) → (𝑥 ≠ 0 ∧ (𝐼‘𝑄) = (𝑁‘{𝑥})))) |
90 | 89 | reximdva 3017 |
. . . . 5
⊢ ((𝜑 ∧ 𝑄 ∈ 𝐴) → (∃𝑥 ∈ 𝑉 (𝐼‘𝑄) = (𝑁‘{𝑥}) → ∃𝑥 ∈ 𝑉 (𝑥 ≠ 0 ∧ (𝐼‘𝑄) = (𝑁‘{𝑥})))) |
91 | 53, 90 | mpd 15 |
. . . 4
⊢ ((𝜑 ∧ 𝑄 ∈ 𝐴) → ∃𝑥 ∈ 𝑉 (𝑥 ≠ 0 ∧ (𝐼‘𝑄) = (𝑁‘{𝑥}))) |
92 | 91 | ex 450 |
. . 3
⊢ (𝜑 → (𝑄 ∈ 𝐴 → ∃𝑥 ∈ 𝑉 (𝑥 ≠ 0 ∧ (𝐼‘𝑄) = (𝑁‘{𝑥})))) |
93 | 1 | ad2antrr 762 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑥 ∈ 𝑉) ∧ (𝑥 ≠ 0 ∧ (𝐼‘𝑄) = (𝑁‘{𝑥}))) → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻)) |
94 | 76 | ad2antrr 762 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑥 ∈ 𝑉) ∧ (𝑥 ≠ 0 ∧ (𝐼‘𝑄) = (𝑁‘{𝑥}))) → 𝑄 ∈ 𝐵) |
95 | 5, 8, 12 | dihcnvid1 36561 |
. . . . . . . 8
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝑄 ∈ 𝐵) → (◡𝐼‘(𝐼‘𝑄)) = 𝑄) |
96 | 93, 94, 95 | syl2anc 693 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑥 ∈ 𝑉) ∧ (𝑥 ≠ 0 ∧ (𝐼‘𝑄) = (𝑁‘{𝑥}))) → (◡𝐼‘(𝐼‘𝑄)) = 𝑄) |
97 | | fveq2 6191 |
. . . . . . . 8
⊢ ((𝐼‘𝑄) = (𝑁‘{𝑥}) → (◡𝐼‘(𝐼‘𝑄)) = (◡𝐼‘(𝑁‘{𝑥}))) |
98 | 97 | ad2antll 765 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑥 ∈ 𝑉) ∧ (𝑥 ≠ 0 ∧ (𝐼‘𝑄) = (𝑁‘{𝑥}))) → (◡𝐼‘(𝐼‘𝑄)) = (◡𝐼‘(𝑁‘{𝑥}))) |
99 | 96, 98 | eqtr3d 2658 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑥 ∈ 𝑉) ∧ (𝑥 ≠ 0 ∧ (𝐼‘𝑄) = (𝑁‘{𝑥}))) → 𝑄 = (◡𝐼‘(𝑁‘{𝑥}))) |
100 | 66 | ad2antrr 762 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑥 ∈ 𝑉) ∧ (𝑥 ≠ 0 ∧ (𝐼‘𝑄) = (𝑁‘{𝑥}))) → 𝑈 ∈ LMod) |
101 | | simplr 792 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑥 ∈ 𝑉) ∧ (𝑥 ≠ 0 ∧ (𝐼‘𝑄) = (𝑁‘{𝑥}))) → 𝑥 ∈ 𝑉) |
102 | | simprl 794 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑥 ∈ 𝑉) ∧ (𝑥 ≠ 0 ∧ (𝐼‘𝑄) = (𝑁‘{𝑥}))) → 𝑥 ≠ 0 ) |
103 | | eqid 2622 |
. . . . . . . . 9
⊢
(LSAtoms‘𝑈) =
(LSAtoms‘𝑈) |
104 | 21, 13, 67, 103 | lsatlspsn2 34279 |
. . . . . . . 8
⊢ ((𝑈 ∈ LMod ∧ 𝑥 ∈ 𝑉 ∧ 𝑥 ≠ 0 ) → (𝑁‘{𝑥}) ∈ (LSAtoms‘𝑈)) |
105 | 100, 101,
102, 104 | syl3anc 1326 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑥 ∈ 𝑉) ∧ (𝑥 ≠ 0 ∧ (𝐼‘𝑄) = (𝑁‘{𝑥}))) → (𝑁‘{𝑥}) ∈ (LSAtoms‘𝑈)) |
106 | 7, 8, 11, 12, 103 | dihlatat 36626 |
. . . . . . 7
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑁‘{𝑥}) ∈ (LSAtoms‘𝑈)) → (◡𝐼‘(𝑁‘{𝑥})) ∈ 𝐴) |
107 | 93, 105, 106 | syl2anc 693 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑥 ∈ 𝑉) ∧ (𝑥 ≠ 0 ∧ (𝐼‘𝑄) = (𝑁‘{𝑥}))) → (◡𝐼‘(𝑁‘{𝑥})) ∈ 𝐴) |
108 | 99, 107 | eqeltrd 2701 |
. . . . 5
⊢ (((𝜑 ∧ 𝑥 ∈ 𝑉) ∧ (𝑥 ≠ 0 ∧ (𝐼‘𝑄) = (𝑁‘{𝑥}))) → 𝑄 ∈ 𝐴) |
109 | 108 | ex 450 |
. . . 4
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑉) → ((𝑥 ≠ 0 ∧ (𝐼‘𝑄) = (𝑁‘{𝑥})) → 𝑄 ∈ 𝐴)) |
110 | 109 | rexlimdva 3031 |
. . 3
⊢ (𝜑 → (∃𝑥 ∈ 𝑉 (𝑥 ≠ 0 ∧ (𝐼‘𝑄) = (𝑁‘{𝑥})) → 𝑄 ∈ 𝐴)) |
111 | 92, 110 | impbid 202 |
. 2
⊢ (𝜑 → (𝑄 ∈ 𝐴 ↔ ∃𝑥 ∈ 𝑉 (𝑥 ≠ 0 ∧ (𝐼‘𝑄) = (𝑁‘{𝑥})))) |
112 | | rexdifsn 4323 |
. 2
⊢
(∃𝑥 ∈
(𝑉 ∖ { 0 })(𝐼‘𝑄) = (𝑁‘{𝑥}) ↔ ∃𝑥 ∈ 𝑉 (𝑥 ≠ 0 ∧ (𝐼‘𝑄) = (𝑁‘{𝑥}))) |
113 | 111, 112 | syl6bbr 278 |
1
⊢ (𝜑 → (𝑄 ∈ 𝐴 ↔ ∃𝑥 ∈ (𝑉 ∖ { 0 })(𝐼‘𝑄) = (𝑁‘{𝑥}))) |