Proof of Theorem cdlemn4
Step | Hyp | Ref
| Expression |
1 | | simp1 1137 |
. . 3
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ (𝑅 ∈ 𝐴 ∧ ¬ 𝑅 ≤ 𝑊)) → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻)) |
2 | | cdlemn4.l |
. . . . . 6
⊢ ≤ =
(le‘𝐾) |
3 | | cdlemn4.a |
. . . . . 6
⊢ 𝐴 = (Atoms‘𝐾) |
4 | | cdlemn4.h |
. . . . . 6
⊢ 𝐻 = (LHyp‘𝐾) |
5 | | cdlemn4.p |
. . . . . 6
⊢ 𝑃 = ((oc‘𝐾)‘𝑊) |
6 | 2, 3, 4, 5 | lhpocnel2 37645 |
. . . . 5
⊢ ((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) → (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊)) |
7 | 1, 6 | syl 17 |
. . . 4
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ (𝑅 ∈ 𝐴 ∧ ¬ 𝑅 ≤ 𝑊)) → (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊)) |
8 | | simp2 1138 |
. . . 4
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ (𝑅 ∈ 𝐴 ∧ ¬ 𝑅 ≤ 𝑊)) → (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊)) |
9 | | cdlemn4.t |
. . . . 5
⊢ 𝑇 = ((LTrn‘𝐾)‘𝑊) |
10 | | cdlemn4.f |
. . . . 5
⊢ 𝐹 = (℩ℎ ∈ 𝑇 (ℎ‘𝑃) = 𝑄) |
11 | 2, 3, 4, 9, 10 | ltrniotacl 38205 |
. . . 4
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊)) → 𝐹 ∈ 𝑇) |
12 | 1, 7, 8, 11 | syl3anc 1372 |
. . 3
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ (𝑅 ∈ 𝐴 ∧ ¬ 𝑅 ≤ 𝑊)) → 𝐹 ∈ 𝑇) |
13 | | eqid 2738 |
. . . . 5
⊢
((TEndo‘𝐾)‘𝑊) = ((TEndo‘𝐾)‘𝑊) |
14 | 4, 9, 13 | tendoidcl 38395 |
. . . 4
⊢ ((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) → ( I ↾ 𝑇) ∈ ((TEndo‘𝐾)‘𝑊)) |
15 | 1, 14 | syl 17 |
. . 3
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ (𝑅 ∈ 𝐴 ∧ ¬ 𝑅 ≤ 𝑊)) → ( I ↾ 𝑇) ∈ ((TEndo‘𝐾)‘𝑊)) |
16 | | cdlemn4.j |
. . . 4
⊢ 𝐽 = (℩ℎ ∈ 𝑇 (ℎ‘𝑄) = 𝑅) |
17 | 2, 3, 4, 9, 16 | ltrniotacl 38205 |
. . 3
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ (𝑅 ∈ 𝐴 ∧ ¬ 𝑅 ≤ 𝑊)) → 𝐽 ∈ 𝑇) |
18 | | cdlemn4.b |
. . . . 5
⊢ 𝐵 = (Base‘𝐾) |
19 | | cdlemn4.o |
. . . . 5
⊢ 𝑂 = (ℎ ∈ 𝑇 ↦ ( I ↾ 𝐵)) |
20 | 18, 4, 9, 13, 19 | tendo0cl 38416 |
. . . 4
⊢ ((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) → 𝑂 ∈ ((TEndo‘𝐾)‘𝑊)) |
21 | 1, 20 | syl 17 |
. . 3
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ (𝑅 ∈ 𝐴 ∧ ¬ 𝑅 ≤ 𝑊)) → 𝑂 ∈ ((TEndo‘𝐾)‘𝑊)) |
22 | | cdlemn4.u |
. . . 4
⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊) |
23 | | eqid 2738 |
. . . 4
⊢
(Scalar‘𝑈) =
(Scalar‘𝑈) |
24 | | cdlemn4.s |
. . . 4
⊢ + =
(+g‘𝑈) |
25 | | eqid 2738 |
. . . 4
⊢
(+g‘(Scalar‘𝑈)) =
(+g‘(Scalar‘𝑈)) |
26 | 4, 9, 13, 22, 23, 24, 25 | dvhopvadd 38719 |
. . 3
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝐹 ∈ 𝑇 ∧ ( I ↾ 𝑇) ∈ ((TEndo‘𝐾)‘𝑊)) ∧ (𝐽 ∈ 𝑇 ∧ 𝑂 ∈ ((TEndo‘𝐾)‘𝑊))) → (〈𝐹, ( I ↾ 𝑇)〉 + 〈𝐽, 𝑂〉) = 〈(𝐹 ∘ 𝐽), (( I ↾ 𝑇)(+g‘(Scalar‘𝑈))𝑂)〉) |
27 | 1, 12, 15, 17, 21, 26 | syl122anc 1380 |
. 2
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ (𝑅 ∈ 𝐴 ∧ ¬ 𝑅 ≤ 𝑊)) → (〈𝐹, ( I ↾ 𝑇)〉 + 〈𝐽, 𝑂〉) = 〈(𝐹 ∘ 𝐽), (( I ↾ 𝑇)(+g‘(Scalar‘𝑈))𝑂)〉) |
28 | 4, 9 | ltrncom 38364 |
. . . . 5
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝐹 ∈ 𝑇 ∧ 𝐽 ∈ 𝑇) → (𝐹 ∘ 𝐽) = (𝐽 ∘ 𝐹)) |
29 | 1, 12, 17, 28 | syl3anc 1372 |
. . . 4
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ (𝑅 ∈ 𝐴 ∧ ¬ 𝑅 ≤ 𝑊)) → (𝐹 ∘ 𝐽) = (𝐽 ∘ 𝐹)) |
30 | | cdlemn4.g |
. . . . 5
⊢ 𝐺 = (℩ℎ ∈ 𝑇 (ℎ‘𝑃) = 𝑅) |
31 | 2, 3, 5, 4, 9, 10,
30, 16 | cdlemn3 38823 |
. . . 4
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ (𝑅 ∈ 𝐴 ∧ ¬ 𝑅 ≤ 𝑊)) → (𝐽 ∘ 𝐹) = 𝐺) |
32 | 29, 31 | eqtrd 2773 |
. . 3
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ (𝑅 ∈ 𝐴 ∧ ¬ 𝑅 ≤ 𝑊)) → (𝐹 ∘ 𝐽) = 𝐺) |
33 | | eqid 2738 |
. . . . . . . . 9
⊢
((EDRing‘𝐾)‘𝑊) = ((EDRing‘𝐾)‘𝑊) |
34 | 4, 33, 22, 23 | dvhsca 38708 |
. . . . . . . 8
⊢ ((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) → (Scalar‘𝑈) = ((EDRing‘𝐾)‘𝑊)) |
35 | 34 | fveq2d 6672 |
. . . . . . 7
⊢ ((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) →
(0g‘(Scalar‘𝑈)) =
(0g‘((EDRing‘𝐾)‘𝑊))) |
36 | | eqid 2738 |
. . . . . . . 8
⊢
(0g‘((EDRing‘𝐾)‘𝑊)) =
(0g‘((EDRing‘𝐾)‘𝑊)) |
37 | 18, 4, 9, 33, 19, 36 | erng0g 38620 |
. . . . . . 7
⊢ ((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) →
(0g‘((EDRing‘𝐾)‘𝑊)) = 𝑂) |
38 | 35, 37 | eqtrd 2773 |
. . . . . 6
⊢ ((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) →
(0g‘(Scalar‘𝑈)) = 𝑂) |
39 | 1, 38 | syl 17 |
. . . . 5
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ (𝑅 ∈ 𝐴 ∧ ¬ 𝑅 ≤ 𝑊)) →
(0g‘(Scalar‘𝑈)) = 𝑂) |
40 | 39 | oveq2d 7180 |
. . . 4
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ (𝑅 ∈ 𝐴 ∧ ¬ 𝑅 ≤ 𝑊)) → (( I ↾ 𝑇)(+g‘(Scalar‘𝑈))(0g‘(Scalar‘𝑈))) = (( I ↾ 𝑇)(+g‘(Scalar‘𝑈))𝑂)) |
41 | 4, 33 | erngdv 38619 |
. . . . . . . 8
⊢ ((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) → ((EDRing‘𝐾)‘𝑊) ∈ DivRing) |
42 | | drnggrp 19622 |
. . . . . . . 8
⊢
(((EDRing‘𝐾)‘𝑊) ∈ DivRing → ((EDRing‘𝐾)‘𝑊) ∈ Grp) |
43 | 41, 42 | syl 17 |
. . . . . . 7
⊢ ((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) → ((EDRing‘𝐾)‘𝑊) ∈ Grp) |
44 | 34, 43 | eqeltrd 2833 |
. . . . . 6
⊢ ((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) → (Scalar‘𝑈) ∈ Grp) |
45 | 1, 44 | syl 17 |
. . . . 5
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ (𝑅 ∈ 𝐴 ∧ ¬ 𝑅 ≤ 𝑊)) → (Scalar‘𝑈) ∈ Grp) |
46 | | eqid 2738 |
. . . . . . . 8
⊢
(Base‘(Scalar‘𝑈)) = (Base‘(Scalar‘𝑈)) |
47 | 4, 13, 22, 23, 46 | dvhbase 38709 |
. . . . . . 7
⊢ ((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) → (Base‘(Scalar‘𝑈)) = ((TEndo‘𝐾)‘𝑊)) |
48 | 1, 47 | syl 17 |
. . . . . 6
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ (𝑅 ∈ 𝐴 ∧ ¬ 𝑅 ≤ 𝑊)) → (Base‘(Scalar‘𝑈)) = ((TEndo‘𝐾)‘𝑊)) |
49 | 15, 48 | eleqtrrd 2836 |
. . . . 5
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ (𝑅 ∈ 𝐴 ∧ ¬ 𝑅 ≤ 𝑊)) → ( I ↾ 𝑇) ∈ (Base‘(Scalar‘𝑈))) |
50 | | eqid 2738 |
. . . . . 6
⊢
(0g‘(Scalar‘𝑈)) =
(0g‘(Scalar‘𝑈)) |
51 | 46, 25, 50 | grprid 18245 |
. . . . 5
⊢
(((Scalar‘𝑈)
∈ Grp ∧ ( I ↾ 𝑇) ∈ (Base‘(Scalar‘𝑈))) → (( I ↾ 𝑇)(+g‘(Scalar‘𝑈))(0g‘(Scalar‘𝑈))) = ( I ↾ 𝑇)) |
52 | 45, 49, 51 | syl2anc 587 |
. . . 4
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ (𝑅 ∈ 𝐴 ∧ ¬ 𝑅 ≤ 𝑊)) → (( I ↾ 𝑇)(+g‘(Scalar‘𝑈))(0g‘(Scalar‘𝑈))) = ( I ↾ 𝑇)) |
53 | 40, 52 | eqtr3d 2775 |
. . 3
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ (𝑅 ∈ 𝐴 ∧ ¬ 𝑅 ≤ 𝑊)) → (( I ↾ 𝑇)(+g‘(Scalar‘𝑈))𝑂) = ( I ↾ 𝑇)) |
54 | 32, 53 | opeq12d 4766 |
. 2
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ (𝑅 ∈ 𝐴 ∧ ¬ 𝑅 ≤ 𝑊)) → 〈(𝐹 ∘ 𝐽), (( I ↾ 𝑇)(+g‘(Scalar‘𝑈))𝑂)〉 = 〈𝐺, ( I ↾ 𝑇)〉) |
55 | 27, 54 | eqtr2d 2774 |
1
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ (𝑅 ∈ 𝐴 ∧ ¬ 𝑅 ≤ 𝑊)) → 〈𝐺, ( I ↾ 𝑇)〉 = (〈𝐹, ( I ↾ 𝑇)〉 + 〈𝐽, 𝑂〉)) |