HSE Home Hilbert Space Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  HSE Home  >  Th. List  >  lnopunilem1 Structured version   Visualization version   GIF version

Theorem lnopunilem1 31848
Description: Lemma for lnopunii 31850. (Contributed by NM, 14-May-2005.) (New usage is discouraged.)
Hypotheses
Ref Expression
lnopunilem.1 ๐‘‡ โˆˆ LinOp
lnopunilem.2 โˆ€๐‘ฅ โˆˆ โ„‹ (normโ„Žโ€˜(๐‘‡โ€˜๐‘ฅ)) = (normโ„Žโ€˜๐‘ฅ)
lnopunilem.3 ๐ด โˆˆ โ„‹
lnopunilem.4 ๐ต โˆˆ โ„‹
lnopunilem1.5 ๐ถ โˆˆ โ„‚
Assertion
Ref Expression
lnopunilem1 (โ„œโ€˜(๐ถ ยท ((๐‘‡โ€˜๐ด) ยทih (๐‘‡โ€˜๐ต)))) = (โ„œโ€˜(๐ถ ยท (๐ด ยทih ๐ต)))
Distinct variable group:   ๐‘ฅ,๐‘‡
Allowed substitution hints:   ๐ด(๐‘ฅ)   ๐ต(๐‘ฅ)   ๐ถ(๐‘ฅ)

Proof of Theorem lnopunilem1
Dummy variable ๐‘ฆ is distinct from all other variables.
StepHypRef Expression
1 lnopunilem1.5 . . . 4 ๐ถ โˆˆ โ„‚
2 lnopunilem.3 . . . . . 6 ๐ด โˆˆ โ„‹
3 lnopunilem.1 . . . . . . . 8 ๐‘‡ โˆˆ LinOp
43lnopfi 31807 . . . . . . 7 ๐‘‡: โ„‹โŸถ โ„‹
54ffvelcdmi 7098 . . . . . 6 (๐ด โˆˆ โ„‹ โ†’ (๐‘‡โ€˜๐ด) โˆˆ โ„‹)
62, 5ax-mp 5 . . . . 5 (๐‘‡โ€˜๐ด) โˆˆ โ„‹
7 lnopunilem.4 . . . . . 6 ๐ต โˆˆ โ„‹
84ffvelcdmi 7098 . . . . . 6 (๐ต โˆˆ โ„‹ โ†’ (๐‘‡โ€˜๐ต) โˆˆ โ„‹)
97, 8ax-mp 5 . . . . 5 (๐‘‡โ€˜๐ต) โˆˆ โ„‹
106, 9hicli 30919 . . . 4 ((๐‘‡โ€˜๐ด) ยทih (๐‘‡โ€˜๐ต)) โˆˆ โ„‚
111, 10mulcli 11261 . . 3 (๐ถ ยท ((๐‘‡โ€˜๐ด) ยทih (๐‘‡โ€˜๐ต))) โˆˆ โ„‚
12 reval 15095 . . 3 ((๐ถ ยท ((๐‘‡โ€˜๐ด) ยทih (๐‘‡โ€˜๐ต))) โˆˆ โ„‚ โ†’ (โ„œโ€˜(๐ถ ยท ((๐‘‡โ€˜๐ด) ยทih (๐‘‡โ€˜๐ต)))) = (((๐ถ ยท ((๐‘‡โ€˜๐ด) ยทih (๐‘‡โ€˜๐ต))) + (โˆ—โ€˜(๐ถ ยท ((๐‘‡โ€˜๐ด) ยทih (๐‘‡โ€˜๐ต))))) / 2))
1311, 12ax-mp 5 . 2 (โ„œโ€˜(๐ถ ยท ((๐‘‡โ€˜๐ด) ยทih (๐‘‡โ€˜๐ต)))) = (((๐ถ ยท ((๐‘‡โ€˜๐ด) ยทih (๐‘‡โ€˜๐ต))) + (โˆ—โ€˜(๐ถ ยท ((๐‘‡โ€˜๐ด) ยทih (๐‘‡โ€˜๐ต))))) / 2)
142, 7hicli 30919 . . . . 5 (๐ด ยทih ๐ต) โˆˆ โ„‚
151, 14mulcli 11261 . . . 4 (๐ถ ยท (๐ด ยทih ๐ต)) โˆˆ โ„‚
16 reval 15095 . . . 4 ((๐ถ ยท (๐ด ยทih ๐ต)) โˆˆ โ„‚ โ†’ (โ„œโ€˜(๐ถ ยท (๐ด ยทih ๐ต))) = (((๐ถ ยท (๐ด ยทih ๐ต)) + (โˆ—โ€˜(๐ถ ยท (๐ด ยทih ๐ต)))) / 2))
1715, 16ax-mp 5 . . 3 (โ„œโ€˜(๐ถ ยท (๐ด ยทih ๐ต))) = (((๐ถ ยท (๐ด ยทih ๐ต)) + (โˆ—โ€˜(๐ถ ยท (๐ด ยทih ๐ต)))) / 2)
18 lnopunilem.2 . . . . . . . . . . . . 13 โˆ€๐‘ฅ โˆˆ โ„‹ (normโ„Žโ€˜(๐‘‡โ€˜๐‘ฅ)) = (normโ„Žโ€˜๐‘ฅ)
19 2fveq3 6907 . . . . . . . . . . . . . . 15 (๐‘ฅ = ๐‘ฆ โ†’ (normโ„Žโ€˜(๐‘‡โ€˜๐‘ฅ)) = (normโ„Žโ€˜(๐‘‡โ€˜๐‘ฆ)))
20 fveq2 6902 . . . . . . . . . . . . . . 15 (๐‘ฅ = ๐‘ฆ โ†’ (normโ„Žโ€˜๐‘ฅ) = (normโ„Žโ€˜๐‘ฆ))
2119, 20eqeq12d 2744 . . . . . . . . . . . . . 14 (๐‘ฅ = ๐‘ฆ โ†’ ((normโ„Žโ€˜(๐‘‡โ€˜๐‘ฅ)) = (normโ„Žโ€˜๐‘ฅ) โ†” (normโ„Žโ€˜(๐‘‡โ€˜๐‘ฆ)) = (normโ„Žโ€˜๐‘ฆ)))
2221cbvralvw 3232 . . . . . . . . . . . . 13 (โˆ€๐‘ฅ โˆˆ โ„‹ (normโ„Žโ€˜(๐‘‡โ€˜๐‘ฅ)) = (normโ„Žโ€˜๐‘ฅ) โ†” โˆ€๐‘ฆ โˆˆ โ„‹ (normโ„Žโ€˜(๐‘‡โ€˜๐‘ฆ)) = (normโ„Žโ€˜๐‘ฆ))
2318, 22mpbi 229 . . . . . . . . . . . 12 โˆ€๐‘ฆ โˆˆ โ„‹ (normโ„Žโ€˜(๐‘‡โ€˜๐‘ฆ)) = (normโ„Žโ€˜๐‘ฆ)
24 oveq1 7433 . . . . . . . . . . . . . 14 ((normโ„Žโ€˜(๐‘‡โ€˜๐‘ฆ)) = (normโ„Žโ€˜๐‘ฆ) โ†’ ((normโ„Žโ€˜(๐‘‡โ€˜๐‘ฆ))โ†‘2) = ((normโ„Žโ€˜๐‘ฆ)โ†‘2))
254ffvelcdmi 7098 . . . . . . . . . . . . . . . 16 (๐‘ฆ โˆˆ โ„‹ โ†’ (๐‘‡โ€˜๐‘ฆ) โˆˆ โ„‹)
26 normsq 30972 . . . . . . . . . . . . . . . 16 ((๐‘‡โ€˜๐‘ฆ) โˆˆ โ„‹ โ†’ ((normโ„Žโ€˜(๐‘‡โ€˜๐‘ฆ))โ†‘2) = ((๐‘‡โ€˜๐‘ฆ) ยทih (๐‘‡โ€˜๐‘ฆ)))
2725, 26syl 17 . . . . . . . . . . . . . . 15 (๐‘ฆ โˆˆ โ„‹ โ†’ ((normโ„Žโ€˜(๐‘‡โ€˜๐‘ฆ))โ†‘2) = ((๐‘‡โ€˜๐‘ฆ) ยทih (๐‘‡โ€˜๐‘ฆ)))
28 normsq 30972 . . . . . . . . . . . . . . 15 (๐‘ฆ โˆˆ โ„‹ โ†’ ((normโ„Žโ€˜๐‘ฆ)โ†‘2) = (๐‘ฆ ยทih ๐‘ฆ))
2927, 28eqeq12d 2744 . . . . . . . . . . . . . 14 (๐‘ฆ โˆˆ โ„‹ โ†’ (((normโ„Žโ€˜(๐‘‡โ€˜๐‘ฆ))โ†‘2) = ((normโ„Žโ€˜๐‘ฆ)โ†‘2) โ†” ((๐‘‡โ€˜๐‘ฆ) ยทih (๐‘‡โ€˜๐‘ฆ)) = (๐‘ฆ ยทih ๐‘ฆ)))
3024, 29imbitrid 243 . . . . . . . . . . . . 13 (๐‘ฆ โˆˆ โ„‹ โ†’ ((normโ„Žโ€˜(๐‘‡โ€˜๐‘ฆ)) = (normโ„Žโ€˜๐‘ฆ) โ†’ ((๐‘‡โ€˜๐‘ฆ) ยทih (๐‘‡โ€˜๐‘ฆ)) = (๐‘ฆ ยทih ๐‘ฆ)))
3130ralimia 3077 . . . . . . . . . . . 12 (โˆ€๐‘ฆ โˆˆ โ„‹ (normโ„Žโ€˜(๐‘‡โ€˜๐‘ฆ)) = (normโ„Žโ€˜๐‘ฆ) โ†’ โˆ€๐‘ฆ โˆˆ โ„‹ ((๐‘‡โ€˜๐‘ฆ) ยทih (๐‘‡โ€˜๐‘ฆ)) = (๐‘ฆ ยทih ๐‘ฆ))
3223, 31ax-mp 5 . . . . . . . . . . 11 โˆ€๐‘ฆ โˆˆ โ„‹ ((๐‘‡โ€˜๐‘ฆ) ยทih (๐‘‡โ€˜๐‘ฆ)) = (๐‘ฆ ยทih ๐‘ฆ)
33 fveq2 6902 . . . . . . . . . . . . . 14 (๐‘ฆ = ๐ด โ†’ (๐‘‡โ€˜๐‘ฆ) = (๐‘‡โ€˜๐ด))
3433, 33oveq12d 7444 . . . . . . . . . . . . 13 (๐‘ฆ = ๐ด โ†’ ((๐‘‡โ€˜๐‘ฆ) ยทih (๐‘‡โ€˜๐‘ฆ)) = ((๐‘‡โ€˜๐ด) ยทih (๐‘‡โ€˜๐ด)))
35 id 22 . . . . . . . . . . . . . 14 (๐‘ฆ = ๐ด โ†’ ๐‘ฆ = ๐ด)
3635, 35oveq12d 7444 . . . . . . . . . . . . 13 (๐‘ฆ = ๐ด โ†’ (๐‘ฆ ยทih ๐‘ฆ) = (๐ด ยทih ๐ด))
3734, 36eqeq12d 2744 . . . . . . . . . . . 12 (๐‘ฆ = ๐ด โ†’ (((๐‘‡โ€˜๐‘ฆ) ยทih (๐‘‡โ€˜๐‘ฆ)) = (๐‘ฆ ยทih ๐‘ฆ) โ†” ((๐‘‡โ€˜๐ด) ยทih (๐‘‡โ€˜๐ด)) = (๐ด ยทih ๐ด)))
3837rspcv 3607 . . . . . . . . . . 11 (๐ด โˆˆ โ„‹ โ†’ (โˆ€๐‘ฆ โˆˆ โ„‹ ((๐‘‡โ€˜๐‘ฆ) ยทih (๐‘‡โ€˜๐‘ฆ)) = (๐‘ฆ ยทih ๐‘ฆ) โ†’ ((๐‘‡โ€˜๐ด) ยทih (๐‘‡โ€˜๐ด)) = (๐ด ยทih ๐ด)))
392, 32, 38mp2 9 . . . . . . . . . 10 ((๐‘‡โ€˜๐ด) ยทih (๐‘‡โ€˜๐ด)) = (๐ด ยทih ๐ด)
4039oveq2i 7437 . . . . . . . . 9 ((โˆ—โ€˜๐ถ) ยท ((๐‘‡โ€˜๐ด) ยทih (๐‘‡โ€˜๐ด))) = ((โˆ—โ€˜๐ถ) ยท (๐ด ยทih ๐ด))
4140oveq2i 7437 . . . . . . . 8 (๐ถ ยท ((โˆ—โ€˜๐ถ) ยท ((๐‘‡โ€˜๐ด) ยทih (๐‘‡โ€˜๐ด)))) = (๐ถ ยท ((โˆ—โ€˜๐ถ) ยท (๐ด ยทih ๐ด)))
42 fveq2 6902 . . . . . . . . . . . 12 (๐‘ฆ = ๐ต โ†’ (๐‘‡โ€˜๐‘ฆ) = (๐‘‡โ€˜๐ต))
4342, 42oveq12d 7444 . . . . . . . . . . 11 (๐‘ฆ = ๐ต โ†’ ((๐‘‡โ€˜๐‘ฆ) ยทih (๐‘‡โ€˜๐‘ฆ)) = ((๐‘‡โ€˜๐ต) ยทih (๐‘‡โ€˜๐ต)))
44 id 22 . . . . . . . . . . . 12 (๐‘ฆ = ๐ต โ†’ ๐‘ฆ = ๐ต)
4544, 44oveq12d 7444 . . . . . . . . . . 11 (๐‘ฆ = ๐ต โ†’ (๐‘ฆ ยทih ๐‘ฆ) = (๐ต ยทih ๐ต))
4643, 45eqeq12d 2744 . . . . . . . . . 10 (๐‘ฆ = ๐ต โ†’ (((๐‘‡โ€˜๐‘ฆ) ยทih (๐‘‡โ€˜๐‘ฆ)) = (๐‘ฆ ยทih ๐‘ฆ) โ†” ((๐‘‡โ€˜๐ต) ยทih (๐‘‡โ€˜๐ต)) = (๐ต ยทih ๐ต)))
4746rspcv 3607 . . . . . . . . 9 (๐ต โˆˆ โ„‹ โ†’ (โˆ€๐‘ฆ โˆˆ โ„‹ ((๐‘‡โ€˜๐‘ฆ) ยทih (๐‘‡โ€˜๐‘ฆ)) = (๐‘ฆ ยทih ๐‘ฆ) โ†’ ((๐‘‡โ€˜๐ต) ยทih (๐‘‡โ€˜๐ต)) = (๐ต ยทih ๐ต)))
487, 32, 47mp2 9 . . . . . . . 8 ((๐‘‡โ€˜๐ต) ยทih (๐‘‡โ€˜๐ต)) = (๐ต ยทih ๐ต)
4941, 48oveq12i 7438 . . . . . . 7 ((๐ถ ยท ((โˆ—โ€˜๐ถ) ยท ((๐‘‡โ€˜๐ด) ยทih (๐‘‡โ€˜๐ด)))) + ((๐‘‡โ€˜๐ต) ยทih (๐‘‡โ€˜๐ต))) = ((๐ถ ยท ((โˆ—โ€˜๐ถ) ยท (๐ด ยทih ๐ด))) + (๐ต ยทih ๐ต))
5049oveq1i 7436 . . . . . 6 (((๐ถ ยท ((โˆ—โ€˜๐ถ) ยท ((๐‘‡โ€˜๐ด) ยทih (๐‘‡โ€˜๐ด)))) + ((๐‘‡โ€˜๐ต) ยทih (๐‘‡โ€˜๐ต))) + ((๐ถ ยท ((๐‘‡โ€˜๐ด) ยทih (๐‘‡โ€˜๐ต))) + (โˆ—โ€˜(๐ถ ยท ((๐‘‡โ€˜๐ด) ยทih (๐‘‡โ€˜๐ต)))))) = (((๐ถ ยท ((โˆ—โ€˜๐ถ) ยท (๐ด ยทih ๐ด))) + (๐ต ยทih ๐ต)) + ((๐ถ ยท ((๐‘‡โ€˜๐ด) ยทih (๐‘‡โ€˜๐ต))) + (โˆ—โ€˜(๐ถ ยท ((๐‘‡โ€˜๐ด) ยทih (๐‘‡โ€˜๐ต))))))
511cjcli 15158 . . . . . . . . . 10 (โˆ—โ€˜๐ถ) โˆˆ โ„‚
526, 6hicli 30919 . . . . . . . . . 10 ((๐‘‡โ€˜๐ด) ยทih (๐‘‡โ€˜๐ด)) โˆˆ โ„‚
5351, 52mulcli 11261 . . . . . . . . 9 ((โˆ—โ€˜๐ถ) ยท ((๐‘‡โ€˜๐ด) ยทih (๐‘‡โ€˜๐ด))) โˆˆ โ„‚
541, 53mulcli 11261 . . . . . . . 8 (๐ถ ยท ((โˆ—โ€˜๐ถ) ยท ((๐‘‡โ€˜๐ด) ยทih (๐‘‡โ€˜๐ด)))) โˆˆ โ„‚
559, 9hicli 30919 . . . . . . . 8 ((๐‘‡โ€˜๐ต) ยทih (๐‘‡โ€˜๐ต)) โˆˆ โ„‚
5611cjcli 15158 . . . . . . . 8 (โˆ—โ€˜(๐ถ ยท ((๐‘‡โ€˜๐ด) ยทih (๐‘‡โ€˜๐ต)))) โˆˆ โ„‚
5754, 55, 11, 56add42i 11479 . . . . . . 7 (((๐ถ ยท ((โˆ—โ€˜๐ถ) ยท ((๐‘‡โ€˜๐ด) ยทih (๐‘‡โ€˜๐ด)))) + ((๐‘‡โ€˜๐ต) ยทih (๐‘‡โ€˜๐ต))) + ((๐ถ ยท ((๐‘‡โ€˜๐ด) ยทih (๐‘‡โ€˜๐ต))) + (โˆ—โ€˜(๐ถ ยท ((๐‘‡โ€˜๐ด) ยทih (๐‘‡โ€˜๐ต)))))) = (((๐ถ ยท ((โˆ—โ€˜๐ถ) ยท ((๐‘‡โ€˜๐ด) ยทih (๐‘‡โ€˜๐ด)))) + (๐ถ ยท ((๐‘‡โ€˜๐ด) ยทih (๐‘‡โ€˜๐ต)))) + ((โˆ—โ€˜(๐ถ ยท ((๐‘‡โ€˜๐ด) ยทih (๐‘‡โ€˜๐ต)))) + ((๐‘‡โ€˜๐ต) ยทih (๐‘‡โ€˜๐ต))))
582, 2hicli 30919 . . . . . . . . . . 11 (๐ด ยทih ๐ด) โˆˆ โ„‚
5951, 58mulcli 11261 . . . . . . . . . 10 ((โˆ—โ€˜๐ถ) ยท (๐ด ยทih ๐ด)) โˆˆ โ„‚
601, 59mulcli 11261 . . . . . . . . 9 (๐ถ ยท ((โˆ—โ€˜๐ถ) ยท (๐ด ยทih ๐ด))) โˆˆ โ„‚
617, 7hicli 30919 . . . . . . . . 9 (๐ต ยทih ๐ต) โˆˆ โ„‚
6215cjcli 15158 . . . . . . . . 9 (โˆ—โ€˜(๐ถ ยท (๐ด ยทih ๐ต))) โˆˆ โ„‚
6360, 61, 15, 62add42i 11479 . . . . . . . 8 (((๐ถ ยท ((โˆ—โ€˜๐ถ) ยท (๐ด ยทih ๐ด))) + (๐ต ยทih ๐ต)) + ((๐ถ ยท (๐ด ยทih ๐ต)) + (โˆ—โ€˜(๐ถ ยท (๐ด ยทih ๐ต))))) = (((๐ถ ยท ((โˆ—โ€˜๐ถ) ยท (๐ด ยทih ๐ด))) + (๐ถ ยท (๐ด ยทih ๐ต))) + ((โˆ—โ€˜(๐ถ ยท (๐ด ยทih ๐ต))) + (๐ต ยทih ๐ต)))
641, 2hvmulcli 30852 . . . . . . . . . . . 12 (๐ถ ยทโ„Ž ๐ด) โˆˆ โ„‹
6564, 7hvaddcli 30856 . . . . . . . . . . 11 ((๐ถ ยทโ„Ž ๐ด) +โ„Ž ๐ต) โˆˆ โ„‹
66 fveq2 6902 . . . . . . . . . . . . . 14 (๐‘ฆ = ((๐ถ ยทโ„Ž ๐ด) +โ„Ž ๐ต) โ†’ (๐‘‡โ€˜๐‘ฆ) = (๐‘‡โ€˜((๐ถ ยทโ„Ž ๐ด) +โ„Ž ๐ต)))
6766, 66oveq12d 7444 . . . . . . . . . . . . 13 (๐‘ฆ = ((๐ถ ยทโ„Ž ๐ด) +โ„Ž ๐ต) โ†’ ((๐‘‡โ€˜๐‘ฆ) ยทih (๐‘‡โ€˜๐‘ฆ)) = ((๐‘‡โ€˜((๐ถ ยทโ„Ž ๐ด) +โ„Ž ๐ต)) ยทih (๐‘‡โ€˜((๐ถ ยทโ„Ž ๐ด) +โ„Ž ๐ต))))
68 id 22 . . . . . . . . . . . . . 14 (๐‘ฆ = ((๐ถ ยทโ„Ž ๐ด) +โ„Ž ๐ต) โ†’ ๐‘ฆ = ((๐ถ ยทโ„Ž ๐ด) +โ„Ž ๐ต))
6968, 68oveq12d 7444 . . . . . . . . . . . . 13 (๐‘ฆ = ((๐ถ ยทโ„Ž ๐ด) +โ„Ž ๐ต) โ†’ (๐‘ฆ ยทih ๐‘ฆ) = (((๐ถ ยทโ„Ž ๐ด) +โ„Ž ๐ต) ยทih ((๐ถ ยทโ„Ž ๐ด) +โ„Ž ๐ต)))
7067, 69eqeq12d 2744 . . . . . . . . . . . 12 (๐‘ฆ = ((๐ถ ยทโ„Ž ๐ด) +โ„Ž ๐ต) โ†’ (((๐‘‡โ€˜๐‘ฆ) ยทih (๐‘‡โ€˜๐‘ฆ)) = (๐‘ฆ ยทih ๐‘ฆ) โ†” ((๐‘‡โ€˜((๐ถ ยทโ„Ž ๐ด) +โ„Ž ๐ต)) ยทih (๐‘‡โ€˜((๐ถ ยทโ„Ž ๐ด) +โ„Ž ๐ต))) = (((๐ถ ยทโ„Ž ๐ด) +โ„Ž ๐ต) ยทih ((๐ถ ยทโ„Ž ๐ด) +โ„Ž ๐ต))))
7170rspcv 3607 . . . . . . . . . . 11 (((๐ถ ยทโ„Ž ๐ด) +โ„Ž ๐ต) โˆˆ โ„‹ โ†’ (โˆ€๐‘ฆ โˆˆ โ„‹ ((๐‘‡โ€˜๐‘ฆ) ยทih (๐‘‡โ€˜๐‘ฆ)) = (๐‘ฆ ยทih ๐‘ฆ) โ†’ ((๐‘‡โ€˜((๐ถ ยทโ„Ž ๐ด) +โ„Ž ๐ต)) ยทih (๐‘‡โ€˜((๐ถ ยทโ„Ž ๐ด) +โ„Ž ๐ต))) = (((๐ถ ยทโ„Ž ๐ด) +โ„Ž ๐ต) ยทih ((๐ถ ยทโ„Ž ๐ด) +โ„Ž ๐ต))))
7265, 32, 71mp2 9 . . . . . . . . . 10 ((๐‘‡โ€˜((๐ถ ยทโ„Ž ๐ด) +โ„Ž ๐ต)) ยทih (๐‘‡โ€˜((๐ถ ยทโ„Ž ๐ด) +โ„Ž ๐ต))) = (((๐ถ ยทโ„Ž ๐ด) +โ„Ž ๐ต) ยทih ((๐ถ ยทโ„Ž ๐ด) +โ„Ž ๐ต))
73 ax-his2 30921 . . . . . . . . . . 11 (((๐ถ ยทโ„Ž ๐ด) โˆˆ โ„‹ โˆง ๐ต โˆˆ โ„‹ โˆง ((๐ถ ยทโ„Ž ๐ด) +โ„Ž ๐ต) โˆˆ โ„‹) โ†’ (((๐ถ ยทโ„Ž ๐ด) +โ„Ž ๐ต) ยทih ((๐ถ ยทโ„Ž ๐ด) +โ„Ž ๐ต)) = (((๐ถ ยทโ„Ž ๐ด) ยทih ((๐ถ ยทโ„Ž ๐ด) +โ„Ž ๐ต)) + (๐ต ยทih ((๐ถ ยทโ„Ž ๐ด) +โ„Ž ๐ต))))
7464, 7, 65, 73mp3an 1457 . . . . . . . . . 10 (((๐ถ ยทโ„Ž ๐ด) +โ„Ž ๐ต) ยทih ((๐ถ ยทโ„Ž ๐ด) +โ„Ž ๐ต)) = (((๐ถ ยทโ„Ž ๐ด) ยทih ((๐ถ ยทโ„Ž ๐ด) +โ„Ž ๐ต)) + (๐ต ยทih ((๐ถ ยทโ„Ž ๐ด) +โ„Ž ๐ต)))
75 ax-his3 30922 . . . . . . . . . . . . 13 ((๐ถ โˆˆ โ„‚ โˆง ๐ด โˆˆ โ„‹ โˆง ((๐ถ ยทโ„Ž ๐ด) +โ„Ž ๐ต) โˆˆ โ„‹) โ†’ ((๐ถ ยทโ„Ž ๐ด) ยทih ((๐ถ ยทโ„Ž ๐ด) +โ„Ž ๐ต)) = (๐ถ ยท (๐ด ยทih ((๐ถ ยทโ„Ž ๐ด) +โ„Ž ๐ต))))
761, 2, 65, 75mp3an 1457 . . . . . . . . . . . 12 ((๐ถ ยทโ„Ž ๐ด) ยทih ((๐ถ ยทโ„Ž ๐ด) +โ„Ž ๐ต)) = (๐ถ ยท (๐ด ยทih ((๐ถ ยทโ„Ž ๐ด) +โ„Ž ๐ต)))
77 his7 30928 . . . . . . . . . . . . . . 15 ((๐ด โˆˆ โ„‹ โˆง (๐ถ ยทโ„Ž ๐ด) โˆˆ โ„‹ โˆง ๐ต โˆˆ โ„‹) โ†’ (๐ด ยทih ((๐ถ ยทโ„Ž ๐ด) +โ„Ž ๐ต)) = ((๐ด ยทih (๐ถ ยทโ„Ž ๐ด)) + (๐ด ยทih ๐ต)))
782, 64, 7, 77mp3an 1457 . . . . . . . . . . . . . 14 (๐ด ยทih ((๐ถ ยทโ„Ž ๐ด) +โ„Ž ๐ต)) = ((๐ด ยทih (๐ถ ยทโ„Ž ๐ด)) + (๐ด ยทih ๐ต))
79 his5 30924 . . . . . . . . . . . . . . . 16 ((๐ถ โˆˆ โ„‚ โˆง ๐ด โˆˆ โ„‹ โˆง ๐ด โˆˆ โ„‹) โ†’ (๐ด ยทih (๐ถ ยทโ„Ž ๐ด)) = ((โˆ—โ€˜๐ถ) ยท (๐ด ยทih ๐ด)))
801, 2, 2, 79mp3an 1457 . . . . . . . . . . . . . . 15 (๐ด ยทih (๐ถ ยทโ„Ž ๐ด)) = ((โˆ—โ€˜๐ถ) ยท (๐ด ยทih ๐ด))
8180oveq1i 7436 . . . . . . . . . . . . . 14 ((๐ด ยทih (๐ถ ยทโ„Ž ๐ด)) + (๐ด ยทih ๐ต)) = (((โˆ—โ€˜๐ถ) ยท (๐ด ยทih ๐ด)) + (๐ด ยทih ๐ต))
8278, 81eqtri 2756 . . . . . . . . . . . . 13 (๐ด ยทih ((๐ถ ยทโ„Ž ๐ด) +โ„Ž ๐ต)) = (((โˆ—โ€˜๐ถ) ยท (๐ด ยทih ๐ด)) + (๐ด ยทih ๐ต))
8382oveq2i 7437 . . . . . . . . . . . 12 (๐ถ ยท (๐ด ยทih ((๐ถ ยทโ„Ž ๐ด) +โ„Ž ๐ต))) = (๐ถ ยท (((โˆ—โ€˜๐ถ) ยท (๐ด ยทih ๐ด)) + (๐ด ยทih ๐ต)))
841, 59, 14adddii 11266 . . . . . . . . . . . 12 (๐ถ ยท (((โˆ—โ€˜๐ถ) ยท (๐ด ยทih ๐ด)) + (๐ด ยทih ๐ต))) = ((๐ถ ยท ((โˆ—โ€˜๐ถ) ยท (๐ด ยทih ๐ด))) + (๐ถ ยท (๐ด ยทih ๐ต)))
8576, 83, 843eqtri 2760 . . . . . . . . . . 11 ((๐ถ ยทโ„Ž ๐ด) ยทih ((๐ถ ยทโ„Ž ๐ด) +โ„Ž ๐ต)) = ((๐ถ ยท ((โˆ—โ€˜๐ถ) ยท (๐ด ยทih ๐ด))) + (๐ถ ยท (๐ด ยทih ๐ต)))
86 his7 30928 . . . . . . . . . . . . 13 ((๐ต โˆˆ โ„‹ โˆง (๐ถ ยทโ„Ž ๐ด) โˆˆ โ„‹ โˆง ๐ต โˆˆ โ„‹) โ†’ (๐ต ยทih ((๐ถ ยทโ„Ž ๐ด) +โ„Ž ๐ต)) = ((๐ต ยทih (๐ถ ยทโ„Ž ๐ด)) + (๐ต ยทih ๐ต)))
877, 64, 7, 86mp3an 1457 . . . . . . . . . . . 12 (๐ต ยทih ((๐ถ ยทโ„Ž ๐ด) +โ„Ž ๐ต)) = ((๐ต ยทih (๐ถ ยทโ„Ž ๐ด)) + (๐ต ยทih ๐ต))
88 his5 30924 . . . . . . . . . . . . . . 15 ((๐ถ โˆˆ โ„‚ โˆง ๐ต โˆˆ โ„‹ โˆง ๐ด โˆˆ โ„‹) โ†’ (๐ต ยทih (๐ถ ยทโ„Ž ๐ด)) = ((โˆ—โ€˜๐ถ) ยท (๐ต ยทih ๐ด)))
891, 7, 2, 88mp3an 1457 . . . . . . . . . . . . . 14 (๐ต ยทih (๐ถ ยทโ„Ž ๐ด)) = ((โˆ—โ€˜๐ถ) ยท (๐ต ยทih ๐ด))
901, 14cjmuli 15178 . . . . . . . . . . . . . . 15 (โˆ—โ€˜(๐ถ ยท (๐ด ยทih ๐ต))) = ((โˆ—โ€˜๐ถ) ยท (โˆ—โ€˜(๐ด ยทih ๐ต)))
917, 2his1i 30938 . . . . . . . . . . . . . . . 16 (๐ต ยทih ๐ด) = (โˆ—โ€˜(๐ด ยทih ๐ต))
9291oveq2i 7437 . . . . . . . . . . . . . . 15 ((โˆ—โ€˜๐ถ) ยท (๐ต ยทih ๐ด)) = ((โˆ—โ€˜๐ถ) ยท (โˆ—โ€˜(๐ด ยทih ๐ต)))
9390, 92eqtr4i 2759 . . . . . . . . . . . . . 14 (โˆ—โ€˜(๐ถ ยท (๐ด ยทih ๐ต))) = ((โˆ—โ€˜๐ถ) ยท (๐ต ยทih ๐ด))
9489, 93eqtr4i 2759 . . . . . . . . . . . . 13 (๐ต ยทih (๐ถ ยทโ„Ž ๐ด)) = (โˆ—โ€˜(๐ถ ยท (๐ด ยทih ๐ต)))
9594oveq1i 7436 . . . . . . . . . . . 12 ((๐ต ยทih (๐ถ ยทโ„Ž ๐ด)) + (๐ต ยทih ๐ต)) = ((โˆ—โ€˜(๐ถ ยท (๐ด ยทih ๐ต))) + (๐ต ยทih ๐ต))
9687, 95eqtri 2756 . . . . . . . . . . 11 (๐ต ยทih ((๐ถ ยทโ„Ž ๐ด) +โ„Ž ๐ต)) = ((โˆ—โ€˜(๐ถ ยท (๐ด ยทih ๐ต))) + (๐ต ยทih ๐ต))
9785, 96oveq12i 7438 . . . . . . . . . 10 (((๐ถ ยทโ„Ž ๐ด) ยทih ((๐ถ ยทโ„Ž ๐ด) +โ„Ž ๐ต)) + (๐ต ยทih ((๐ถ ยทโ„Ž ๐ด) +โ„Ž ๐ต))) = (((๐ถ ยท ((โˆ—โ€˜๐ถ) ยท (๐ด ยทih ๐ด))) + (๐ถ ยท (๐ด ยทih ๐ต))) + ((โˆ—โ€˜(๐ถ ยท (๐ด ยทih ๐ต))) + (๐ต ยทih ๐ต)))
9872, 74, 973eqtrri 2761 . . . . . . . . 9 (((๐ถ ยท ((โˆ—โ€˜๐ถ) ยท (๐ด ยทih ๐ด))) + (๐ถ ยท (๐ด ยทih ๐ต))) + ((โˆ—โ€˜(๐ถ ยท (๐ด ยทih ๐ต))) + (๐ต ยทih ๐ต))) = ((๐‘‡โ€˜((๐ถ ยทโ„Ž ๐ด) +โ„Ž ๐ต)) ยทih (๐‘‡โ€˜((๐ถ ยทโ„Ž ๐ด) +โ„Ž ๐ต)))
993lnopli 31806 . . . . . . . . . . . 12 ((๐ถ โˆˆ โ„‚ โˆง ๐ด โˆˆ โ„‹ โˆง ๐ต โˆˆ โ„‹) โ†’ (๐‘‡โ€˜((๐ถ ยทโ„Ž ๐ด) +โ„Ž ๐ต)) = ((๐ถ ยทโ„Ž (๐‘‡โ€˜๐ด)) +โ„Ž (๐‘‡โ€˜๐ต)))
1001, 2, 7, 99mp3an 1457 . . . . . . . . . . 11 (๐‘‡โ€˜((๐ถ ยทโ„Ž ๐ด) +โ„Ž ๐ต)) = ((๐ถ ยทโ„Ž (๐‘‡โ€˜๐ด)) +โ„Ž (๐‘‡โ€˜๐ต))
101100, 100oveq12i 7438 . . . . . . . . . 10 ((๐‘‡โ€˜((๐ถ ยทโ„Ž ๐ด) +โ„Ž ๐ต)) ยทih (๐‘‡โ€˜((๐ถ ยทโ„Ž ๐ด) +โ„Ž ๐ต))) = (((๐ถ ยทโ„Ž (๐‘‡โ€˜๐ด)) +โ„Ž (๐‘‡โ€˜๐ต)) ยทih ((๐ถ ยทโ„Ž (๐‘‡โ€˜๐ด)) +โ„Ž (๐‘‡โ€˜๐ต)))
1021, 6hvmulcli 30852 . . . . . . . . . . 11 (๐ถ ยทโ„Ž (๐‘‡โ€˜๐ด)) โˆˆ โ„‹
103102, 9hvaddcli 30856 . . . . . . . . . . 11 ((๐ถ ยทโ„Ž (๐‘‡โ€˜๐ด)) +โ„Ž (๐‘‡โ€˜๐ต)) โˆˆ โ„‹
104 ax-his2 30921 . . . . . . . . . . 11 (((๐ถ ยทโ„Ž (๐‘‡โ€˜๐ด)) โˆˆ โ„‹ โˆง (๐‘‡โ€˜๐ต) โˆˆ โ„‹ โˆง ((๐ถ ยทโ„Ž (๐‘‡โ€˜๐ด)) +โ„Ž (๐‘‡โ€˜๐ต)) โˆˆ โ„‹) โ†’ (((๐ถ ยทโ„Ž (๐‘‡โ€˜๐ด)) +โ„Ž (๐‘‡โ€˜๐ต)) ยทih ((๐ถ ยทโ„Ž (๐‘‡โ€˜๐ด)) +โ„Ž (๐‘‡โ€˜๐ต))) = (((๐ถ ยทโ„Ž (๐‘‡โ€˜๐ด)) ยทih ((๐ถ ยทโ„Ž (๐‘‡โ€˜๐ด)) +โ„Ž (๐‘‡โ€˜๐ต))) + ((๐‘‡โ€˜๐ต) ยทih ((๐ถ ยทโ„Ž (๐‘‡โ€˜๐ด)) +โ„Ž (๐‘‡โ€˜๐ต)))))
105102, 9, 103, 104mp3an 1457 . . . . . . . . . 10 (((๐ถ ยทโ„Ž (๐‘‡โ€˜๐ด)) +โ„Ž (๐‘‡โ€˜๐ต)) ยทih ((๐ถ ยทโ„Ž (๐‘‡โ€˜๐ด)) +โ„Ž (๐‘‡โ€˜๐ต))) = (((๐ถ ยทโ„Ž (๐‘‡โ€˜๐ด)) ยทih ((๐ถ ยทโ„Ž (๐‘‡โ€˜๐ด)) +โ„Ž (๐‘‡โ€˜๐ต))) + ((๐‘‡โ€˜๐ต) ยทih ((๐ถ ยทโ„Ž (๐‘‡โ€˜๐ด)) +โ„Ž (๐‘‡โ€˜๐ต))))
106101, 105eqtri 2756 . . . . . . . . 9 ((๐‘‡โ€˜((๐ถ ยทโ„Ž ๐ด) +โ„Ž ๐ต)) ยทih (๐‘‡โ€˜((๐ถ ยทโ„Ž ๐ด) +โ„Ž ๐ต))) = (((๐ถ ยทโ„Ž (๐‘‡โ€˜๐ด)) ยทih ((๐ถ ยทโ„Ž (๐‘‡โ€˜๐ด)) +โ„Ž (๐‘‡โ€˜๐ต))) + ((๐‘‡โ€˜๐ต) ยทih ((๐ถ ยทโ„Ž (๐‘‡โ€˜๐ด)) +โ„Ž (๐‘‡โ€˜๐ต))))
107 ax-his3 30922 . . . . . . . . . . . 12 ((๐ถ โˆˆ โ„‚ โˆง (๐‘‡โ€˜๐ด) โˆˆ โ„‹ โˆง ((๐ถ ยทโ„Ž (๐‘‡โ€˜๐ด)) +โ„Ž (๐‘‡โ€˜๐ต)) โˆˆ โ„‹) โ†’ ((๐ถ ยทโ„Ž (๐‘‡โ€˜๐ด)) ยทih ((๐ถ ยทโ„Ž (๐‘‡โ€˜๐ด)) +โ„Ž (๐‘‡โ€˜๐ต))) = (๐ถ ยท ((๐‘‡โ€˜๐ด) ยทih ((๐ถ ยทโ„Ž (๐‘‡โ€˜๐ด)) +โ„Ž (๐‘‡โ€˜๐ต)))))
1081, 6, 103, 107mp3an 1457 . . . . . . . . . . 11 ((๐ถ ยทโ„Ž (๐‘‡โ€˜๐ด)) ยทih ((๐ถ ยทโ„Ž (๐‘‡โ€˜๐ด)) +โ„Ž (๐‘‡โ€˜๐ต))) = (๐ถ ยท ((๐‘‡โ€˜๐ด) ยทih ((๐ถ ยทโ„Ž (๐‘‡โ€˜๐ด)) +โ„Ž (๐‘‡โ€˜๐ต))))
109 his7 30928 . . . . . . . . . . . . . 14 (((๐‘‡โ€˜๐ด) โˆˆ โ„‹ โˆง (๐ถ ยทโ„Ž (๐‘‡โ€˜๐ด)) โˆˆ โ„‹ โˆง (๐‘‡โ€˜๐ต) โˆˆ โ„‹) โ†’ ((๐‘‡โ€˜๐ด) ยทih ((๐ถ ยทโ„Ž (๐‘‡โ€˜๐ด)) +โ„Ž (๐‘‡โ€˜๐ต))) = (((๐‘‡โ€˜๐ด) ยทih (๐ถ ยทโ„Ž (๐‘‡โ€˜๐ด))) + ((๐‘‡โ€˜๐ด) ยทih (๐‘‡โ€˜๐ต))))
1106, 102, 9, 109mp3an 1457 . . . . . . . . . . . . 13 ((๐‘‡โ€˜๐ด) ยทih ((๐ถ ยทโ„Ž (๐‘‡โ€˜๐ด)) +โ„Ž (๐‘‡โ€˜๐ต))) = (((๐‘‡โ€˜๐ด) ยทih (๐ถ ยทโ„Ž (๐‘‡โ€˜๐ด))) + ((๐‘‡โ€˜๐ด) ยทih (๐‘‡โ€˜๐ต)))
111 his5 30924 . . . . . . . . . . . . . . 15 ((๐ถ โˆˆ โ„‚ โˆง (๐‘‡โ€˜๐ด) โˆˆ โ„‹ โˆง (๐‘‡โ€˜๐ด) โˆˆ โ„‹) โ†’ ((๐‘‡โ€˜๐ด) ยทih (๐ถ ยทโ„Ž (๐‘‡โ€˜๐ด))) = ((โˆ—โ€˜๐ถ) ยท ((๐‘‡โ€˜๐ด) ยทih (๐‘‡โ€˜๐ด))))
1121, 6, 6, 111mp3an 1457 . . . . . . . . . . . . . 14 ((๐‘‡โ€˜๐ด) ยทih (๐ถ ยทโ„Ž (๐‘‡โ€˜๐ด))) = ((โˆ—โ€˜๐ถ) ยท ((๐‘‡โ€˜๐ด) ยทih (๐‘‡โ€˜๐ด)))
113112oveq1i 7436 . . . . . . . . . . . . 13 (((๐‘‡โ€˜๐ด) ยทih (๐ถ ยทโ„Ž (๐‘‡โ€˜๐ด))) + ((๐‘‡โ€˜๐ด) ยทih (๐‘‡โ€˜๐ต))) = (((โˆ—โ€˜๐ถ) ยท ((๐‘‡โ€˜๐ด) ยทih (๐‘‡โ€˜๐ด))) + ((๐‘‡โ€˜๐ด) ยทih (๐‘‡โ€˜๐ต)))
114110, 113eqtri 2756 . . . . . . . . . . . 12 ((๐‘‡โ€˜๐ด) ยทih ((๐ถ ยทโ„Ž (๐‘‡โ€˜๐ด)) +โ„Ž (๐‘‡โ€˜๐ต))) = (((โˆ—โ€˜๐ถ) ยท ((๐‘‡โ€˜๐ด) ยทih (๐‘‡โ€˜๐ด))) + ((๐‘‡โ€˜๐ด) ยทih (๐‘‡โ€˜๐ต)))
115114oveq2i 7437 . . . . . . . . . . 11 (๐ถ ยท ((๐‘‡โ€˜๐ด) ยทih ((๐ถ ยทโ„Ž (๐‘‡โ€˜๐ด)) +โ„Ž (๐‘‡โ€˜๐ต)))) = (๐ถ ยท (((โˆ—โ€˜๐ถ) ยท ((๐‘‡โ€˜๐ด) ยทih (๐‘‡โ€˜๐ด))) + ((๐‘‡โ€˜๐ด) ยทih (๐‘‡โ€˜๐ต))))
1161, 53, 10adddii 11266 . . . . . . . . . . 11 (๐ถ ยท (((โˆ—โ€˜๐ถ) ยท ((๐‘‡โ€˜๐ด) ยทih (๐‘‡โ€˜๐ด))) + ((๐‘‡โ€˜๐ด) ยทih (๐‘‡โ€˜๐ต)))) = ((๐ถ ยท ((โˆ—โ€˜๐ถ) ยท ((๐‘‡โ€˜๐ด) ยทih (๐‘‡โ€˜๐ด)))) + (๐ถ ยท ((๐‘‡โ€˜๐ด) ยทih (๐‘‡โ€˜๐ต))))
117108, 115, 1163eqtri 2760 . . . . . . . . . 10 ((๐ถ ยทโ„Ž (๐‘‡โ€˜๐ด)) ยทih ((๐ถ ยทโ„Ž (๐‘‡โ€˜๐ด)) +โ„Ž (๐‘‡โ€˜๐ต))) = ((๐ถ ยท ((โˆ—โ€˜๐ถ) ยท ((๐‘‡โ€˜๐ด) ยทih (๐‘‡โ€˜๐ด)))) + (๐ถ ยท ((๐‘‡โ€˜๐ด) ยทih (๐‘‡โ€˜๐ต))))
118 his7 30928 . . . . . . . . . . . 12 (((๐‘‡โ€˜๐ต) โˆˆ โ„‹ โˆง (๐ถ ยทโ„Ž (๐‘‡โ€˜๐ด)) โˆˆ โ„‹ โˆง (๐‘‡โ€˜๐ต) โˆˆ โ„‹) โ†’ ((๐‘‡โ€˜๐ต) ยทih ((๐ถ ยทโ„Ž (๐‘‡โ€˜๐ด)) +โ„Ž (๐‘‡โ€˜๐ต))) = (((๐‘‡โ€˜๐ต) ยทih (๐ถ ยทโ„Ž (๐‘‡โ€˜๐ด))) + ((๐‘‡โ€˜๐ต) ยทih (๐‘‡โ€˜๐ต))))
1199, 102, 9, 118mp3an 1457 . . . . . . . . . . 11 ((๐‘‡โ€˜๐ต) ยทih ((๐ถ ยทโ„Ž (๐‘‡โ€˜๐ด)) +โ„Ž (๐‘‡โ€˜๐ต))) = (((๐‘‡โ€˜๐ต) ยทih (๐ถ ยทโ„Ž (๐‘‡โ€˜๐ด))) + ((๐‘‡โ€˜๐ต) ยทih (๐‘‡โ€˜๐ต)))
120 his5 30924 . . . . . . . . . . . . . 14 ((๐ถ โˆˆ โ„‚ โˆง (๐‘‡โ€˜๐ต) โˆˆ โ„‹ โˆง (๐‘‡โ€˜๐ด) โˆˆ โ„‹) โ†’ ((๐‘‡โ€˜๐ต) ยทih (๐ถ ยทโ„Ž (๐‘‡โ€˜๐ด))) = ((โˆ—โ€˜๐ถ) ยท ((๐‘‡โ€˜๐ต) ยทih (๐‘‡โ€˜๐ด))))
1211, 9, 6, 120mp3an 1457 . . . . . . . . . . . . 13 ((๐‘‡โ€˜๐ต) ยทih (๐ถ ยทโ„Ž (๐‘‡โ€˜๐ด))) = ((โˆ—โ€˜๐ถ) ยท ((๐‘‡โ€˜๐ต) ยทih (๐‘‡โ€˜๐ด)))
1221, 10cjmuli 15178 . . . . . . . . . . . . . 14 (โˆ—โ€˜(๐ถ ยท ((๐‘‡โ€˜๐ด) ยทih (๐‘‡โ€˜๐ต)))) = ((โˆ—โ€˜๐ถ) ยท (โˆ—โ€˜((๐‘‡โ€˜๐ด) ยทih (๐‘‡โ€˜๐ต))))
1239, 6his1i 30938 . . . . . . . . . . . . . . 15 ((๐‘‡โ€˜๐ต) ยทih (๐‘‡โ€˜๐ด)) = (โˆ—โ€˜((๐‘‡โ€˜๐ด) ยทih (๐‘‡โ€˜๐ต)))
124123oveq2i 7437 . . . . . . . . . . . . . 14 ((โˆ—โ€˜๐ถ) ยท ((๐‘‡โ€˜๐ต) ยทih (๐‘‡โ€˜๐ด))) = ((โˆ—โ€˜๐ถ) ยท (โˆ—โ€˜((๐‘‡โ€˜๐ด) ยทih (๐‘‡โ€˜๐ต))))
125122, 124eqtr4i 2759 . . . . . . . . . . . . 13 (โˆ—โ€˜(๐ถ ยท ((๐‘‡โ€˜๐ด) ยทih (๐‘‡โ€˜๐ต)))) = ((โˆ—โ€˜๐ถ) ยท ((๐‘‡โ€˜๐ต) ยทih (๐‘‡โ€˜๐ด)))
126121, 125eqtr4i 2759 . . . . . . . . . . . 12 ((๐‘‡โ€˜๐ต) ยทih (๐ถ ยทโ„Ž (๐‘‡โ€˜๐ด))) = (โˆ—โ€˜(๐ถ ยท ((๐‘‡โ€˜๐ด) ยทih (๐‘‡โ€˜๐ต))))
127126oveq1i 7436 . . . . . . . . . . 11 (((๐‘‡โ€˜๐ต) ยทih (๐ถ ยทโ„Ž (๐‘‡โ€˜๐ด))) + ((๐‘‡โ€˜๐ต) ยทih (๐‘‡โ€˜๐ต))) = ((โˆ—โ€˜(๐ถ ยท ((๐‘‡โ€˜๐ด) ยทih (๐‘‡โ€˜๐ต)))) + ((๐‘‡โ€˜๐ต) ยทih (๐‘‡โ€˜๐ต)))
128119, 127eqtri 2756 . . . . . . . . . 10 ((๐‘‡โ€˜๐ต) ยทih ((๐ถ ยทโ„Ž (๐‘‡โ€˜๐ด)) +โ„Ž (๐‘‡โ€˜๐ต))) = ((โˆ—โ€˜(๐ถ ยท ((๐‘‡โ€˜๐ด) ยทih (๐‘‡โ€˜๐ต)))) + ((๐‘‡โ€˜๐ต) ยทih (๐‘‡โ€˜๐ต)))
129117, 128oveq12i 7438 . . . . . . . . 9 (((๐ถ ยทโ„Ž (๐‘‡โ€˜๐ด)) ยทih ((๐ถ ยทโ„Ž (๐‘‡โ€˜๐ด)) +โ„Ž (๐‘‡โ€˜๐ต))) + ((๐‘‡โ€˜๐ต) ยทih ((๐ถ ยทโ„Ž (๐‘‡โ€˜๐ด)) +โ„Ž (๐‘‡โ€˜๐ต)))) = (((๐ถ ยท ((โˆ—โ€˜๐ถ) ยท ((๐‘‡โ€˜๐ด) ยทih (๐‘‡โ€˜๐ด)))) + (๐ถ ยท ((๐‘‡โ€˜๐ด) ยทih (๐‘‡โ€˜๐ต)))) + ((โˆ—โ€˜(๐ถ ยท ((๐‘‡โ€˜๐ด) ยทih (๐‘‡โ€˜๐ต)))) + ((๐‘‡โ€˜๐ต) ยทih (๐‘‡โ€˜๐ต))))
13098, 106, 1293eqtrri 2761 . . . . . . . 8 (((๐ถ ยท ((โˆ—โ€˜๐ถ) ยท ((๐‘‡โ€˜๐ด) ยทih (๐‘‡โ€˜๐ด)))) + (๐ถ ยท ((๐‘‡โ€˜๐ด) ยทih (๐‘‡โ€˜๐ต)))) + ((โˆ—โ€˜(๐ถ ยท ((๐‘‡โ€˜๐ด) ยทih (๐‘‡โ€˜๐ต)))) + ((๐‘‡โ€˜๐ต) ยทih (๐‘‡โ€˜๐ต)))) = (((๐ถ ยท ((โˆ—โ€˜๐ถ) ยท (๐ด ยทih ๐ด))) + (๐ถ ยท (๐ด ยทih ๐ต))) + ((โˆ—โ€˜(๐ถ ยท (๐ด ยทih ๐ต))) + (๐ต ยทih ๐ต)))
13163, 130eqtr4i 2759 . . . . . . 7 (((๐ถ ยท ((โˆ—โ€˜๐ถ) ยท (๐ด ยทih ๐ด))) + (๐ต ยทih ๐ต)) + ((๐ถ ยท (๐ด ยทih ๐ต)) + (โˆ—โ€˜(๐ถ ยท (๐ด ยทih ๐ต))))) = (((๐ถ ยท ((โˆ—โ€˜๐ถ) ยท ((๐‘‡โ€˜๐ด) ยทih (๐‘‡โ€˜๐ด)))) + (๐ถ ยท ((๐‘‡โ€˜๐ด) ยทih (๐‘‡โ€˜๐ต)))) + ((โˆ—โ€˜(๐ถ ยท ((๐‘‡โ€˜๐ด) ยทih (๐‘‡โ€˜๐ต)))) + ((๐‘‡โ€˜๐ต) ยทih (๐‘‡โ€˜๐ต))))
13257, 131eqtr4i 2759 . . . . . 6 (((๐ถ ยท ((โˆ—โ€˜๐ถ) ยท ((๐‘‡โ€˜๐ด) ยทih (๐‘‡โ€˜๐ด)))) + ((๐‘‡โ€˜๐ต) ยทih (๐‘‡โ€˜๐ต))) + ((๐ถ ยท ((๐‘‡โ€˜๐ด) ยทih (๐‘‡โ€˜๐ต))) + (โˆ—โ€˜(๐ถ ยท ((๐‘‡โ€˜๐ด) ยทih (๐‘‡โ€˜๐ต)))))) = (((๐ถ ยท ((โˆ—โ€˜๐ถ) ยท (๐ด ยทih ๐ด))) + (๐ต ยทih ๐ต)) + ((๐ถ ยท (๐ด ยทih ๐ต)) + (โˆ—โ€˜(๐ถ ยท (๐ด ยทih ๐ต)))))
13350, 132eqtr3i 2758 . . . . 5 (((๐ถ ยท ((โˆ—โ€˜๐ถ) ยท (๐ด ยทih ๐ด))) + (๐ต ยทih ๐ต)) + ((๐ถ ยท ((๐‘‡โ€˜๐ด) ยทih (๐‘‡โ€˜๐ต))) + (โˆ—โ€˜(๐ถ ยท ((๐‘‡โ€˜๐ด) ยทih (๐‘‡โ€˜๐ต)))))) = (((๐ถ ยท ((โˆ—โ€˜๐ถ) ยท (๐ด ยทih ๐ด))) + (๐ต ยทih ๐ต)) + ((๐ถ ยท (๐ด ยทih ๐ต)) + (โˆ—โ€˜(๐ถ ยท (๐ด ยทih ๐ต)))))
13460, 61addcli 11260 . . . . . 6 ((๐ถ ยท ((โˆ—โ€˜๐ถ) ยท (๐ด ยทih ๐ด))) + (๐ต ยทih ๐ต)) โˆˆ โ„‚
13511, 56addcli 11260 . . . . . 6 ((๐ถ ยท ((๐‘‡โ€˜๐ด) ยทih (๐‘‡โ€˜๐ต))) + (โˆ—โ€˜(๐ถ ยท ((๐‘‡โ€˜๐ด) ยทih (๐‘‡โ€˜๐ต))))) โˆˆ โ„‚
13615, 62addcli 11260 . . . . . 6 ((๐ถ ยท (๐ด ยทih ๐ต)) + (โˆ—โ€˜(๐ถ ยท (๐ด ยทih ๐ต)))) โˆˆ โ„‚
137134, 135, 136addcani 11447 . . . . 5 ((((๐ถ ยท ((โˆ—โ€˜๐ถ) ยท (๐ด ยทih ๐ด))) + (๐ต ยทih ๐ต)) + ((๐ถ ยท ((๐‘‡โ€˜๐ด) ยทih (๐‘‡โ€˜๐ต))) + (โˆ—โ€˜(๐ถ ยท ((๐‘‡โ€˜๐ด) ยทih (๐‘‡โ€˜๐ต)))))) = (((๐ถ ยท ((โˆ—โ€˜๐ถ) ยท (๐ด ยทih ๐ด))) + (๐ต ยทih ๐ต)) + ((๐ถ ยท (๐ด ยทih ๐ต)) + (โˆ—โ€˜(๐ถ ยท (๐ด ยทih ๐ต))))) โ†” ((๐ถ ยท ((๐‘‡โ€˜๐ด) ยทih (๐‘‡โ€˜๐ต))) + (โˆ—โ€˜(๐ถ ยท ((๐‘‡โ€˜๐ด) ยทih (๐‘‡โ€˜๐ต))))) = ((๐ถ ยท (๐ด ยทih ๐ต)) + (โˆ—โ€˜(๐ถ ยท (๐ด ยทih ๐ต)))))
138133, 137mpbi 229 . . . 4 ((๐ถ ยท ((๐‘‡โ€˜๐ด) ยทih (๐‘‡โ€˜๐ต))) + (โˆ—โ€˜(๐ถ ยท ((๐‘‡โ€˜๐ด) ยทih (๐‘‡โ€˜๐ต))))) = ((๐ถ ยท (๐ด ยทih ๐ต)) + (โˆ—โ€˜(๐ถ ยท (๐ด ยทih ๐ต))))
139138oveq1i 7436 . . 3 (((๐ถ ยท ((๐‘‡โ€˜๐ด) ยทih (๐‘‡โ€˜๐ต))) + (โˆ—โ€˜(๐ถ ยท ((๐‘‡โ€˜๐ด) ยทih (๐‘‡โ€˜๐ต))))) / 2) = (((๐ถ ยท (๐ด ยทih ๐ต)) + (โˆ—โ€˜(๐ถ ยท (๐ด ยทih ๐ต)))) / 2)
14017, 139eqtr4i 2759 . 2 (โ„œโ€˜(๐ถ ยท (๐ด ยทih ๐ต))) = (((๐ถ ยท ((๐‘‡โ€˜๐ด) ยทih (๐‘‡โ€˜๐ต))) + (โˆ—โ€˜(๐ถ ยท ((๐‘‡โ€˜๐ด) ยทih (๐‘‡โ€˜๐ต))))) / 2)
14113, 140eqtr4i 2759 1 (โ„œโ€˜(๐ถ ยท ((๐‘‡โ€˜๐ด) ยทih (๐‘‡โ€˜๐ต)))) = (โ„œโ€˜(๐ถ ยท (๐ด ยทih ๐ต)))
Colors of variables: wff setvar class
Syntax hints:   = wceq 1533   โˆˆ wcel 2098  โˆ€wral 3058  โ€˜cfv 6553  (class class class)co 7426  โ„‚cc 11146   + caddc 11151   ยท cmul 11153   / cdiv 11911  2c2 12307  โ†‘cexp 14068  โˆ—ccj 15085  โ„œcre 15086   โ„‹chba 30757   +โ„Ž cva 30758   ยทโ„Ž csm 30759   ยทih csp 30760  normโ„Žcno 30761  LinOpclo 30785
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803  ax-5 1905  ax-6 1963  ax-7 2003  ax-8 2100  ax-9 2108  ax-10 2129  ax-11 2146  ax-12 2166  ax-ext 2699  ax-sep 5303  ax-nul 5310  ax-pow 5369  ax-pr 5433  ax-un 7748  ax-cnex 11204  ax-resscn 11205  ax-1cn 11206  ax-icn 11207  ax-addcl 11208  ax-addrcl 11209  ax-mulcl 11210  ax-mulrcl 11211  ax-mulcom 11212  ax-addass 11213  ax-mulass 11214  ax-distr 11215  ax-i2m1 11216  ax-1ne0 11217  ax-1rid 11218  ax-rnegex 11219  ax-rrecex 11220  ax-cnre 11221  ax-pre-lttri 11222  ax-pre-lttrn 11223  ax-pre-ltadd 11224  ax-pre-mulgt0 11225  ax-pre-sup 11226  ax-hilex 30837  ax-hfvadd 30838  ax-hv0cl 30841  ax-hfvmul 30843  ax-hvmul0 30848  ax-hfi 30917  ax-his1 30920  ax-his2 30921  ax-his3 30922  ax-his4 30923
This theorem depends on definitions:  df-bi 206  df-an 395  df-or 846  df-3or 1085  df-3an 1086  df-tru 1536  df-fal 1546  df-ex 1774  df-nf 1778  df-sb 2060  df-mo 2529  df-eu 2558  df-clab 2706  df-cleq 2720  df-clel 2806  df-nfc 2881  df-ne 2938  df-nel 3044  df-ral 3059  df-rex 3068  df-rmo 3374  df-reu 3375  df-rab 3431  df-v 3475  df-sbc 3779  df-csb 3895  df-dif 3952  df-un 3954  df-in 3956  df-ss 3966  df-pss 3968  df-nul 4327  df-if 4533  df-pw 4608  df-sn 4633  df-pr 4635  df-op 4639  df-uni 4913  df-iun 5002  df-br 5153  df-opab 5215  df-mpt 5236  df-tr 5270  df-id 5580  df-eprel 5586  df-po 5594  df-so 5595  df-fr 5637  df-we 5639  df-xp 5688  df-rel 5689  df-cnv 5690  df-co 5691  df-dm 5692  df-rn 5693  df-res 5694  df-ima 5695  df-pred 6310  df-ord 6377  df-on 6378  df-lim 6379  df-suc 6380  df-iota 6505  df-fun 6555  df-fn 6556  df-f 6557  df-f1 6558  df-fo 6559  df-f1o 6560  df-fv 6561  df-riota 7382  df-ov 7429  df-oprab 7430  df-mpo 7431  df-om 7879  df-2nd 8002  df-frecs 8295  df-wrecs 8326  df-recs 8400  df-rdg 8439  df-er 8733  df-map 8855  df-en 8973  df-dom 8974  df-sdom 8975  df-sup 9475  df-pnf 11290  df-mnf 11291  df-xr 11292  df-ltxr 11293  df-le 11294  df-sub 11486  df-neg 11487  df-div 11912  df-nn 12253  df-2 12315  df-3 12316  df-n0 12513  df-z 12599  df-uz 12863  df-rp 13017  df-seq 14009  df-exp 14069  df-cj 15088  df-re 15089  df-im 15090  df-sqrt 15224  df-hnorm 30806  df-lnop 31679
This theorem is referenced by:  lnopunilem2  31849
  Copyright terms: Public domain W3C validator