Step | Hyp | Ref
| Expression |
1 | | eqid 2737 |
. . . 4
⊢
(0g‘𝑈) = (0g‘𝑈) |
2 | | eqid 2737 |
. . . 4
⊢
(LSAtoms‘𝑈) =
(LSAtoms‘𝑈) |
3 | | dochkr1OLD.h |
. . . . 5
⊢ 𝐻 = (LHyp‘𝐾) |
4 | | dochkr1OLD.u |
. . . . 5
⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊) |
5 | | dochkr1OLD.k |
. . . . 5
⊢ (𝜑 → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻)) |
6 | 3, 4, 5 | dvhlmod 38861 |
. . . 4
⊢ (𝜑 → 𝑈 ∈ LMod) |
7 | | dochkr1OLD.n |
. . . . 5
⊢ (𝜑 → ( ⊥ ‘( ⊥
‘(𝐿‘𝐺))) ≠ 𝑉) |
8 | | dochkr1OLD.o |
. . . . . 6
⊢ ⊥ =
((ocH‘𝐾)‘𝑊) |
9 | | dochkr1OLD.v |
. . . . . 6
⊢ 𝑉 = (Base‘𝑈) |
10 | | dochkr1OLD.f |
. . . . . 6
⊢ 𝐹 = (LFnl‘𝑈) |
11 | | dochkr1OLD.l |
. . . . . 6
⊢ 𝐿 = (LKer‘𝑈) |
12 | | dochkr1OLD.g |
. . . . . 6
⊢ (𝜑 → 𝐺 ∈ 𝐹) |
13 | 3, 8, 4, 9, 2, 10,
11, 5, 12 | dochkrsat2 39207 |
. . . . 5
⊢ (𝜑 → (( ⊥ ‘( ⊥
‘(𝐿‘𝐺))) ≠ 𝑉 ↔ ( ⊥ ‘(𝐿‘𝐺)) ∈ (LSAtoms‘𝑈))) |
14 | 7, 13 | mpbid 235 |
. . . 4
⊢ (𝜑 → ( ⊥ ‘(𝐿‘𝐺)) ∈ (LSAtoms‘𝑈)) |
15 | 1, 2, 6, 14 | lsateln0 36746 |
. . 3
⊢ (𝜑 → ∃𝑧 ∈ ( ⊥ ‘(𝐿‘𝐺))𝑧 ≠ (0g‘𝑈)) |
16 | | dochkr1OLD.r |
. . . . . 6
⊢ 𝑅 = (Scalar‘𝑈) |
17 | | dochkr1OLD.z |
. . . . . 6
⊢ 0 =
(0g‘𝑅) |
18 | 5 | ad2antrr 726 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑧 ∈ ( ⊥ ‘(𝐿‘𝐺))) ∧ 𝑧 ≠ (0g‘𝑈)) → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻)) |
19 | 12 | ad2antrr 726 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑧 ∈ ( ⊥ ‘(𝐿‘𝐺))) ∧ 𝑧 ≠ (0g‘𝑈)) → 𝐺 ∈ 𝐹) |
20 | | eldifsn 4700 |
. . . . . . . 8
⊢ (𝑧 ∈ (( ⊥ ‘(𝐿‘𝐺)) ∖ {(0g‘𝑈)}) ↔ (𝑧 ∈ ( ⊥ ‘(𝐿‘𝐺)) ∧ 𝑧 ≠ (0g‘𝑈))) |
21 | 20 | biimpri 231 |
. . . . . . 7
⊢ ((𝑧 ∈ ( ⊥ ‘(𝐿‘𝐺)) ∧ 𝑧 ≠ (0g‘𝑈)) → 𝑧 ∈ (( ⊥ ‘(𝐿‘𝐺)) ∖ {(0g‘𝑈)})) |
22 | 21 | adantll 714 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑧 ∈ ( ⊥ ‘(𝐿‘𝐺))) ∧ 𝑧 ≠ (0g‘𝑈)) → 𝑧 ∈ (( ⊥ ‘(𝐿‘𝐺)) ∖ {(0g‘𝑈)})) |
23 | 3, 8, 4, 9, 16, 17, 1, 10, 11, 18, 19, 22 | dochfln0 39228 |
. . . . 5
⊢ (((𝜑 ∧ 𝑧 ∈ ( ⊥ ‘(𝐿‘𝐺))) ∧ 𝑧 ≠ (0g‘𝑈)) → (𝐺‘𝑧) ≠ 0 ) |
24 | 23 | ex 416 |
. . . 4
⊢ ((𝜑 ∧ 𝑧 ∈ ( ⊥ ‘(𝐿‘𝐺))) → (𝑧 ≠ (0g‘𝑈) → (𝐺‘𝑧) ≠ 0 )) |
25 | 24 | reximdva 3193 |
. . 3
⊢ (𝜑 → (∃𝑧 ∈ ( ⊥ ‘(𝐿‘𝐺))𝑧 ≠ (0g‘𝑈) → ∃𝑧 ∈ ( ⊥ ‘(𝐿‘𝐺))(𝐺‘𝑧) ≠ 0 )) |
26 | 15, 25 | mpd 15 |
. 2
⊢ (𝜑 → ∃𝑧 ∈ ( ⊥ ‘(𝐿‘𝐺))(𝐺‘𝑧) ≠ 0 ) |
27 | 9, 10, 11, 6, 12 | lkrssv 36847 |
. . . . . . . 8
⊢ (𝜑 → (𝐿‘𝐺) ⊆ 𝑉) |
28 | | eqid 2737 |
. . . . . . . . 9
⊢
(LSubSp‘𝑈) =
(LSubSp‘𝑈) |
29 | 3, 4, 9, 28, 8 | dochlss 39105 |
. . . . . . . 8
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝐿‘𝐺) ⊆ 𝑉) → ( ⊥ ‘(𝐿‘𝐺)) ∈ (LSubSp‘𝑈)) |
30 | 5, 27, 29 | syl2anc 587 |
. . . . . . 7
⊢ (𝜑 → ( ⊥ ‘(𝐿‘𝐺)) ∈ (LSubSp‘𝑈)) |
31 | 6, 30 | jca 515 |
. . . . . 6
⊢ (𝜑 → (𝑈 ∈ LMod ∧ ( ⊥ ‘(𝐿‘𝐺)) ∈ (LSubSp‘𝑈))) |
32 | 31 | 3ad2ant1 1135 |
. . . . 5
⊢ ((𝜑 ∧ 𝑧 ∈ ( ⊥ ‘(𝐿‘𝐺)) ∧ (𝐺‘𝑧) ≠ 0 ) → (𝑈 ∈ LMod ∧ ( ⊥
‘(𝐿‘𝐺)) ∈ (LSubSp‘𝑈))) |
33 | 3, 4, 5 | dvhlvec 38860 |
. . . . . . . 8
⊢ (𝜑 → 𝑈 ∈ LVec) |
34 | 33 | 3ad2ant1 1135 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑧 ∈ ( ⊥ ‘(𝐿‘𝐺)) ∧ (𝐺‘𝑧) ≠ 0 ) → 𝑈 ∈ LVec) |
35 | 16 | lvecdrng 20142 |
. . . . . . 7
⊢ (𝑈 ∈ LVec → 𝑅 ∈
DivRing) |
36 | 34, 35 | syl 17 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑧 ∈ ( ⊥ ‘(𝐿‘𝐺)) ∧ (𝐺‘𝑧) ≠ 0 ) → 𝑅 ∈ DivRing) |
37 | 6 | 3ad2ant1 1135 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑧 ∈ ( ⊥ ‘(𝐿‘𝐺)) ∧ (𝐺‘𝑧) ≠ 0 ) → 𝑈 ∈ LMod) |
38 | 12 | 3ad2ant1 1135 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑧 ∈ ( ⊥ ‘(𝐿‘𝐺)) ∧ (𝐺‘𝑧) ≠ 0 ) → 𝐺 ∈ 𝐹) |
39 | 3, 4, 9, 8 | dochssv 39106 |
. . . . . . . . . 10
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝐿‘𝐺) ⊆ 𝑉) → ( ⊥ ‘(𝐿‘𝐺)) ⊆ 𝑉) |
40 | 5, 27, 39 | syl2anc 587 |
. . . . . . . . 9
⊢ (𝜑 → ( ⊥ ‘(𝐿‘𝐺)) ⊆ 𝑉) |
41 | 40 | sselda 3901 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑧 ∈ ( ⊥ ‘(𝐿‘𝐺))) → 𝑧 ∈ 𝑉) |
42 | 41 | 3adant3 1134 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑧 ∈ ( ⊥ ‘(𝐿‘𝐺)) ∧ (𝐺‘𝑧) ≠ 0 ) → 𝑧 ∈ 𝑉) |
43 | | eqid 2737 |
. . . . . . . 8
⊢
(Base‘𝑅) =
(Base‘𝑅) |
44 | 16, 43, 9, 10 | lflcl 36815 |
. . . . . . 7
⊢ ((𝑈 ∈ LMod ∧ 𝐺 ∈ 𝐹 ∧ 𝑧 ∈ 𝑉) → (𝐺‘𝑧) ∈ (Base‘𝑅)) |
45 | 37, 38, 42, 44 | syl3anc 1373 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑧 ∈ ( ⊥ ‘(𝐿‘𝐺)) ∧ (𝐺‘𝑧) ≠ 0 ) → (𝐺‘𝑧) ∈ (Base‘𝑅)) |
46 | | simp3 1140 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑧 ∈ ( ⊥ ‘(𝐿‘𝐺)) ∧ (𝐺‘𝑧) ≠ 0 ) → (𝐺‘𝑧) ≠ 0 ) |
47 | | eqid 2737 |
. . . . . . 7
⊢
(invr‘𝑅) = (invr‘𝑅) |
48 | 43, 17, 47 | drnginvrcl 19784 |
. . . . . 6
⊢ ((𝑅 ∈ DivRing ∧ (𝐺‘𝑧) ∈ (Base‘𝑅) ∧ (𝐺‘𝑧) ≠ 0 ) →
((invr‘𝑅)‘(𝐺‘𝑧)) ∈ (Base‘𝑅)) |
49 | 36, 45, 46, 48 | syl3anc 1373 |
. . . . 5
⊢ ((𝜑 ∧ 𝑧 ∈ ( ⊥ ‘(𝐿‘𝐺)) ∧ (𝐺‘𝑧) ≠ 0 ) →
((invr‘𝑅)‘(𝐺‘𝑧)) ∈ (Base‘𝑅)) |
50 | | simp2 1139 |
. . . . 5
⊢ ((𝜑 ∧ 𝑧 ∈ ( ⊥ ‘(𝐿‘𝐺)) ∧ (𝐺‘𝑧) ≠ 0 ) → 𝑧 ∈ ( ⊥ ‘(𝐿‘𝐺))) |
51 | | eqid 2737 |
. . . . . 6
⊢ (
·𝑠 ‘𝑈) = ( ·𝑠
‘𝑈) |
52 | 16, 51, 43, 28 | lssvscl 19992 |
. . . . 5
⊢ (((𝑈 ∈ LMod ∧ ( ⊥
‘(𝐿‘𝐺)) ∈ (LSubSp‘𝑈)) ∧
(((invr‘𝑅)‘(𝐺‘𝑧)) ∈ (Base‘𝑅) ∧ 𝑧 ∈ ( ⊥ ‘(𝐿‘𝐺)))) → (((invr‘𝑅)‘(𝐺‘𝑧))( ·𝑠
‘𝑈)𝑧) ∈ ( ⊥ ‘(𝐿‘𝐺))) |
53 | 32, 49, 50, 52 | syl12anc 837 |
. . . 4
⊢ ((𝜑 ∧ 𝑧 ∈ ( ⊥ ‘(𝐿‘𝐺)) ∧ (𝐺‘𝑧) ≠ 0 ) →
(((invr‘𝑅)‘(𝐺‘𝑧))( ·𝑠
‘𝑈)𝑧) ∈ ( ⊥ ‘(𝐿‘𝐺))) |
54 | | eqid 2737 |
. . . . . . 7
⊢
(.r‘𝑅) = (.r‘𝑅) |
55 | 16, 43, 54, 9, 51, 10 | lflmul 36819 |
. . . . . 6
⊢ ((𝑈 ∈ LMod ∧ 𝐺 ∈ 𝐹 ∧ (((invr‘𝑅)‘(𝐺‘𝑧)) ∈ (Base‘𝑅) ∧ 𝑧 ∈ 𝑉)) → (𝐺‘(((invr‘𝑅)‘(𝐺‘𝑧))( ·𝑠
‘𝑈)𝑧)) = (((invr‘𝑅)‘(𝐺‘𝑧))(.r‘𝑅)(𝐺‘𝑧))) |
56 | 37, 38, 49, 42, 55 | syl112anc 1376 |
. . . . 5
⊢ ((𝜑 ∧ 𝑧 ∈ ( ⊥ ‘(𝐿‘𝐺)) ∧ (𝐺‘𝑧) ≠ 0 ) → (𝐺‘(((invr‘𝑅)‘(𝐺‘𝑧))( ·𝑠
‘𝑈)𝑧)) = (((invr‘𝑅)‘(𝐺‘𝑧))(.r‘𝑅)(𝐺‘𝑧))) |
57 | | dochkr1OLD.i |
. . . . . . 7
⊢ 1 =
(1r‘𝑅) |
58 | 43, 17, 54, 57, 47 | drnginvrl 19786 |
. . . . . 6
⊢ ((𝑅 ∈ DivRing ∧ (𝐺‘𝑧) ∈ (Base‘𝑅) ∧ (𝐺‘𝑧) ≠ 0 ) →
(((invr‘𝑅)‘(𝐺‘𝑧))(.r‘𝑅)(𝐺‘𝑧)) = 1 ) |
59 | 36, 45, 46, 58 | syl3anc 1373 |
. . . . 5
⊢ ((𝜑 ∧ 𝑧 ∈ ( ⊥ ‘(𝐿‘𝐺)) ∧ (𝐺‘𝑧) ≠ 0 ) →
(((invr‘𝑅)‘(𝐺‘𝑧))(.r‘𝑅)(𝐺‘𝑧)) = 1 ) |
60 | 56, 59 | eqtrd 2777 |
. . . 4
⊢ ((𝜑 ∧ 𝑧 ∈ ( ⊥ ‘(𝐿‘𝐺)) ∧ (𝐺‘𝑧) ≠ 0 ) → (𝐺‘(((invr‘𝑅)‘(𝐺‘𝑧))( ·𝑠
‘𝑈)𝑧)) = 1 ) |
61 | | fveqeq2 6726 |
. . . . 5
⊢ (𝑥 =
(((invr‘𝑅)‘(𝐺‘𝑧))( ·𝑠
‘𝑈)𝑧) → ((𝐺‘𝑥) = 1 ↔ (𝐺‘(((invr‘𝑅)‘(𝐺‘𝑧))( ·𝑠
‘𝑈)𝑧)) = 1 )) |
62 | 61 | rspcev 3537 |
. . . 4
⊢
(((((invr‘𝑅)‘(𝐺‘𝑧))( ·𝑠
‘𝑈)𝑧) ∈ ( ⊥ ‘(𝐿‘𝐺)) ∧ (𝐺‘(((invr‘𝑅)‘(𝐺‘𝑧))( ·𝑠
‘𝑈)𝑧)) = 1 ) → ∃𝑥 ∈ ( ⊥ ‘(𝐿‘𝐺))(𝐺‘𝑥) = 1 ) |
63 | 53, 60, 62 | syl2anc 587 |
. . 3
⊢ ((𝜑 ∧ 𝑧 ∈ ( ⊥ ‘(𝐿‘𝐺)) ∧ (𝐺‘𝑧) ≠ 0 ) → ∃𝑥 ∈ ( ⊥ ‘(𝐿‘𝐺))(𝐺‘𝑥) = 1 ) |
64 | 63 | rexlimdv3a 3205 |
. 2
⊢ (𝜑 → (∃𝑧 ∈ ( ⊥ ‘(𝐿‘𝐺))(𝐺‘𝑧) ≠ 0 → ∃𝑥 ∈ ( ⊥ ‘(𝐿‘𝐺))(𝐺‘𝑥) = 1 )) |
65 | 26, 64 | mpd 15 |
1
⊢ (𝜑 → ∃𝑥 ∈ ( ⊥ ‘(𝐿‘𝐺))(𝐺‘𝑥) = 1 ) |