Step | Hyp | Ref
| Expression |
1 | | eqid 2610 |
. . . . . . 7
⊢
(0g‘𝑊) = (0g‘𝑊) |
2 | 1 | obsne0 19888 |
. . . . . 6
⊢ ((𝐵 ∈ (OBasis‘𝑊) ∧ 𝐴 ∈ 𝐵) → 𝐴 ≠ (0g‘𝑊)) |
3 | 2 | 3adant2 1073 |
. . . . 5
⊢ ((𝐵 ∈ (OBasis‘𝑊) ∧ 𝐶 ⊆ 𝐵 ∧ 𝐴 ∈ 𝐵) → 𝐴 ≠ (0g‘𝑊)) |
4 | | elin 3758 |
. . . . . . . 8
⊢ (𝐴 ∈ (𝐶 ∩ ( ⊥ ‘𝐶)) ↔ (𝐴 ∈ 𝐶 ∧ 𝐴 ∈ ( ⊥ ‘𝐶))) |
5 | | obsrcl 19886 |
. . . . . . . . . . . . . 14
⊢ (𝐵 ∈ (OBasis‘𝑊) → 𝑊 ∈ PreHil) |
6 | 5 | 3ad2ant1 1075 |
. . . . . . . . . . . . 13
⊢ ((𝐵 ∈ (OBasis‘𝑊) ∧ 𝐶 ⊆ 𝐵 ∧ 𝐴 ∈ 𝐵) → 𝑊 ∈ PreHil) |
7 | | phllmod 19794 |
. . . . . . . . . . . . 13
⊢ (𝑊 ∈ PreHil → 𝑊 ∈ LMod) |
8 | 6, 7 | syl 17 |
. . . . . . . . . . . 12
⊢ ((𝐵 ∈ (OBasis‘𝑊) ∧ 𝐶 ⊆ 𝐵 ∧ 𝐴 ∈ 𝐵) → 𝑊 ∈ LMod) |
9 | | simp2 1055 |
. . . . . . . . . . . . 13
⊢ ((𝐵 ∈ (OBasis‘𝑊) ∧ 𝐶 ⊆ 𝐵 ∧ 𝐴 ∈ 𝐵) → 𝐶 ⊆ 𝐵) |
10 | | eqid 2610 |
. . . . . . . . . . . . . . 15
⊢
(Base‘𝑊) =
(Base‘𝑊) |
11 | 10 | obsss 19887 |
. . . . . . . . . . . . . 14
⊢ (𝐵 ∈ (OBasis‘𝑊) → 𝐵 ⊆ (Base‘𝑊)) |
12 | 11 | 3ad2ant1 1075 |
. . . . . . . . . . . . 13
⊢ ((𝐵 ∈ (OBasis‘𝑊) ∧ 𝐶 ⊆ 𝐵 ∧ 𝐴 ∈ 𝐵) → 𝐵 ⊆ (Base‘𝑊)) |
13 | 9, 12 | sstrd 3578 |
. . . . . . . . . . . 12
⊢ ((𝐵 ∈ (OBasis‘𝑊) ∧ 𝐶 ⊆ 𝐵 ∧ 𝐴 ∈ 𝐵) → 𝐶 ⊆ (Base‘𝑊)) |
14 | | eqid 2610 |
. . . . . . . . . . . . 13
⊢
(LSpan‘𝑊) =
(LSpan‘𝑊) |
15 | 10, 14 | lspssid 18806 |
. . . . . . . . . . . 12
⊢ ((𝑊 ∈ LMod ∧ 𝐶 ⊆ (Base‘𝑊)) → 𝐶 ⊆ ((LSpan‘𝑊)‘𝐶)) |
16 | 8, 13, 15 | syl2anc 691 |
. . . . . . . . . . 11
⊢ ((𝐵 ∈ (OBasis‘𝑊) ∧ 𝐶 ⊆ 𝐵 ∧ 𝐴 ∈ 𝐵) → 𝐶 ⊆ ((LSpan‘𝑊)‘𝐶)) |
17 | | ssrin 3800 |
. . . . . . . . . . 11
⊢ (𝐶 ⊆ ((LSpan‘𝑊)‘𝐶) → (𝐶 ∩ ( ⊥ ‘𝐶)) ⊆ (((LSpan‘𝑊)‘𝐶) ∩ ( ⊥ ‘𝐶))) |
18 | 16, 17 | syl 17 |
. . . . . . . . . 10
⊢ ((𝐵 ∈ (OBasis‘𝑊) ∧ 𝐶 ⊆ 𝐵 ∧ 𝐴 ∈ 𝐵) → (𝐶 ∩ ( ⊥ ‘𝐶)) ⊆ (((LSpan‘𝑊)‘𝐶) ∩ ( ⊥ ‘𝐶))) |
19 | | obselocv.o |
. . . . . . . . . . . . . 14
⊢ ⊥ =
(ocv‘𝑊) |
20 | 10, 19, 14 | ocvlsp 19839 |
. . . . . . . . . . . . 13
⊢ ((𝑊 ∈ PreHil ∧ 𝐶 ⊆ (Base‘𝑊)) → ( ⊥
‘((LSpan‘𝑊)‘𝐶)) = ( ⊥ ‘𝐶)) |
21 | 6, 13, 20 | syl2anc 691 |
. . . . . . . . . . . 12
⊢ ((𝐵 ∈ (OBasis‘𝑊) ∧ 𝐶 ⊆ 𝐵 ∧ 𝐴 ∈ 𝐵) → ( ⊥
‘((LSpan‘𝑊)‘𝐶)) = ( ⊥ ‘𝐶)) |
22 | 21 | ineq2d 3776 |
. . . . . . . . . . 11
⊢ ((𝐵 ∈ (OBasis‘𝑊) ∧ 𝐶 ⊆ 𝐵 ∧ 𝐴 ∈ 𝐵) → (((LSpan‘𝑊)‘𝐶) ∩ ( ⊥
‘((LSpan‘𝑊)‘𝐶))) = (((LSpan‘𝑊)‘𝐶) ∩ ( ⊥ ‘𝐶))) |
23 | | eqid 2610 |
. . . . . . . . . . . . . 14
⊢
(LSubSp‘𝑊) =
(LSubSp‘𝑊) |
24 | 10, 23, 14 | lspcl 18797 |
. . . . . . . . . . . . 13
⊢ ((𝑊 ∈ LMod ∧ 𝐶 ⊆ (Base‘𝑊)) → ((LSpan‘𝑊)‘𝐶) ∈ (LSubSp‘𝑊)) |
25 | 8, 13, 24 | syl2anc 691 |
. . . . . . . . . . . 12
⊢ ((𝐵 ∈ (OBasis‘𝑊) ∧ 𝐶 ⊆ 𝐵 ∧ 𝐴 ∈ 𝐵) → ((LSpan‘𝑊)‘𝐶) ∈ (LSubSp‘𝑊)) |
26 | 19, 23, 1 | ocvin 19837 |
. . . . . . . . . . . 12
⊢ ((𝑊 ∈ PreHil ∧
((LSpan‘𝑊)‘𝐶) ∈ (LSubSp‘𝑊)) → (((LSpan‘𝑊)‘𝐶) ∩ ( ⊥
‘((LSpan‘𝑊)‘𝐶))) = {(0g‘𝑊)}) |
27 | 6, 25, 26 | syl2anc 691 |
. . . . . . . . . . 11
⊢ ((𝐵 ∈ (OBasis‘𝑊) ∧ 𝐶 ⊆ 𝐵 ∧ 𝐴 ∈ 𝐵) → (((LSpan‘𝑊)‘𝐶) ∩ ( ⊥
‘((LSpan‘𝑊)‘𝐶))) = {(0g‘𝑊)}) |
28 | 22, 27 | eqtr3d 2646 |
. . . . . . . . . 10
⊢ ((𝐵 ∈ (OBasis‘𝑊) ∧ 𝐶 ⊆ 𝐵 ∧ 𝐴 ∈ 𝐵) → (((LSpan‘𝑊)‘𝐶) ∩ ( ⊥ ‘𝐶)) = {(0g‘𝑊)}) |
29 | 18, 28 | sseqtrd 3604 |
. . . . . . . . 9
⊢ ((𝐵 ∈ (OBasis‘𝑊) ∧ 𝐶 ⊆ 𝐵 ∧ 𝐴 ∈ 𝐵) → (𝐶 ∩ ( ⊥ ‘𝐶)) ⊆
{(0g‘𝑊)}) |
30 | 29 | sseld 3567 |
. . . . . . . 8
⊢ ((𝐵 ∈ (OBasis‘𝑊) ∧ 𝐶 ⊆ 𝐵 ∧ 𝐴 ∈ 𝐵) → (𝐴 ∈ (𝐶 ∩ ( ⊥ ‘𝐶)) → 𝐴 ∈ {(0g‘𝑊)})) |
31 | 4, 30 | syl5bir 232 |
. . . . . . 7
⊢ ((𝐵 ∈ (OBasis‘𝑊) ∧ 𝐶 ⊆ 𝐵 ∧ 𝐴 ∈ 𝐵) → ((𝐴 ∈ 𝐶 ∧ 𝐴 ∈ ( ⊥ ‘𝐶)) → 𝐴 ∈ {(0g‘𝑊)})) |
32 | | elsni 4142 |
. . . . . . 7
⊢ (𝐴 ∈
{(0g‘𝑊)}
→ 𝐴 =
(0g‘𝑊)) |
33 | 31, 32 | syl6 34 |
. . . . . 6
⊢ ((𝐵 ∈ (OBasis‘𝑊) ∧ 𝐶 ⊆ 𝐵 ∧ 𝐴 ∈ 𝐵) → ((𝐴 ∈ 𝐶 ∧ 𝐴 ∈ ( ⊥ ‘𝐶)) → 𝐴 = (0g‘𝑊))) |
34 | 33 | necon3ad 2795 |
. . . . 5
⊢ ((𝐵 ∈ (OBasis‘𝑊) ∧ 𝐶 ⊆ 𝐵 ∧ 𝐴 ∈ 𝐵) → (𝐴 ≠ (0g‘𝑊) → ¬ (𝐴 ∈ 𝐶 ∧ 𝐴 ∈ ( ⊥ ‘𝐶)))) |
35 | 3, 34 | mpd 15 |
. . . 4
⊢ ((𝐵 ∈ (OBasis‘𝑊) ∧ 𝐶 ⊆ 𝐵 ∧ 𝐴 ∈ 𝐵) → ¬ (𝐴 ∈ 𝐶 ∧ 𝐴 ∈ ( ⊥ ‘𝐶))) |
36 | | imnan 437 |
. . . 4
⊢ ((𝐴 ∈ 𝐶 → ¬ 𝐴 ∈ ( ⊥ ‘𝐶)) ↔ ¬ (𝐴 ∈ 𝐶 ∧ 𝐴 ∈ ( ⊥ ‘𝐶))) |
37 | 35, 36 | sylibr 223 |
. . 3
⊢ ((𝐵 ∈ (OBasis‘𝑊) ∧ 𝐶 ⊆ 𝐵 ∧ 𝐴 ∈ 𝐵) → (𝐴 ∈ 𝐶 → ¬ 𝐴 ∈ ( ⊥ ‘𝐶))) |
38 | 37 | con2d 128 |
. 2
⊢ ((𝐵 ∈ (OBasis‘𝑊) ∧ 𝐶 ⊆ 𝐵 ∧ 𝐴 ∈ 𝐵) → (𝐴 ∈ ( ⊥ ‘𝐶) → ¬ 𝐴 ∈ 𝐶)) |
39 | | simpr 476 |
. . . . . . 7
⊢ (((𝐵 ∈ (OBasis‘𝑊) ∧ 𝐶 ⊆ 𝐵 ∧ 𝐴 ∈ 𝐵) ∧ 𝑥 ∈ 𝐶) → 𝑥 ∈ 𝐶) |
40 | | eleq1 2676 |
. . . . . . 7
⊢ (𝐴 = 𝑥 → (𝐴 ∈ 𝐶 ↔ 𝑥 ∈ 𝐶)) |
41 | 39, 40 | syl5ibrcom 236 |
. . . . . 6
⊢ (((𝐵 ∈ (OBasis‘𝑊) ∧ 𝐶 ⊆ 𝐵 ∧ 𝐴 ∈ 𝐵) ∧ 𝑥 ∈ 𝐶) → (𝐴 = 𝑥 → 𝐴 ∈ 𝐶)) |
42 | 41 | con3d 147 |
. . . . 5
⊢ (((𝐵 ∈ (OBasis‘𝑊) ∧ 𝐶 ⊆ 𝐵 ∧ 𝐴 ∈ 𝐵) ∧ 𝑥 ∈ 𝐶) → (¬ 𝐴 ∈ 𝐶 → ¬ 𝐴 = 𝑥)) |
43 | | simpl1 1057 |
. . . . . . 7
⊢ (((𝐵 ∈ (OBasis‘𝑊) ∧ 𝐶 ⊆ 𝐵 ∧ 𝐴 ∈ 𝐵) ∧ 𝑥 ∈ 𝐶) → 𝐵 ∈ (OBasis‘𝑊)) |
44 | | simpl3 1059 |
. . . . . . 7
⊢ (((𝐵 ∈ (OBasis‘𝑊) ∧ 𝐶 ⊆ 𝐵 ∧ 𝐴 ∈ 𝐵) ∧ 𝑥 ∈ 𝐶) → 𝐴 ∈ 𝐵) |
45 | 9 | sselda 3568 |
. . . . . . 7
⊢ (((𝐵 ∈ (OBasis‘𝑊) ∧ 𝐶 ⊆ 𝐵 ∧ 𝐴 ∈ 𝐵) ∧ 𝑥 ∈ 𝐶) → 𝑥 ∈ 𝐵) |
46 | | eqid 2610 |
. . . . . . . 8
⊢
(·𝑖‘𝑊) =
(·𝑖‘𝑊) |
47 | | eqid 2610 |
. . . . . . . 8
⊢
(Scalar‘𝑊) =
(Scalar‘𝑊) |
48 | | eqid 2610 |
. . . . . . . 8
⊢
(1r‘(Scalar‘𝑊)) =
(1r‘(Scalar‘𝑊)) |
49 | | eqid 2610 |
. . . . . . . 8
⊢
(0g‘(Scalar‘𝑊)) =
(0g‘(Scalar‘𝑊)) |
50 | 10, 46, 47, 48, 49 | obsip 19884 |
. . . . . . 7
⊢ ((𝐵 ∈ (OBasis‘𝑊) ∧ 𝐴 ∈ 𝐵 ∧ 𝑥 ∈ 𝐵) → (𝐴(·𝑖‘𝑊)𝑥) = if(𝐴 = 𝑥, (1r‘(Scalar‘𝑊)),
(0g‘(Scalar‘𝑊)))) |
51 | 43, 44, 45, 50 | syl3anc 1318 |
. . . . . 6
⊢ (((𝐵 ∈ (OBasis‘𝑊) ∧ 𝐶 ⊆ 𝐵 ∧ 𝐴 ∈ 𝐵) ∧ 𝑥 ∈ 𝐶) → (𝐴(·𝑖‘𝑊)𝑥) = if(𝐴 = 𝑥, (1r‘(Scalar‘𝑊)),
(0g‘(Scalar‘𝑊)))) |
52 | | iffalse 4045 |
. . . . . . 7
⊢ (¬
𝐴 = 𝑥 → if(𝐴 = 𝑥, (1r‘(Scalar‘𝑊)),
(0g‘(Scalar‘𝑊))) =
(0g‘(Scalar‘𝑊))) |
53 | 52 | eqeq2d 2620 |
. . . . . 6
⊢ (¬
𝐴 = 𝑥 → ((𝐴(·𝑖‘𝑊)𝑥) = if(𝐴 = 𝑥, (1r‘(Scalar‘𝑊)),
(0g‘(Scalar‘𝑊))) ↔ (𝐴(·𝑖‘𝑊)𝑥) = (0g‘(Scalar‘𝑊)))) |
54 | 51, 53 | syl5ibcom 234 |
. . . . 5
⊢ (((𝐵 ∈ (OBasis‘𝑊) ∧ 𝐶 ⊆ 𝐵 ∧ 𝐴 ∈ 𝐵) ∧ 𝑥 ∈ 𝐶) → (¬ 𝐴 = 𝑥 → (𝐴(·𝑖‘𝑊)𝑥) = (0g‘(Scalar‘𝑊)))) |
55 | 42, 54 | syld 46 |
. . . 4
⊢ (((𝐵 ∈ (OBasis‘𝑊) ∧ 𝐶 ⊆ 𝐵 ∧ 𝐴 ∈ 𝐵) ∧ 𝑥 ∈ 𝐶) → (¬ 𝐴 ∈ 𝐶 → (𝐴(·𝑖‘𝑊)𝑥) = (0g‘(Scalar‘𝑊)))) |
56 | 55 | ralrimdva 2952 |
. . 3
⊢ ((𝐵 ∈ (OBasis‘𝑊) ∧ 𝐶 ⊆ 𝐵 ∧ 𝐴 ∈ 𝐵) → (¬ 𝐴 ∈ 𝐶 → ∀𝑥 ∈ 𝐶 (𝐴(·𝑖‘𝑊)𝑥) = (0g‘(Scalar‘𝑊)))) |
57 | | simp3 1056 |
. . . . 5
⊢ ((𝐵 ∈ (OBasis‘𝑊) ∧ 𝐶 ⊆ 𝐵 ∧ 𝐴 ∈ 𝐵) → 𝐴 ∈ 𝐵) |
58 | 12, 57 | sseldd 3569 |
. . . 4
⊢ ((𝐵 ∈ (OBasis‘𝑊) ∧ 𝐶 ⊆ 𝐵 ∧ 𝐴 ∈ 𝐵) → 𝐴 ∈ (Base‘𝑊)) |
59 | 10, 46, 47, 49, 19 | elocv 19831 |
. . . . . 6
⊢ (𝐴 ∈ ( ⊥ ‘𝐶) ↔ (𝐶 ⊆ (Base‘𝑊) ∧ 𝐴 ∈ (Base‘𝑊) ∧ ∀𝑥 ∈ 𝐶 (𝐴(·𝑖‘𝑊)𝑥) = (0g‘(Scalar‘𝑊)))) |
60 | | df-3an 1033 |
. . . . . 6
⊢ ((𝐶 ⊆ (Base‘𝑊) ∧ 𝐴 ∈ (Base‘𝑊) ∧ ∀𝑥 ∈ 𝐶 (𝐴(·𝑖‘𝑊)𝑥) = (0g‘(Scalar‘𝑊))) ↔ ((𝐶 ⊆ (Base‘𝑊) ∧ 𝐴 ∈ (Base‘𝑊)) ∧ ∀𝑥 ∈ 𝐶 (𝐴(·𝑖‘𝑊)𝑥) = (0g‘(Scalar‘𝑊)))) |
61 | 59, 60 | bitri 263 |
. . . . 5
⊢ (𝐴 ∈ ( ⊥ ‘𝐶) ↔ ((𝐶 ⊆ (Base‘𝑊) ∧ 𝐴 ∈ (Base‘𝑊)) ∧ ∀𝑥 ∈ 𝐶 (𝐴(·𝑖‘𝑊)𝑥) = (0g‘(Scalar‘𝑊)))) |
62 | 61 | baib 942 |
. . . 4
⊢ ((𝐶 ⊆ (Base‘𝑊) ∧ 𝐴 ∈ (Base‘𝑊)) → (𝐴 ∈ ( ⊥ ‘𝐶) ↔ ∀𝑥 ∈ 𝐶 (𝐴(·𝑖‘𝑊)𝑥) = (0g‘(Scalar‘𝑊)))) |
63 | 13, 58, 62 | syl2anc 691 |
. . 3
⊢ ((𝐵 ∈ (OBasis‘𝑊) ∧ 𝐶 ⊆ 𝐵 ∧ 𝐴 ∈ 𝐵) → (𝐴 ∈ ( ⊥ ‘𝐶) ↔ ∀𝑥 ∈ 𝐶 (𝐴(·𝑖‘𝑊)𝑥) = (0g‘(Scalar‘𝑊)))) |
64 | 56, 63 | sylibrd 248 |
. 2
⊢ ((𝐵 ∈ (OBasis‘𝑊) ∧ 𝐶 ⊆ 𝐵 ∧ 𝐴 ∈ 𝐵) → (¬ 𝐴 ∈ 𝐶 → 𝐴 ∈ ( ⊥ ‘𝐶))) |
65 | 38, 64 | impbid 201 |
1
⊢ ((𝐵 ∈ (OBasis‘𝑊) ∧ 𝐶 ⊆ 𝐵 ∧ 𝐴 ∈ 𝐵) → (𝐴 ∈ ( ⊥ ‘𝐶) ↔ ¬ 𝐴 ∈ 𝐶)) |