Proof of Theorem ip2subdi
| Step | Hyp | Ref | Expression | 
|---|
| 1 |  | eqid 2737 | . . . 4
⊢
(Base‘𝐹) =
(Base‘𝐹) | 
| 2 |  | ip2subdi.p | . . . 4
⊢  + =
(+g‘𝐹) | 
| 3 |  | ipsubdir.s | . . . 4
⊢ 𝑆 = (-g‘𝐹) | 
| 4 |  | ip2subdi.1 | . . . . . . 7
⊢ (𝜑 → 𝑊 ∈ PreHil) | 
| 5 |  | phllmod 21648 | . . . . . . 7
⊢ (𝑊 ∈ PreHil → 𝑊 ∈ LMod) | 
| 6 | 4, 5 | syl 17 | . . . . . 6
⊢ (𝜑 → 𝑊 ∈ LMod) | 
| 7 |  | phlsrng.f | . . . . . . 7
⊢ 𝐹 = (Scalar‘𝑊) | 
| 8 | 7 | lmodring 20866 | . . . . . 6
⊢ (𝑊 ∈ LMod → 𝐹 ∈ Ring) | 
| 9 | 6, 8 | syl 17 | . . . . 5
⊢ (𝜑 → 𝐹 ∈ Ring) | 
| 10 |  | ringabl 20278 | . . . . 5
⊢ (𝐹 ∈ Ring → 𝐹 ∈ Abel) | 
| 11 | 9, 10 | syl 17 | . . . 4
⊢ (𝜑 → 𝐹 ∈ Abel) | 
| 12 |  | ip2subdi.2 | . . . . 5
⊢ (𝜑 → 𝐴 ∈ 𝑉) | 
| 13 |  | ip2subdi.4 | . . . . 5
⊢ (𝜑 → 𝐶 ∈ 𝑉) | 
| 14 |  | phllmhm.h | . . . . . 6
⊢  , =
(·𝑖‘𝑊) | 
| 15 |  | phllmhm.v | . . . . . 6
⊢ 𝑉 = (Base‘𝑊) | 
| 16 | 7, 14, 15, 1 | ipcl 21651 | . . . . 5
⊢ ((𝑊 ∈ PreHil ∧ 𝐴 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉) → (𝐴 , 𝐶) ∈ (Base‘𝐹)) | 
| 17 | 4, 12, 13, 16 | syl3anc 1373 | . . . 4
⊢ (𝜑 → (𝐴 , 𝐶) ∈ (Base‘𝐹)) | 
| 18 |  | ip2subdi.5 | . . . . 5
⊢ (𝜑 → 𝐷 ∈ 𝑉) | 
| 19 | 7, 14, 15, 1 | ipcl 21651 | . . . . 5
⊢ ((𝑊 ∈ PreHil ∧ 𝐴 ∈ 𝑉 ∧ 𝐷 ∈ 𝑉) → (𝐴 , 𝐷) ∈ (Base‘𝐹)) | 
| 20 | 4, 12, 18, 19 | syl3anc 1373 | . . . 4
⊢ (𝜑 → (𝐴 , 𝐷) ∈ (Base‘𝐹)) | 
| 21 |  | ip2subdi.3 | . . . . 5
⊢ (𝜑 → 𝐵 ∈ 𝑉) | 
| 22 | 7, 14, 15, 1 | ipcl 21651 | . . . . 5
⊢ ((𝑊 ∈ PreHil ∧ 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉) → (𝐵 , 𝐶) ∈ (Base‘𝐹)) | 
| 23 | 4, 21, 13, 22 | syl3anc 1373 | . . . 4
⊢ (𝜑 → (𝐵 , 𝐶) ∈ (Base‘𝐹)) | 
| 24 | 1, 2, 3, 11, 17, 20, 23 | ablsubsub4 19836 | . . 3
⊢ (𝜑 → (((𝐴 , 𝐶)𝑆(𝐴 , 𝐷))𝑆(𝐵 , 𝐶)) = ((𝐴 , 𝐶)𝑆((𝐴 , 𝐷) + (𝐵 , 𝐶)))) | 
| 25 | 24 | oveq1d 7446 | . 2
⊢ (𝜑 → ((((𝐴 , 𝐶)𝑆(𝐴 , 𝐷))𝑆(𝐵 , 𝐶)) + (𝐵 , 𝐷)) = (((𝐴 , 𝐶)𝑆((𝐴 , 𝐷) + (𝐵 , 𝐶))) + (𝐵 , 𝐷))) | 
| 26 |  | ipsubdir.m | . . . . . 6
⊢  − =
(-g‘𝑊) | 
| 27 | 15, 26 | lmodvsubcl 20905 | . . . . 5
⊢ ((𝑊 ∈ LMod ∧ 𝐶 ∈ 𝑉 ∧ 𝐷 ∈ 𝑉) → (𝐶 − 𝐷) ∈ 𝑉) | 
| 28 | 6, 13, 18, 27 | syl3anc 1373 | . . . 4
⊢ (𝜑 → (𝐶 − 𝐷) ∈ 𝑉) | 
| 29 | 7, 14, 15, 26, 3 | ipsubdir 21660 | . . . 4
⊢ ((𝑊 ∈ PreHil ∧ (𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ∧ (𝐶 − 𝐷) ∈ 𝑉)) → ((𝐴 − 𝐵) , (𝐶 − 𝐷)) = ((𝐴 , (𝐶 − 𝐷))𝑆(𝐵 , (𝐶 − 𝐷)))) | 
| 30 | 4, 12, 21, 28, 29 | syl13anc 1374 | . . 3
⊢ (𝜑 → ((𝐴 − 𝐵) , (𝐶 − 𝐷)) = ((𝐴 , (𝐶 − 𝐷))𝑆(𝐵 , (𝐶 − 𝐷)))) | 
| 31 | 7, 14, 15, 26, 3 | ipsubdi 21661 | . . . . 5
⊢ ((𝑊 ∈ PreHil ∧ (𝐴 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉 ∧ 𝐷 ∈ 𝑉)) → (𝐴 , (𝐶 − 𝐷)) = ((𝐴 , 𝐶)𝑆(𝐴 , 𝐷))) | 
| 32 | 4, 12, 13, 18, 31 | syl13anc 1374 | . . . 4
⊢ (𝜑 → (𝐴 , (𝐶 − 𝐷)) = ((𝐴 , 𝐶)𝑆(𝐴 , 𝐷))) | 
| 33 | 7, 14, 15, 26, 3 | ipsubdi 21661 | . . . . 5
⊢ ((𝑊 ∈ PreHil ∧ (𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉 ∧ 𝐷 ∈ 𝑉)) → (𝐵 , (𝐶 − 𝐷)) = ((𝐵 , 𝐶)𝑆(𝐵 , 𝐷))) | 
| 34 | 4, 21, 13, 18, 33 | syl13anc 1374 | . . . 4
⊢ (𝜑 → (𝐵 , (𝐶 − 𝐷)) = ((𝐵 , 𝐶)𝑆(𝐵 , 𝐷))) | 
| 35 | 32, 34 | oveq12d 7449 | . . 3
⊢ (𝜑 → ((𝐴 , (𝐶 − 𝐷))𝑆(𝐵 , (𝐶 − 𝐷))) = (((𝐴 , 𝐶)𝑆(𝐴 , 𝐷))𝑆((𝐵 , 𝐶)𝑆(𝐵 , 𝐷)))) | 
| 36 |  | ringgrp 20235 | . . . . . 6
⊢ (𝐹 ∈ Ring → 𝐹 ∈ Grp) | 
| 37 | 9, 36 | syl 17 | . . . . 5
⊢ (𝜑 → 𝐹 ∈ Grp) | 
| 38 | 1, 3 | grpsubcl 19038 | . . . . 5
⊢ ((𝐹 ∈ Grp ∧ (𝐴 , 𝐶) ∈ (Base‘𝐹) ∧ (𝐴 , 𝐷) ∈ (Base‘𝐹)) → ((𝐴 , 𝐶)𝑆(𝐴 , 𝐷)) ∈ (Base‘𝐹)) | 
| 39 | 37, 17, 20, 38 | syl3anc 1373 | . . . 4
⊢ (𝜑 → ((𝐴 , 𝐶)𝑆(𝐴 , 𝐷)) ∈ (Base‘𝐹)) | 
| 40 | 7, 14, 15, 1 | ipcl 21651 | . . . . 5
⊢ ((𝑊 ∈ PreHil ∧ 𝐵 ∈ 𝑉 ∧ 𝐷 ∈ 𝑉) → (𝐵 , 𝐷) ∈ (Base‘𝐹)) | 
| 41 | 4, 21, 18, 40 | syl3anc 1373 | . . . 4
⊢ (𝜑 → (𝐵 , 𝐷) ∈ (Base‘𝐹)) | 
| 42 | 1, 2, 3, 11, 39, 23, 41 | ablsubsub 19835 | . . 3
⊢ (𝜑 → (((𝐴 , 𝐶)𝑆(𝐴 , 𝐷))𝑆((𝐵 , 𝐶)𝑆(𝐵 , 𝐷))) = ((((𝐴 , 𝐶)𝑆(𝐴 , 𝐷))𝑆(𝐵 , 𝐶)) + (𝐵 , 𝐷))) | 
| 43 | 30, 35, 42 | 3eqtrd 2781 | . 2
⊢ (𝜑 → ((𝐴 − 𝐵) , (𝐶 − 𝐷)) = ((((𝐴 , 𝐶)𝑆(𝐴 , 𝐷))𝑆(𝐵 , 𝐶)) + (𝐵 , 𝐷))) | 
| 44 | 1, 2 | ringacl 20275 | . . . 4
⊢ ((𝐹 ∈ Ring ∧ (𝐴 , 𝐷) ∈ (Base‘𝐹) ∧ (𝐵 , 𝐶) ∈ (Base‘𝐹)) → ((𝐴 , 𝐷) + (𝐵 , 𝐶)) ∈ (Base‘𝐹)) | 
| 45 | 9, 20, 23, 44 | syl3anc 1373 | . . 3
⊢ (𝜑 → ((𝐴 , 𝐷) + (𝐵 , 𝐶)) ∈ (Base‘𝐹)) | 
| 46 | 1, 2, 3 | abladdsub 19830 | . . 3
⊢ ((𝐹 ∈ Abel ∧ ((𝐴 , 𝐶) ∈ (Base‘𝐹) ∧ (𝐵 , 𝐷) ∈ (Base‘𝐹) ∧ ((𝐴 , 𝐷) + (𝐵 , 𝐶)) ∈ (Base‘𝐹))) → (((𝐴 , 𝐶) + (𝐵 , 𝐷))𝑆((𝐴 , 𝐷) + (𝐵 , 𝐶))) = (((𝐴 , 𝐶)𝑆((𝐴 , 𝐷) + (𝐵 , 𝐶))) + (𝐵 , 𝐷))) | 
| 47 | 11, 17, 41, 45, 46 | syl13anc 1374 | . 2
⊢ (𝜑 → (((𝐴 , 𝐶) + (𝐵 , 𝐷))𝑆((𝐴 , 𝐷) + (𝐵 , 𝐶))) = (((𝐴 , 𝐶)𝑆((𝐴 , 𝐷) + (𝐵 , 𝐶))) + (𝐵 , 𝐷))) | 
| 48 | 25, 43, 47 | 3eqtr4d 2787 | 1
⊢ (𝜑 → ((𝐴 − 𝐵) , (𝐶 − 𝐷)) = (((𝐴 , 𝐶) + (𝐵 , 𝐷))𝑆((𝐴 , 𝐷) + (𝐵 , 𝐶)))) |