Proof of Theorem ldualvsubval
| Step | Hyp | Ref | Expression | 
|---|
| 1 |  | ldualvsubval.d | . . . . 5
⊢ 𝐷 = (LDual‘𝑊) | 
| 2 |  | ldualvsubval.w | . . . . 5
⊢ (𝜑 → 𝑊 ∈ LMod) | 
| 3 | 1, 2 | lduallmod 39154 | . . . 4
⊢ (𝜑 → 𝐷 ∈ LMod) | 
| 4 |  | ldualvsubval.f | . . . . 5
⊢ 𝐹 = (LFnl‘𝑊) | 
| 5 |  | eqid 2737 | . . . . 5
⊢
(Base‘𝐷) =
(Base‘𝐷) | 
| 6 |  | ldualvsubval.g | . . . . 5
⊢ (𝜑 → 𝐺 ∈ 𝐹) | 
| 7 | 4, 1, 5, 2, 6 | ldualelvbase 39128 | . . . 4
⊢ (𝜑 → 𝐺 ∈ (Base‘𝐷)) | 
| 8 |  | ldualvsubval.h | . . . . 5
⊢ (𝜑 → 𝐻 ∈ 𝐹) | 
| 9 | 4, 1, 5, 2, 8 | ldualelvbase 39128 | . . . 4
⊢ (𝜑 → 𝐻 ∈ (Base‘𝐷)) | 
| 10 |  | eqid 2737 | . . . . 5
⊢
(+g‘𝐷) = (+g‘𝐷) | 
| 11 |  | ldualvsubval.m | . . . . 5
⊢  − =
(-g‘𝐷) | 
| 12 |  | eqid 2737 | . . . . 5
⊢
(Scalar‘𝐷) =
(Scalar‘𝐷) | 
| 13 |  | eqid 2737 | . . . . 5
⊢ (
·𝑠 ‘𝐷) = ( ·𝑠
‘𝐷) | 
| 14 |  | eqid 2737 | . . . . 5
⊢
(invg‘(Scalar‘𝐷)) =
(invg‘(Scalar‘𝐷)) | 
| 15 |  | eqid 2737 | . . . . 5
⊢
(1r‘(Scalar‘𝐷)) =
(1r‘(Scalar‘𝐷)) | 
| 16 | 5, 10, 11, 12, 13, 14, 15 | lmodvsubval2 20915 | . . . 4
⊢ ((𝐷 ∈ LMod ∧ 𝐺 ∈ (Base‘𝐷) ∧ 𝐻 ∈ (Base‘𝐷)) → (𝐺 − 𝐻) = (𝐺(+g‘𝐷)(((invg‘(Scalar‘𝐷))‘(1r‘(Scalar‘𝐷)))(
·𝑠 ‘𝐷)𝐻))) | 
| 17 | 3, 7, 9, 16 | syl3anc 1373 | . . 3
⊢ (𝜑 → (𝐺 − 𝐻) = (𝐺(+g‘𝐷)(((invg‘(Scalar‘𝐷))‘(1r‘(Scalar‘𝐷)))(
·𝑠 ‘𝐷)𝐻))) | 
| 18 | 17 | fveq1d 6908 | . 2
⊢ (𝜑 → ((𝐺 − 𝐻)‘𝑋) = ((𝐺(+g‘𝐷)(((invg‘(Scalar‘𝐷))‘(1r‘(Scalar‘𝐷)))(
·𝑠 ‘𝐷)𝐻))‘𝑋)) | 
| 19 |  | ldualvsubval.v | . . 3
⊢ 𝑉 = (Base‘𝑊) | 
| 20 |  | ldualvsubval.r | . . 3
⊢ 𝑅 = (Scalar‘𝑊) | 
| 21 |  | eqid 2737 | . . 3
⊢
(+g‘𝑅) = (+g‘𝑅) | 
| 22 |  | eqid 2737 | . . . 4
⊢
(Base‘𝑅) =
(Base‘𝑅) | 
| 23 | 12 | lmodfgrp 20867 | . . . . . . 7
⊢ (𝐷 ∈ LMod →
(Scalar‘𝐷) ∈
Grp) | 
| 24 | 3, 23 | syl 17 | . . . . . 6
⊢ (𝜑 → (Scalar‘𝐷) ∈ Grp) | 
| 25 | 12 | lmodring 20866 | . . . . . . . 8
⊢ (𝐷 ∈ LMod →
(Scalar‘𝐷) ∈
Ring) | 
| 26 | 3, 25 | syl 17 | . . . . . . 7
⊢ (𝜑 → (Scalar‘𝐷) ∈ Ring) | 
| 27 |  | eqid 2737 | . . . . . . . 8
⊢
(Base‘(Scalar‘𝐷)) = (Base‘(Scalar‘𝐷)) | 
| 28 | 27, 15 | ringidcl 20262 | . . . . . . 7
⊢
((Scalar‘𝐷)
∈ Ring → (1r‘(Scalar‘𝐷)) ∈ (Base‘(Scalar‘𝐷))) | 
| 29 | 26, 28 | syl 17 | . . . . . 6
⊢ (𝜑 →
(1r‘(Scalar‘𝐷)) ∈ (Base‘(Scalar‘𝐷))) | 
| 30 | 27, 14 | grpinvcl 19005 | . . . . . 6
⊢
(((Scalar‘𝐷)
∈ Grp ∧ (1r‘(Scalar‘𝐷)) ∈ (Base‘(Scalar‘𝐷))) →
((invg‘(Scalar‘𝐷))‘(1r‘(Scalar‘𝐷))) ∈
(Base‘(Scalar‘𝐷))) | 
| 31 | 24, 29, 30 | syl2anc 584 | . . . . 5
⊢ (𝜑 →
((invg‘(Scalar‘𝐷))‘(1r‘(Scalar‘𝐷))) ∈
(Base‘(Scalar‘𝐷))) | 
| 32 | 20, 22, 1, 12, 27, 2 | ldualsbase 39134 | . . . . 5
⊢ (𝜑 →
(Base‘(Scalar‘𝐷)) = (Base‘𝑅)) | 
| 33 | 31, 32 | eleqtrd 2843 | . . . 4
⊢ (𝜑 →
((invg‘(Scalar‘𝐷))‘(1r‘(Scalar‘𝐷))) ∈ (Base‘𝑅)) | 
| 34 | 4, 20, 22, 1, 13, 2, 33, 8 | ldualvscl 39140 | . . 3
⊢ (𝜑 →
(((invg‘(Scalar‘𝐷))‘(1r‘(Scalar‘𝐷)))(
·𝑠 ‘𝐷)𝐻) ∈ 𝐹) | 
| 35 |  | ldualvsubval.x | . . 3
⊢ (𝜑 → 𝑋 ∈ 𝑉) | 
| 36 | 19, 20, 21, 4, 1, 10, 2, 6, 34, 35 | ldualvaddval 39132 | . 2
⊢ (𝜑 → ((𝐺(+g‘𝐷)(((invg‘(Scalar‘𝐷))‘(1r‘(Scalar‘𝐷)))(
·𝑠 ‘𝐷)𝐻))‘𝑋) = ((𝐺‘𝑋)(+g‘𝑅)((((invg‘(Scalar‘𝐷))‘(1r‘(Scalar‘𝐷)))(
·𝑠 ‘𝐷)𝐻)‘𝑋))) | 
| 37 |  | eqid 2737 | . . . . . . . . 9
⊢
(invg‘𝑅) = (invg‘𝑅) | 
| 38 | 20, 37, 1, 12, 14, 2 | ldualneg 39150 | . . . . . . . 8
⊢ (𝜑 →
(invg‘(Scalar‘𝐷)) = (invg‘𝑅)) | 
| 39 |  | eqid 2737 | . . . . . . . . 9
⊢
(1r‘𝑅) = (1r‘𝑅) | 
| 40 | 20, 39, 1, 12, 15, 2 | ldual1 39149 | . . . . . . . 8
⊢ (𝜑 →
(1r‘(Scalar‘𝐷)) = (1r‘𝑅)) | 
| 41 | 38, 40 | fveq12d 6913 | . . . . . . 7
⊢ (𝜑 →
((invg‘(Scalar‘𝐷))‘(1r‘(Scalar‘𝐷))) = ((invg‘𝑅)‘(1r‘𝑅))) | 
| 42 | 41 | oveq1d 7446 | . . . . . 6
⊢ (𝜑 →
(((invg‘(Scalar‘𝐷))‘(1r‘(Scalar‘𝐷)))(
·𝑠 ‘𝐷)𝐻) = (((invg‘𝑅)‘(1r‘𝑅))( ·𝑠
‘𝐷)𝐻)) | 
| 43 | 42 | fveq1d 6908 | . . . . 5
⊢ (𝜑 →
((((invg‘(Scalar‘𝐷))‘(1r‘(Scalar‘𝐷)))(
·𝑠 ‘𝐷)𝐻)‘𝑋) = ((((invg‘𝑅)‘(1r‘𝑅))( ·𝑠
‘𝐷)𝐻)‘𝑋)) | 
| 44 |  | eqid 2737 | . . . . . 6
⊢
(.r‘𝑅) = (.r‘𝑅) | 
| 45 | 20 | lmodring 20866 | . . . . . . . . 9
⊢ (𝑊 ∈ LMod → 𝑅 ∈ Ring) | 
| 46 | 2, 45 | syl 17 | . . . . . . . 8
⊢ (𝜑 → 𝑅 ∈ Ring) | 
| 47 |  | ringgrp 20235 | . . . . . . . 8
⊢ (𝑅 ∈ Ring → 𝑅 ∈ Grp) | 
| 48 | 46, 47 | syl 17 | . . . . . . 7
⊢ (𝜑 → 𝑅 ∈ Grp) | 
| 49 | 20, 22, 39 | lmod1cl 20887 | . . . . . . . 8
⊢ (𝑊 ∈ LMod →
(1r‘𝑅)
∈ (Base‘𝑅)) | 
| 50 | 2, 49 | syl 17 | . . . . . . 7
⊢ (𝜑 → (1r‘𝑅) ∈ (Base‘𝑅)) | 
| 51 | 22, 37 | grpinvcl 19005 | . . . . . . 7
⊢ ((𝑅 ∈ Grp ∧
(1r‘𝑅)
∈ (Base‘𝑅))
→ ((invg‘𝑅)‘(1r‘𝑅)) ∈ (Base‘𝑅)) | 
| 52 | 48, 50, 51 | syl2anc 584 | . . . . . 6
⊢ (𝜑 →
((invg‘𝑅)‘(1r‘𝑅)) ∈ (Base‘𝑅)) | 
| 53 | 4, 19, 20, 22, 44, 1, 13, 2, 52, 8, 35 | ldualvsval 39139 | . . . . 5
⊢ (𝜑 →
((((invg‘𝑅)‘(1r‘𝑅))(
·𝑠 ‘𝐷)𝐻)‘𝑋) = ((𝐻‘𝑋)(.r‘𝑅)((invg‘𝑅)‘(1r‘𝑅)))) | 
| 54 | 20, 22, 19, 4 | lflcl 39065 | . . . . . . 7
⊢ ((𝑊 ∈ LMod ∧ 𝐻 ∈ 𝐹 ∧ 𝑋 ∈ 𝑉) → (𝐻‘𝑋) ∈ (Base‘𝑅)) | 
| 55 | 2, 8, 35, 54 | syl3anc 1373 | . . . . . 6
⊢ (𝜑 → (𝐻‘𝑋) ∈ (Base‘𝑅)) | 
| 56 | 22, 44, 39, 37, 46, 55 | ringnegr 20300 | . . . . 5
⊢ (𝜑 → ((𝐻‘𝑋)(.r‘𝑅)((invg‘𝑅)‘(1r‘𝑅))) =
((invg‘𝑅)‘(𝐻‘𝑋))) | 
| 57 | 43, 53, 56 | 3eqtrd 2781 | . . . 4
⊢ (𝜑 →
((((invg‘(Scalar‘𝐷))‘(1r‘(Scalar‘𝐷)))(
·𝑠 ‘𝐷)𝐻)‘𝑋) = ((invg‘𝑅)‘(𝐻‘𝑋))) | 
| 58 | 57 | oveq2d 7447 | . . 3
⊢ (𝜑 → ((𝐺‘𝑋)(+g‘𝑅)((((invg‘(Scalar‘𝐷))‘(1r‘(Scalar‘𝐷)))(
·𝑠 ‘𝐷)𝐻)‘𝑋)) = ((𝐺‘𝑋)(+g‘𝑅)((invg‘𝑅)‘(𝐻‘𝑋)))) | 
| 59 | 20, 22, 19, 4 | lflcl 39065 | . . . . 5
⊢ ((𝑊 ∈ LMod ∧ 𝐺 ∈ 𝐹 ∧ 𝑋 ∈ 𝑉) → (𝐺‘𝑋) ∈ (Base‘𝑅)) | 
| 60 | 2, 6, 35, 59 | syl3anc 1373 | . . . 4
⊢ (𝜑 → (𝐺‘𝑋) ∈ (Base‘𝑅)) | 
| 61 |  | ldualvsubval.s | . . . . 5
⊢ 𝑆 = (-g‘𝑅) | 
| 62 | 22, 21, 37, 61 | grpsubval 19003 | . . . 4
⊢ (((𝐺‘𝑋) ∈ (Base‘𝑅) ∧ (𝐻‘𝑋) ∈ (Base‘𝑅)) → ((𝐺‘𝑋)𝑆(𝐻‘𝑋)) = ((𝐺‘𝑋)(+g‘𝑅)((invg‘𝑅)‘(𝐻‘𝑋)))) | 
| 63 | 60, 55, 62 | syl2anc 584 | . . 3
⊢ (𝜑 → ((𝐺‘𝑋)𝑆(𝐻‘𝑋)) = ((𝐺‘𝑋)(+g‘𝑅)((invg‘𝑅)‘(𝐻‘𝑋)))) | 
| 64 | 58, 63 | eqtr4d 2780 | . 2
⊢ (𝜑 → ((𝐺‘𝑋)(+g‘𝑅)((((invg‘(Scalar‘𝐷))‘(1r‘(Scalar‘𝐷)))(
·𝑠 ‘𝐷)𝐻)‘𝑋)) = ((𝐺‘𝑋)𝑆(𝐻‘𝑋))) | 
| 65 | 18, 36, 64 | 3eqtrd 2781 | 1
⊢ (𝜑 → ((𝐺 − 𝐻)‘𝑋) = ((𝐺‘𝑋)𝑆(𝐻‘𝑋))) |