Step | Hyp | Ref
| Expression |
1 | | lcv1.q |
. . . . 5
⊢ (𝜑 → 𝑄 ∈ 𝐴) |
2 | | lcv1.w |
. . . . . 6
⊢ (𝜑 → 𝑊 ∈ LVec) |
3 | | eqid 2795 |
. . . . . . 7
⊢
(Base‘𝑊) =
(Base‘𝑊) |
4 | | eqid 2795 |
. . . . . . 7
⊢
(LSpan‘𝑊) =
(LSpan‘𝑊) |
5 | | eqid 2795 |
. . . . . . 7
⊢
(0g‘𝑊) = (0g‘𝑊) |
6 | | lcv1.a |
. . . . . . 7
⊢ 𝐴 = (LSAtoms‘𝑊) |
7 | 3, 4, 5, 6 | islsat 35658 |
. . . . . 6
⊢ (𝑊 ∈ LVec → (𝑄 ∈ 𝐴 ↔ ∃𝑥 ∈ ((Base‘𝑊) ∖ {(0g‘𝑊)})𝑄 = ((LSpan‘𝑊)‘{𝑥}))) |
8 | 2, 7 | syl 17 |
. . . . 5
⊢ (𝜑 → (𝑄 ∈ 𝐴 ↔ ∃𝑥 ∈ ((Base‘𝑊) ∖ {(0g‘𝑊)})𝑄 = ((LSpan‘𝑊)‘{𝑥}))) |
9 | 1, 8 | mpbid 233 |
. . . 4
⊢ (𝜑 → ∃𝑥 ∈ ((Base‘𝑊) ∖ {(0g‘𝑊)})𝑄 = ((LSpan‘𝑊)‘{𝑥})) |
10 | 9 | adantr 481 |
. . 3
⊢ ((𝜑 ∧ ¬ 𝑄 ⊆ 𝑈) → ∃𝑥 ∈ ((Base‘𝑊) ∖ {(0g‘𝑊)})𝑄 = ((LSpan‘𝑊)‘{𝑥})) |
11 | | lcv1.s |
. . . . . 6
⊢ 𝑆 = (LSubSp‘𝑊) |
12 | | lcv1.p |
. . . . . 6
⊢ ⊕ =
(LSSum‘𝑊) |
13 | | lcv1.c |
. . . . . 6
⊢ 𝐶 = ( ⋖L
‘𝑊) |
14 | 2 | adantr 481 |
. . . . . . 7
⊢ ((𝜑 ∧ ¬ 𝑄 ⊆ 𝑈) → 𝑊 ∈ LVec) |
15 | 14 | 3ad2ant1 1126 |
. . . . . 6
⊢ (((𝜑 ∧ ¬ 𝑄 ⊆ 𝑈) ∧ 𝑥 ∈ ((Base‘𝑊) ∖ {(0g‘𝑊)}) ∧ 𝑄 = ((LSpan‘𝑊)‘{𝑥})) → 𝑊 ∈ LVec) |
16 | | lcv1.u |
. . . . . . . 8
⊢ (𝜑 → 𝑈 ∈ 𝑆) |
17 | 16 | adantr 481 |
. . . . . . 7
⊢ ((𝜑 ∧ ¬ 𝑄 ⊆ 𝑈) → 𝑈 ∈ 𝑆) |
18 | 17 | 3ad2ant1 1126 |
. . . . . 6
⊢ (((𝜑 ∧ ¬ 𝑄 ⊆ 𝑈) ∧ 𝑥 ∈ ((Base‘𝑊) ∖ {(0g‘𝑊)}) ∧ 𝑄 = ((LSpan‘𝑊)‘{𝑥})) → 𝑈 ∈ 𝑆) |
19 | | eldifi 4024 |
. . . . . . 7
⊢ (𝑥 ∈ ((Base‘𝑊) ∖
{(0g‘𝑊)})
→ 𝑥 ∈
(Base‘𝑊)) |
20 | 19 | 3ad2ant2 1127 |
. . . . . 6
⊢ (((𝜑 ∧ ¬ 𝑄 ⊆ 𝑈) ∧ 𝑥 ∈ ((Base‘𝑊) ∖ {(0g‘𝑊)}) ∧ 𝑄 = ((LSpan‘𝑊)‘{𝑥})) → 𝑥 ∈ (Base‘𝑊)) |
21 | | simp1r 1191 |
. . . . . . 7
⊢ (((𝜑 ∧ ¬ 𝑄 ⊆ 𝑈) ∧ 𝑥 ∈ ((Base‘𝑊) ∖ {(0g‘𝑊)}) ∧ 𝑄 = ((LSpan‘𝑊)‘{𝑥})) → ¬ 𝑄 ⊆ 𝑈) |
22 | | simp3 1131 |
. . . . . . . 8
⊢ (((𝜑 ∧ ¬ 𝑄 ⊆ 𝑈) ∧ 𝑥 ∈ ((Base‘𝑊) ∖ {(0g‘𝑊)}) ∧ 𝑄 = ((LSpan‘𝑊)‘{𝑥})) → 𝑄 = ((LSpan‘𝑊)‘{𝑥})) |
23 | 22 | sseq1d 3919 |
. . . . . . 7
⊢ (((𝜑 ∧ ¬ 𝑄 ⊆ 𝑈) ∧ 𝑥 ∈ ((Base‘𝑊) ∖ {(0g‘𝑊)}) ∧ 𝑄 = ((LSpan‘𝑊)‘{𝑥})) → (𝑄 ⊆ 𝑈 ↔ ((LSpan‘𝑊)‘{𝑥}) ⊆ 𝑈)) |
24 | 21, 23 | mtbid 325 |
. . . . . 6
⊢ (((𝜑 ∧ ¬ 𝑄 ⊆ 𝑈) ∧ 𝑥 ∈ ((Base‘𝑊) ∖ {(0g‘𝑊)}) ∧ 𝑄 = ((LSpan‘𝑊)‘{𝑥})) → ¬ ((LSpan‘𝑊)‘{𝑥}) ⊆ 𝑈) |
25 | 3, 11, 4, 12, 13, 15, 18, 20, 24 | lsmcv2 35696 |
. . . . 5
⊢ (((𝜑 ∧ ¬ 𝑄 ⊆ 𝑈) ∧ 𝑥 ∈ ((Base‘𝑊) ∖ {(0g‘𝑊)}) ∧ 𝑄 = ((LSpan‘𝑊)‘{𝑥})) → 𝑈𝐶(𝑈 ⊕ ((LSpan‘𝑊)‘{𝑥}))) |
26 | 22 | oveq2d 7032 |
. . . . 5
⊢ (((𝜑 ∧ ¬ 𝑄 ⊆ 𝑈) ∧ 𝑥 ∈ ((Base‘𝑊) ∖ {(0g‘𝑊)}) ∧ 𝑄 = ((LSpan‘𝑊)‘{𝑥})) → (𝑈 ⊕ 𝑄) = (𝑈 ⊕ ((LSpan‘𝑊)‘{𝑥}))) |
27 | 25, 26 | breqtrrd 4990 |
. . . 4
⊢ (((𝜑 ∧ ¬ 𝑄 ⊆ 𝑈) ∧ 𝑥 ∈ ((Base‘𝑊) ∖ {(0g‘𝑊)}) ∧ 𝑄 = ((LSpan‘𝑊)‘{𝑥})) → 𝑈𝐶(𝑈 ⊕ 𝑄)) |
28 | 27 | rexlimdv3a 3249 |
. . 3
⊢ ((𝜑 ∧ ¬ 𝑄 ⊆ 𝑈) → (∃𝑥 ∈ ((Base‘𝑊) ∖ {(0g‘𝑊)})𝑄 = ((LSpan‘𝑊)‘{𝑥}) → 𝑈𝐶(𝑈 ⊕ 𝑄))) |
29 | 10, 28 | mpd 15 |
. 2
⊢ ((𝜑 ∧ ¬ 𝑄 ⊆ 𝑈) → 𝑈𝐶(𝑈 ⊕ 𝑄)) |
30 | 2 | adantr 481 |
. . . 4
⊢ ((𝜑 ∧ 𝑈𝐶(𝑈 ⊕ 𝑄)) → 𝑊 ∈ LVec) |
31 | 16 | adantr 481 |
. . . 4
⊢ ((𝜑 ∧ 𝑈𝐶(𝑈 ⊕ 𝑄)) → 𝑈 ∈ 𝑆) |
32 | | lveclmod 19568 |
. . . . . . 7
⊢ (𝑊 ∈ LVec → 𝑊 ∈ LMod) |
33 | 2, 32 | syl 17 |
. . . . . 6
⊢ (𝜑 → 𝑊 ∈ LMod) |
34 | 11, 6, 33, 1 | lsatlssel 35664 |
. . . . . 6
⊢ (𝜑 → 𝑄 ∈ 𝑆) |
35 | 11, 12 | lsmcl 19545 |
. . . . . 6
⊢ ((𝑊 ∈ LMod ∧ 𝑈 ∈ 𝑆 ∧ 𝑄 ∈ 𝑆) → (𝑈 ⊕ 𝑄) ∈ 𝑆) |
36 | 33, 16, 34, 35 | syl3anc 1364 |
. . . . 5
⊢ (𝜑 → (𝑈 ⊕ 𝑄) ∈ 𝑆) |
37 | 36 | adantr 481 |
. . . 4
⊢ ((𝜑 ∧ 𝑈𝐶(𝑈 ⊕ 𝑄)) → (𝑈 ⊕ 𝑄) ∈ 𝑆) |
38 | | simpr 485 |
. . . 4
⊢ ((𝜑 ∧ 𝑈𝐶(𝑈 ⊕ 𝑄)) → 𝑈𝐶(𝑈 ⊕ 𝑄)) |
39 | 11, 13, 30, 31, 37, 38 | lcvpss 35691 |
. . 3
⊢ ((𝜑 ∧ 𝑈𝐶(𝑈 ⊕ 𝑄)) → 𝑈 ⊊ (𝑈 ⊕ 𝑄)) |
40 | 11 | lsssssubg 19420 |
. . . . . . 7
⊢ (𝑊 ∈ LMod → 𝑆 ⊆ (SubGrp‘𝑊)) |
41 | 33, 40 | syl 17 |
. . . . . 6
⊢ (𝜑 → 𝑆 ⊆ (SubGrp‘𝑊)) |
42 | 41, 16 | sseldd 3890 |
. . . . 5
⊢ (𝜑 → 𝑈 ∈ (SubGrp‘𝑊)) |
43 | 41, 34 | sseldd 3890 |
. . . . 5
⊢ (𝜑 → 𝑄 ∈ (SubGrp‘𝑊)) |
44 | 12, 42, 43 | lssnle 18527 |
. . . 4
⊢ (𝜑 → (¬ 𝑄 ⊆ 𝑈 ↔ 𝑈 ⊊ (𝑈 ⊕ 𝑄))) |
45 | 44 | adantr 481 |
. . 3
⊢ ((𝜑 ∧ 𝑈𝐶(𝑈 ⊕ 𝑄)) → (¬ 𝑄 ⊆ 𝑈 ↔ 𝑈 ⊊ (𝑈 ⊕ 𝑄))) |
46 | 39, 45 | mpbird 258 |
. 2
⊢ ((𝜑 ∧ 𝑈𝐶(𝑈 ⊕ 𝑄)) → ¬ 𝑄 ⊆ 𝑈) |
47 | 29, 46 | impbida 797 |
1
⊢ (𝜑 → (¬ 𝑄 ⊆ 𝑈 ↔ 𝑈𝐶(𝑈 ⊕ 𝑄))) |