Proof of Theorem nvaddsub4
| Step | Hyp | Ref
| Expression |
| 1 | | neg1cn 12380 |
. . . . . 6
⊢ -1 ∈
ℂ |
| 2 | | nvpncan2.1 |
. . . . . . 7
⊢ 𝑋 = (BaseSet‘𝑈) |
| 3 | | nvpncan2.2 |
. . . . . . 7
⊢ 𝐺 = ( +𝑣
‘𝑈) |
| 4 | | eqid 2737 |
. . . . . . 7
⊢ (
·𝑠OLD ‘𝑈) = ( ·𝑠OLD
‘𝑈) |
| 5 | 2, 3, 4 | nvdi 30649 |
. . . . . 6
⊢ ((𝑈 ∈ NrmCVec ∧ (-1 ∈
ℂ ∧ 𝐶 ∈
𝑋 ∧ 𝐷 ∈ 𝑋)) → (-1(
·𝑠OLD ‘𝑈)(𝐶𝐺𝐷)) = ((-1(
·𝑠OLD ‘𝑈)𝐶)𝐺(-1( ·𝑠OLD
‘𝑈)𝐷))) |
| 6 | 1, 5 | mp3anr1 1460 |
. . . . 5
⊢ ((𝑈 ∈ NrmCVec ∧ (𝐶 ∈ 𝑋 ∧ 𝐷 ∈ 𝑋)) → (-1(
·𝑠OLD ‘𝑈)(𝐶𝐺𝐷)) = ((-1(
·𝑠OLD ‘𝑈)𝐶)𝐺(-1( ·𝑠OLD
‘𝑈)𝐷))) |
| 7 | 6 | 3adant2 1132 |
. . . 4
⊢ ((𝑈 ∈ NrmCVec ∧ (𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋) ∧ (𝐶 ∈ 𝑋 ∧ 𝐷 ∈ 𝑋)) → (-1(
·𝑠OLD ‘𝑈)(𝐶𝐺𝐷)) = ((-1(
·𝑠OLD ‘𝑈)𝐶)𝐺(-1( ·𝑠OLD
‘𝑈)𝐷))) |
| 8 | 7 | oveq2d 7447 |
. . 3
⊢ ((𝑈 ∈ NrmCVec ∧ (𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋) ∧ (𝐶 ∈ 𝑋 ∧ 𝐷 ∈ 𝑋)) → ((𝐴𝐺𝐵)𝐺(-1( ·𝑠OLD
‘𝑈)(𝐶𝐺𝐷))) = ((𝐴𝐺𝐵)𝐺((-1( ·𝑠OLD
‘𝑈)𝐶)𝐺(-1( ·𝑠OLD
‘𝑈)𝐷)))) |
| 9 | 2, 4 | nvscl 30645 |
. . . . . . 7
⊢ ((𝑈 ∈ NrmCVec ∧ -1 ∈
ℂ ∧ 𝐶 ∈
𝑋) → (-1(
·𝑠OLD ‘𝑈)𝐶) ∈ 𝑋) |
| 10 | 1, 9 | mp3an2 1451 |
. . . . . 6
⊢ ((𝑈 ∈ NrmCVec ∧ 𝐶 ∈ 𝑋) → (-1(
·𝑠OLD ‘𝑈)𝐶) ∈ 𝑋) |
| 11 | 2, 4 | nvscl 30645 |
. . . . . . 7
⊢ ((𝑈 ∈ NrmCVec ∧ -1 ∈
ℂ ∧ 𝐷 ∈
𝑋) → (-1(
·𝑠OLD ‘𝑈)𝐷) ∈ 𝑋) |
| 12 | 1, 11 | mp3an2 1451 |
. . . . . 6
⊢ ((𝑈 ∈ NrmCVec ∧ 𝐷 ∈ 𝑋) → (-1(
·𝑠OLD ‘𝑈)𝐷) ∈ 𝑋) |
| 13 | 10, 12 | anim12dan 619 |
. . . . 5
⊢ ((𝑈 ∈ NrmCVec ∧ (𝐶 ∈ 𝑋 ∧ 𝐷 ∈ 𝑋)) → ((-1(
·𝑠OLD ‘𝑈)𝐶) ∈ 𝑋 ∧ (-1(
·𝑠OLD ‘𝑈)𝐷) ∈ 𝑋)) |
| 14 | 13 | 3adant2 1132 |
. . . 4
⊢ ((𝑈 ∈ NrmCVec ∧ (𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋) ∧ (𝐶 ∈ 𝑋 ∧ 𝐷 ∈ 𝑋)) → ((-1(
·𝑠OLD ‘𝑈)𝐶) ∈ 𝑋 ∧ (-1(
·𝑠OLD ‘𝑈)𝐷) ∈ 𝑋)) |
| 15 | 2, 3 | nvadd4 30644 |
. . . 4
⊢ ((𝑈 ∈ NrmCVec ∧ (𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋) ∧ ((-1(
·𝑠OLD ‘𝑈)𝐶) ∈ 𝑋 ∧ (-1(
·𝑠OLD ‘𝑈)𝐷) ∈ 𝑋)) → ((𝐴𝐺𝐵)𝐺((-1( ·𝑠OLD
‘𝑈)𝐶)𝐺(-1( ·𝑠OLD
‘𝑈)𝐷))) = ((𝐴𝐺(-1( ·𝑠OLD
‘𝑈)𝐶))𝐺(𝐵𝐺(-1( ·𝑠OLD
‘𝑈)𝐷)))) |
| 16 | 14, 15 | syld3an3 1411 |
. . 3
⊢ ((𝑈 ∈ NrmCVec ∧ (𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋) ∧ (𝐶 ∈ 𝑋 ∧ 𝐷 ∈ 𝑋)) → ((𝐴𝐺𝐵)𝐺((-1( ·𝑠OLD
‘𝑈)𝐶)𝐺(-1( ·𝑠OLD
‘𝑈)𝐷))) = ((𝐴𝐺(-1( ·𝑠OLD
‘𝑈)𝐶))𝐺(𝐵𝐺(-1( ·𝑠OLD
‘𝑈)𝐷)))) |
| 17 | 8, 16 | eqtrd 2777 |
. 2
⊢ ((𝑈 ∈ NrmCVec ∧ (𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋) ∧ (𝐶 ∈ 𝑋 ∧ 𝐷 ∈ 𝑋)) → ((𝐴𝐺𝐵)𝐺(-1( ·𝑠OLD
‘𝑈)(𝐶𝐺𝐷))) = ((𝐴𝐺(-1( ·𝑠OLD
‘𝑈)𝐶))𝐺(𝐵𝐺(-1( ·𝑠OLD
‘𝑈)𝐷)))) |
| 18 | | simp1 1137 |
. . 3
⊢ ((𝑈 ∈ NrmCVec ∧ (𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋) ∧ (𝐶 ∈ 𝑋 ∧ 𝐷 ∈ 𝑋)) → 𝑈 ∈ NrmCVec) |
| 19 | 2, 3 | nvgcl 30639 |
. . . . 5
⊢ ((𝑈 ∈ NrmCVec ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋) → (𝐴𝐺𝐵) ∈ 𝑋) |
| 20 | 19 | 3expb 1121 |
. . . 4
⊢ ((𝑈 ∈ NrmCVec ∧ (𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋)) → (𝐴𝐺𝐵) ∈ 𝑋) |
| 21 | 20 | 3adant3 1133 |
. . 3
⊢ ((𝑈 ∈ NrmCVec ∧ (𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋) ∧ (𝐶 ∈ 𝑋 ∧ 𝐷 ∈ 𝑋)) → (𝐴𝐺𝐵) ∈ 𝑋) |
| 22 | 2, 3 | nvgcl 30639 |
. . . . 5
⊢ ((𝑈 ∈ NrmCVec ∧ 𝐶 ∈ 𝑋 ∧ 𝐷 ∈ 𝑋) → (𝐶𝐺𝐷) ∈ 𝑋) |
| 23 | 22 | 3expb 1121 |
. . . 4
⊢ ((𝑈 ∈ NrmCVec ∧ (𝐶 ∈ 𝑋 ∧ 𝐷 ∈ 𝑋)) → (𝐶𝐺𝐷) ∈ 𝑋) |
| 24 | 23 | 3adant2 1132 |
. . 3
⊢ ((𝑈 ∈ NrmCVec ∧ (𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋) ∧ (𝐶 ∈ 𝑋 ∧ 𝐷 ∈ 𝑋)) → (𝐶𝐺𝐷) ∈ 𝑋) |
| 25 | | nvpncan2.3 |
. . . 4
⊢ 𝑀 = ( −𝑣
‘𝑈) |
| 26 | 2, 3, 4, 25 | nvmval 30661 |
. . 3
⊢ ((𝑈 ∈ NrmCVec ∧ (𝐴𝐺𝐵) ∈ 𝑋 ∧ (𝐶𝐺𝐷) ∈ 𝑋) → ((𝐴𝐺𝐵)𝑀(𝐶𝐺𝐷)) = ((𝐴𝐺𝐵)𝐺(-1( ·𝑠OLD
‘𝑈)(𝐶𝐺𝐷)))) |
| 27 | 18, 21, 24, 26 | syl3anc 1373 |
. 2
⊢ ((𝑈 ∈ NrmCVec ∧ (𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋) ∧ (𝐶 ∈ 𝑋 ∧ 𝐷 ∈ 𝑋)) → ((𝐴𝐺𝐵)𝑀(𝐶𝐺𝐷)) = ((𝐴𝐺𝐵)𝐺(-1( ·𝑠OLD
‘𝑈)(𝐶𝐺𝐷)))) |
| 28 | 2, 3, 4, 25 | nvmval 30661 |
. . . . 5
⊢ ((𝑈 ∈ NrmCVec ∧ 𝐴 ∈ 𝑋 ∧ 𝐶 ∈ 𝑋) → (𝐴𝑀𝐶) = (𝐴𝐺(-1( ·𝑠OLD
‘𝑈)𝐶))) |
| 29 | 28 | 3adant3r 1182 |
. . . 4
⊢ ((𝑈 ∈ NrmCVec ∧ 𝐴 ∈ 𝑋 ∧ (𝐶 ∈ 𝑋 ∧ 𝐷 ∈ 𝑋)) → (𝐴𝑀𝐶) = (𝐴𝐺(-1( ·𝑠OLD
‘𝑈)𝐶))) |
| 30 | 29 | 3adant2r 1180 |
. . 3
⊢ ((𝑈 ∈ NrmCVec ∧ (𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋) ∧ (𝐶 ∈ 𝑋 ∧ 𝐷 ∈ 𝑋)) → (𝐴𝑀𝐶) = (𝐴𝐺(-1( ·𝑠OLD
‘𝑈)𝐶))) |
| 31 | 2, 3, 4, 25 | nvmval 30661 |
. . . . 5
⊢ ((𝑈 ∈ NrmCVec ∧ 𝐵 ∈ 𝑋 ∧ 𝐷 ∈ 𝑋) → (𝐵𝑀𝐷) = (𝐵𝐺(-1( ·𝑠OLD
‘𝑈)𝐷))) |
| 32 | 31 | 3adant3l 1181 |
. . . 4
⊢ ((𝑈 ∈ NrmCVec ∧ 𝐵 ∈ 𝑋 ∧ (𝐶 ∈ 𝑋 ∧ 𝐷 ∈ 𝑋)) → (𝐵𝑀𝐷) = (𝐵𝐺(-1( ·𝑠OLD
‘𝑈)𝐷))) |
| 33 | 32 | 3adant2l 1179 |
. . 3
⊢ ((𝑈 ∈ NrmCVec ∧ (𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋) ∧ (𝐶 ∈ 𝑋 ∧ 𝐷 ∈ 𝑋)) → (𝐵𝑀𝐷) = (𝐵𝐺(-1( ·𝑠OLD
‘𝑈)𝐷))) |
| 34 | 30, 33 | oveq12d 7449 |
. 2
⊢ ((𝑈 ∈ NrmCVec ∧ (𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋) ∧ (𝐶 ∈ 𝑋 ∧ 𝐷 ∈ 𝑋)) → ((𝐴𝑀𝐶)𝐺(𝐵𝑀𝐷)) = ((𝐴𝐺(-1( ·𝑠OLD
‘𝑈)𝐶))𝐺(𝐵𝐺(-1( ·𝑠OLD
‘𝑈)𝐷)))) |
| 35 | 17, 27, 34 | 3eqtr4d 2787 |
1
⊢ ((𝑈 ∈ NrmCVec ∧ (𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋) ∧ (𝐶 ∈ 𝑋 ∧ 𝐷 ∈ 𝑋)) → ((𝐴𝐺𝐵)𝑀(𝐶𝐺𝐷)) = ((𝐴𝑀𝐶)𝐺(𝐵𝑀𝐷))) |