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

Theorem lnopunilem1 31001
Description: Lemma for lnopunii 31003. (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 30960 . . . . . . 7 ๐‘‡: โ„‹โŸถ โ„‹
54ffvelcdmi 7038 . . . . . 6 (๐ด โˆˆ โ„‹ โ†’ (๐‘‡โ€˜๐ด) โˆˆ โ„‹)
62, 5ax-mp 5 . . . . 5 (๐‘‡โ€˜๐ด) โˆˆ โ„‹
7 lnopunilem.4 . . . . . 6 ๐ต โˆˆ โ„‹
84ffvelcdmi 7038 . . . . . 6 (๐ต โˆˆ โ„‹ โ†’ (๐‘‡โ€˜๐ต) โˆˆ โ„‹)
97, 8ax-mp 5 . . . . 5 (๐‘‡โ€˜๐ต) โˆˆ โ„‹
106, 9hicli 30072 . . . 4 ((๐‘‡โ€˜๐ด) ยทih (๐‘‡โ€˜๐ต)) โˆˆ โ„‚
111, 10mulcli 11170 . . 3 (๐ถ ยท ((๐‘‡โ€˜๐ด) ยทih (๐‘‡โ€˜๐ต))) โˆˆ โ„‚
12 reval 15000 . . 3 ((๐ถ ยท ((๐‘‡โ€˜๐ด) ยทih (๐‘‡โ€˜๐ต))) โˆˆ โ„‚ โ†’ (โ„œโ€˜(๐ถ ยท ((๐‘‡โ€˜๐ด) ยทih (๐‘‡โ€˜๐ต)))) = (((๐ถ ยท ((๐‘‡โ€˜๐ด) ยทih (๐‘‡โ€˜๐ต))) + (โˆ—โ€˜(๐ถ ยท ((๐‘‡โ€˜๐ด) ยทih (๐‘‡โ€˜๐ต))))) / 2))
1311, 12ax-mp 5 . 2 (โ„œโ€˜(๐ถ ยท ((๐‘‡โ€˜๐ด) ยทih (๐‘‡โ€˜๐ต)))) = (((๐ถ ยท ((๐‘‡โ€˜๐ด) ยทih (๐‘‡โ€˜๐ต))) + (โˆ—โ€˜(๐ถ ยท ((๐‘‡โ€˜๐ด) ยทih (๐‘‡โ€˜๐ต))))) / 2)
142, 7hicli 30072 . . . . 5 (๐ด ยทih ๐ต) โˆˆ โ„‚
151, 14mulcli 11170 . . . 4 (๐ถ ยท (๐ด ยทih ๐ต)) โˆˆ โ„‚
16 reval 15000 . . . 4 ((๐ถ ยท (๐ด ยทih ๐ต)) โˆˆ โ„‚ โ†’ (โ„œโ€˜(๐ถ ยท (๐ด ยทih ๐ต))) = (((๐ถ ยท (๐ด ยทih ๐ต)) + (โˆ—โ€˜(๐ถ ยท (๐ด ยทih ๐ต)))) / 2))
1715, 16ax-mp 5 . . 3 (โ„œโ€˜(๐ถ ยท (๐ด ยทih ๐ต))) = (((๐ถ ยท (๐ด ยทih ๐ต)) + (โˆ—โ€˜(๐ถ ยท (๐ด ยทih ๐ต)))) / 2)
18 lnopunilem.2 . . . . . . . . . . . . 13 โˆ€๐‘ฅ โˆˆ โ„‹ (normโ„Žโ€˜(๐‘‡โ€˜๐‘ฅ)) = (normโ„Žโ€˜๐‘ฅ)
19 2fveq3 6851 . . . . . . . . . . . . . . 15 (๐‘ฅ = ๐‘ฆ โ†’ (normโ„Žโ€˜(๐‘‡โ€˜๐‘ฅ)) = (normโ„Žโ€˜(๐‘‡โ€˜๐‘ฆ)))
20 fveq2 6846 . . . . . . . . . . . . . . 15 (๐‘ฅ = ๐‘ฆ โ†’ (normโ„Žโ€˜๐‘ฅ) = (normโ„Žโ€˜๐‘ฆ))
2119, 20eqeq12d 2749 . . . . . . . . . . . . . 14 (๐‘ฅ = ๐‘ฆ โ†’ ((normโ„Žโ€˜(๐‘‡โ€˜๐‘ฅ)) = (normโ„Žโ€˜๐‘ฅ) โ†” (normโ„Žโ€˜(๐‘‡โ€˜๐‘ฆ)) = (normโ„Žโ€˜๐‘ฆ)))
2221cbvralvw 3224 . . . . . . . . . . . . 13 (โˆ€๐‘ฅ โˆˆ โ„‹ (normโ„Žโ€˜(๐‘‡โ€˜๐‘ฅ)) = (normโ„Žโ€˜๐‘ฅ) โ†” โˆ€๐‘ฆ โˆˆ โ„‹ (normโ„Žโ€˜(๐‘‡โ€˜๐‘ฆ)) = (normโ„Žโ€˜๐‘ฆ))
2318, 22mpbi 229 . . . . . . . . . . . 12 โˆ€๐‘ฆ โˆˆ โ„‹ (normโ„Žโ€˜(๐‘‡โ€˜๐‘ฆ)) = (normโ„Žโ€˜๐‘ฆ)
24 oveq1 7368 . . . . . . . . . . . . . 14 ((normโ„Žโ€˜(๐‘‡โ€˜๐‘ฆ)) = (normโ„Žโ€˜๐‘ฆ) โ†’ ((normโ„Žโ€˜(๐‘‡โ€˜๐‘ฆ))โ†‘2) = ((normโ„Žโ€˜๐‘ฆ)โ†‘2))
254ffvelcdmi 7038 . . . . . . . . . . . . . . . 16 (๐‘ฆ โˆˆ โ„‹ โ†’ (๐‘‡โ€˜๐‘ฆ) โˆˆ โ„‹)
26 normsq 30125 . . . . . . . . . . . . . . . 16 ((๐‘‡โ€˜๐‘ฆ) โˆˆ โ„‹ โ†’ ((normโ„Žโ€˜(๐‘‡โ€˜๐‘ฆ))โ†‘2) = ((๐‘‡โ€˜๐‘ฆ) ยทih (๐‘‡โ€˜๐‘ฆ)))
2725, 26syl 17 . . . . . . . . . . . . . . 15 (๐‘ฆ โˆˆ โ„‹ โ†’ ((normโ„Žโ€˜(๐‘‡โ€˜๐‘ฆ))โ†‘2) = ((๐‘‡โ€˜๐‘ฆ) ยทih (๐‘‡โ€˜๐‘ฆ)))
28 normsq 30125 . . . . . . . . . . . . . . 15 (๐‘ฆ โˆˆ โ„‹ โ†’ ((normโ„Žโ€˜๐‘ฆ)โ†‘2) = (๐‘ฆ ยทih ๐‘ฆ))
2927, 28eqeq12d 2749 . . . . . . . . . . . . . 14 (๐‘ฆ โˆˆ โ„‹ โ†’ (((normโ„Žโ€˜(๐‘‡โ€˜๐‘ฆ))โ†‘2) = ((normโ„Žโ€˜๐‘ฆ)โ†‘2) โ†” ((๐‘‡โ€˜๐‘ฆ) ยทih (๐‘‡โ€˜๐‘ฆ)) = (๐‘ฆ ยทih ๐‘ฆ)))
3024, 29imbitrid 243 . . . . . . . . . . . . 13 (๐‘ฆ โˆˆ โ„‹ โ†’ ((normโ„Žโ€˜(๐‘‡โ€˜๐‘ฆ)) = (normโ„Žโ€˜๐‘ฆ) โ†’ ((๐‘‡โ€˜๐‘ฆ) ยทih (๐‘‡โ€˜๐‘ฆ)) = (๐‘ฆ ยทih ๐‘ฆ)))
3130ralimia 3080 . . . . . . . . . . . 12 (โˆ€๐‘ฆ โˆˆ โ„‹ (normโ„Žโ€˜(๐‘‡โ€˜๐‘ฆ)) = (normโ„Žโ€˜๐‘ฆ) โ†’ โˆ€๐‘ฆ โˆˆ โ„‹ ((๐‘‡โ€˜๐‘ฆ) ยทih (๐‘‡โ€˜๐‘ฆ)) = (๐‘ฆ ยทih ๐‘ฆ))
3223, 31ax-mp 5 . . . . . . . . . . 11 โˆ€๐‘ฆ โˆˆ โ„‹ ((๐‘‡โ€˜๐‘ฆ) ยทih (๐‘‡โ€˜๐‘ฆ)) = (๐‘ฆ ยทih ๐‘ฆ)
33 fveq2 6846 . . . . . . . . . . . . . 14 (๐‘ฆ = ๐ด โ†’ (๐‘‡โ€˜๐‘ฆ) = (๐‘‡โ€˜๐ด))
3433, 33oveq12d 7379 . . . . . . . . . . . . 13 (๐‘ฆ = ๐ด โ†’ ((๐‘‡โ€˜๐‘ฆ) ยทih (๐‘‡โ€˜๐‘ฆ)) = ((๐‘‡โ€˜๐ด) ยทih (๐‘‡โ€˜๐ด)))
35 id 22 . . . . . . . . . . . . . 14 (๐‘ฆ = ๐ด โ†’ ๐‘ฆ = ๐ด)
3635, 35oveq12d 7379 . . . . . . . . . . . . 13 (๐‘ฆ = ๐ด โ†’ (๐‘ฆ ยทih ๐‘ฆ) = (๐ด ยทih ๐ด))
3734, 36eqeq12d 2749 . . . . . . . . . . . 12 (๐‘ฆ = ๐ด โ†’ (((๐‘‡โ€˜๐‘ฆ) ยทih (๐‘‡โ€˜๐‘ฆ)) = (๐‘ฆ ยทih ๐‘ฆ) โ†” ((๐‘‡โ€˜๐ด) ยทih (๐‘‡โ€˜๐ด)) = (๐ด ยทih ๐ด)))
3837rspcv 3579 . . . . . . . . . . 11 (๐ด โˆˆ โ„‹ โ†’ (โˆ€๐‘ฆ โˆˆ โ„‹ ((๐‘‡โ€˜๐‘ฆ) ยทih (๐‘‡โ€˜๐‘ฆ)) = (๐‘ฆ ยทih ๐‘ฆ) โ†’ ((๐‘‡โ€˜๐ด) ยทih (๐‘‡โ€˜๐ด)) = (๐ด ยทih ๐ด)))
392, 32, 38mp2 9 . . . . . . . . . 10 ((๐‘‡โ€˜๐ด) ยทih (๐‘‡โ€˜๐ด)) = (๐ด ยทih ๐ด)
4039oveq2i 7372 . . . . . . . . 9 ((โˆ—โ€˜๐ถ) ยท ((๐‘‡โ€˜๐ด) ยทih (๐‘‡โ€˜๐ด))) = ((โˆ—โ€˜๐ถ) ยท (๐ด ยทih ๐ด))
4140oveq2i 7372 . . . . . . . 8 (๐ถ ยท ((โˆ—โ€˜๐ถ) ยท ((๐‘‡โ€˜๐ด) ยทih (๐‘‡โ€˜๐ด)))) = (๐ถ ยท ((โˆ—โ€˜๐ถ) ยท (๐ด ยทih ๐ด)))
42 fveq2 6846 . . . . . . . . . . . 12 (๐‘ฆ = ๐ต โ†’ (๐‘‡โ€˜๐‘ฆ) = (๐‘‡โ€˜๐ต))
4342, 42oveq12d 7379 . . . . . . . . . . 11 (๐‘ฆ = ๐ต โ†’ ((๐‘‡โ€˜๐‘ฆ) ยทih (๐‘‡โ€˜๐‘ฆ)) = ((๐‘‡โ€˜๐ต) ยทih (๐‘‡โ€˜๐ต)))
44 id 22 . . . . . . . . . . . 12 (๐‘ฆ = ๐ต โ†’ ๐‘ฆ = ๐ต)
4544, 44oveq12d 7379 . . . . . . . . . . 11 (๐‘ฆ = ๐ต โ†’ (๐‘ฆ ยทih ๐‘ฆ) = (๐ต ยทih ๐ต))
4643, 45eqeq12d 2749 . . . . . . . . . 10 (๐‘ฆ = ๐ต โ†’ (((๐‘‡โ€˜๐‘ฆ) ยทih (๐‘‡โ€˜๐‘ฆ)) = (๐‘ฆ ยทih ๐‘ฆ) โ†” ((๐‘‡โ€˜๐ต) ยทih (๐‘‡โ€˜๐ต)) = (๐ต ยทih ๐ต)))
4746rspcv 3579 . . . . . . . . 9 (๐ต โˆˆ โ„‹ โ†’ (โˆ€๐‘ฆ โˆˆ โ„‹ ((๐‘‡โ€˜๐‘ฆ) ยทih (๐‘‡โ€˜๐‘ฆ)) = (๐‘ฆ ยทih ๐‘ฆ) โ†’ ((๐‘‡โ€˜๐ต) ยทih (๐‘‡โ€˜๐ต)) = (๐ต ยทih ๐ต)))
487, 32, 47mp2 9 . . . . . . . 8 ((๐‘‡โ€˜๐ต) ยทih (๐‘‡โ€˜๐ต)) = (๐ต ยทih ๐ต)
4941, 48oveq12i 7373 . . . . . . 7 ((๐ถ ยท ((โˆ—โ€˜๐ถ) ยท ((๐‘‡โ€˜๐ด) ยทih (๐‘‡โ€˜๐ด)))) + ((๐‘‡โ€˜๐ต) ยทih (๐‘‡โ€˜๐ต))) = ((๐ถ ยท ((โˆ—โ€˜๐ถ) ยท (๐ด ยทih ๐ด))) + (๐ต ยทih ๐ต))
5049oveq1i 7371 . . . . . 6 (((๐ถ ยท ((โˆ—โ€˜๐ถ) ยท ((๐‘‡โ€˜๐ด) ยทih (๐‘‡โ€˜๐ด)))) + ((๐‘‡โ€˜๐ต) ยทih (๐‘‡โ€˜๐ต))) + ((๐ถ ยท ((๐‘‡โ€˜๐ด) ยทih (๐‘‡โ€˜๐ต))) + (โˆ—โ€˜(๐ถ ยท ((๐‘‡โ€˜๐ด) ยทih (๐‘‡โ€˜๐ต)))))) = (((๐ถ ยท ((โˆ—โ€˜๐ถ) ยท (๐ด ยทih ๐ด))) + (๐ต ยทih ๐ต)) + ((๐ถ ยท ((๐‘‡โ€˜๐ด) ยทih (๐‘‡โ€˜๐ต))) + (โˆ—โ€˜(๐ถ ยท ((๐‘‡โ€˜๐ด) ยทih (๐‘‡โ€˜๐ต))))))
511cjcli 15063 . . . . . . . . . 10 (โˆ—โ€˜๐ถ) โˆˆ โ„‚
526, 6hicli 30072 . . . . . . . . . 10 ((๐‘‡โ€˜๐ด) ยทih (๐‘‡โ€˜๐ด)) โˆˆ โ„‚
5351, 52mulcli 11170 . . . . . . . . 9 ((โˆ—โ€˜๐ถ) ยท ((๐‘‡โ€˜๐ด) ยทih (๐‘‡โ€˜๐ด))) โˆˆ โ„‚
541, 53mulcli 11170 . . . . . . . 8 (๐ถ ยท ((โˆ—โ€˜๐ถ) ยท ((๐‘‡โ€˜๐ด) ยทih (๐‘‡โ€˜๐ด)))) โˆˆ โ„‚
559, 9hicli 30072 . . . . . . . 8 ((๐‘‡โ€˜๐ต) ยทih (๐‘‡โ€˜๐ต)) โˆˆ โ„‚
5611cjcli 15063 . . . . . . . 8 (โˆ—โ€˜(๐ถ ยท ((๐‘‡โ€˜๐ด) ยทih (๐‘‡โ€˜๐ต)))) โˆˆ โ„‚
5754, 55, 11, 56add42i 11388 . . . . . . 7 (((๐ถ ยท ((โˆ—โ€˜๐ถ) ยท ((๐‘‡โ€˜๐ด) ยทih (๐‘‡โ€˜๐ด)))) + ((๐‘‡โ€˜๐ต) ยทih (๐‘‡โ€˜๐ต))) + ((๐ถ ยท ((๐‘‡โ€˜๐ด) ยทih (๐‘‡โ€˜๐ต))) + (โˆ—โ€˜(๐ถ ยท ((๐‘‡โ€˜๐ด) ยทih (๐‘‡โ€˜๐ต)))))) = (((๐ถ ยท ((โˆ—โ€˜๐ถ) ยท ((๐‘‡โ€˜๐ด) ยทih (๐‘‡โ€˜๐ด)))) + (๐ถ ยท ((๐‘‡โ€˜๐ด) ยทih (๐‘‡โ€˜๐ต)))) + ((โˆ—โ€˜(๐ถ ยท ((๐‘‡โ€˜๐ด) ยทih (๐‘‡โ€˜๐ต)))) + ((๐‘‡โ€˜๐ต) ยทih (๐‘‡โ€˜๐ต))))
582, 2hicli 30072 . . . . . . . . . . 11 (๐ด ยทih ๐ด) โˆˆ โ„‚
5951, 58mulcli 11170 . . . . . . . . . 10 ((โˆ—โ€˜๐ถ) ยท (๐ด ยทih ๐ด)) โˆˆ โ„‚
601, 59mulcli 11170 . . . . . . . . 9 (๐ถ ยท ((โˆ—โ€˜๐ถ) ยท (๐ด ยทih ๐ด))) โˆˆ โ„‚
617, 7hicli 30072 . . . . . . . . 9 (๐ต ยทih ๐ต) โˆˆ โ„‚
6215cjcli 15063 . . . . . . . . 9 (โˆ—โ€˜(๐ถ ยท (๐ด ยทih ๐ต))) โˆˆ โ„‚
6360, 61, 15, 62add42i 11388 . . . . . . . 8 (((๐ถ ยท ((โˆ—โ€˜๐ถ) ยท (๐ด ยทih ๐ด))) + (๐ต ยทih ๐ต)) + ((๐ถ ยท (๐ด ยทih ๐ต)) + (โˆ—โ€˜(๐ถ ยท (๐ด ยทih ๐ต))))) = (((๐ถ ยท ((โˆ—โ€˜๐ถ) ยท (๐ด ยทih ๐ด))) + (๐ถ ยท (๐ด ยทih ๐ต))) + ((โˆ—โ€˜(๐ถ ยท (๐ด ยทih ๐ต))) + (๐ต ยทih ๐ต)))
641, 2hvmulcli 30005 . . . . . . . . . . . 12 (๐ถ ยทโ„Ž ๐ด) โˆˆ โ„‹
6564, 7hvaddcli 30009 . . . . . . . . . . 11 ((๐ถ ยทโ„Ž ๐ด) +โ„Ž ๐ต) โˆˆ โ„‹
66 fveq2 6846 . . . . . . . . . . . . . 14 (๐‘ฆ = ((๐ถ ยทโ„Ž ๐ด) +โ„Ž ๐ต) โ†’ (๐‘‡โ€˜๐‘ฆ) = (๐‘‡โ€˜((๐ถ ยทโ„Ž ๐ด) +โ„Ž ๐ต)))
6766, 66oveq12d 7379 . . . . . . . . . . . . 13 (๐‘ฆ = ((๐ถ ยทโ„Ž ๐ด) +โ„Ž ๐ต) โ†’ ((๐‘‡โ€˜๐‘ฆ) ยทih (๐‘‡โ€˜๐‘ฆ)) = ((๐‘‡โ€˜((๐ถ ยทโ„Ž ๐ด) +โ„Ž ๐ต)) ยทih (๐‘‡โ€˜((๐ถ ยทโ„Ž ๐ด) +โ„Ž ๐ต))))
68 id 22 . . . . . . . . . . . . . 14 (๐‘ฆ = ((๐ถ ยทโ„Ž ๐ด) +โ„Ž ๐ต) โ†’ ๐‘ฆ = ((๐ถ ยทโ„Ž ๐ด) +โ„Ž ๐ต))
6968, 68oveq12d 7379 . . . . . . . . . . . . 13 (๐‘ฆ = ((๐ถ ยทโ„Ž ๐ด) +โ„Ž ๐ต) โ†’ (๐‘ฆ ยทih ๐‘ฆ) = (((๐ถ ยทโ„Ž ๐ด) +โ„Ž ๐ต) ยทih ((๐ถ ยทโ„Ž ๐ด) +โ„Ž ๐ต)))
7067, 69eqeq12d 2749 . . . . . . . . . . . 12 (๐‘ฆ = ((๐ถ ยทโ„Ž ๐ด) +โ„Ž ๐ต) โ†’ (((๐‘‡โ€˜๐‘ฆ) ยทih (๐‘‡โ€˜๐‘ฆ)) = (๐‘ฆ ยทih ๐‘ฆ) โ†” ((๐‘‡โ€˜((๐ถ ยทโ„Ž ๐ด) +โ„Ž ๐ต)) ยทih (๐‘‡โ€˜((๐ถ ยทโ„Ž ๐ด) +โ„Ž ๐ต))) = (((๐ถ ยทโ„Ž ๐ด) +โ„Ž ๐ต) ยทih ((๐ถ ยทโ„Ž ๐ด) +โ„Ž ๐ต))))
7170rspcv 3579 . . . . . . . . . . 11 (((๐ถ ยทโ„Ž ๐ด) +โ„Ž ๐ต) โˆˆ โ„‹ โ†’ (โˆ€๐‘ฆ โˆˆ โ„‹ ((๐‘‡โ€˜๐‘ฆ) ยทih (๐‘‡โ€˜๐‘ฆ)) = (๐‘ฆ ยทih ๐‘ฆ) โ†’ ((๐‘‡โ€˜((๐ถ ยทโ„Ž ๐ด) +โ„Ž ๐ต)) ยทih (๐‘‡โ€˜((๐ถ ยทโ„Ž ๐ด) +โ„Ž ๐ต))) = (((๐ถ ยทโ„Ž ๐ด) +โ„Ž ๐ต) ยทih ((๐ถ ยทโ„Ž ๐ด) +โ„Ž ๐ต))))
7265, 32, 71mp2 9 . . . . . . . . . 10 ((๐‘‡โ€˜((๐ถ ยทโ„Ž ๐ด) +โ„Ž ๐ต)) ยทih (๐‘‡โ€˜((๐ถ ยทโ„Ž ๐ด) +โ„Ž ๐ต))) = (((๐ถ ยทโ„Ž ๐ด) +โ„Ž ๐ต) ยทih ((๐ถ ยทโ„Ž ๐ด) +โ„Ž ๐ต))
73 ax-his2 30074 . . . . . . . . . . 11 (((๐ถ ยทโ„Ž ๐ด) โˆˆ โ„‹ โˆง ๐ต โˆˆ โ„‹ โˆง ((๐ถ ยทโ„Ž ๐ด) +โ„Ž ๐ต) โˆˆ โ„‹) โ†’ (((๐ถ ยทโ„Ž ๐ด) +โ„Ž ๐ต) ยทih ((๐ถ ยทโ„Ž ๐ด) +โ„Ž ๐ต)) = (((๐ถ ยทโ„Ž ๐ด) ยทih ((๐ถ ยทโ„Ž ๐ด) +โ„Ž ๐ต)) + (๐ต ยทih ((๐ถ ยทโ„Ž ๐ด) +โ„Ž ๐ต))))
7464, 7, 65, 73mp3an 1462 . . . . . . . . . 10 (((๐ถ ยทโ„Ž ๐ด) +โ„Ž ๐ต) ยทih ((๐ถ ยทโ„Ž ๐ด) +โ„Ž ๐ต)) = (((๐ถ ยทโ„Ž ๐ด) ยทih ((๐ถ ยทโ„Ž ๐ด) +โ„Ž ๐ต)) + (๐ต ยทih ((๐ถ ยทโ„Ž ๐ด) +โ„Ž ๐ต)))
75 ax-his3 30075 . . . . . . . . . . . . 13 ((๐ถ โˆˆ โ„‚ โˆง ๐ด โˆˆ โ„‹ โˆง ((๐ถ ยทโ„Ž ๐ด) +โ„Ž ๐ต) โˆˆ โ„‹) โ†’ ((๐ถ ยทโ„Ž ๐ด) ยทih ((๐ถ ยทโ„Ž ๐ด) +โ„Ž ๐ต)) = (๐ถ ยท (๐ด ยทih ((๐ถ ยทโ„Ž ๐ด) +โ„Ž ๐ต))))
761, 2, 65, 75mp3an 1462 . . . . . . . . . . . 12 ((๐ถ ยทโ„Ž ๐ด) ยทih ((๐ถ ยทโ„Ž ๐ด) +โ„Ž ๐ต)) = (๐ถ ยท (๐ด ยทih ((๐ถ ยทโ„Ž ๐ด) +โ„Ž ๐ต)))
77 his7 30081 . . . . . . . . . . . . . . 15 ((๐ด โˆˆ โ„‹ โˆง (๐ถ ยทโ„Ž ๐ด) โˆˆ โ„‹ โˆง ๐ต โˆˆ โ„‹) โ†’ (๐ด ยทih ((๐ถ ยทโ„Ž ๐ด) +โ„Ž ๐ต)) = ((๐ด ยทih (๐ถ ยทโ„Ž ๐ด)) + (๐ด ยทih ๐ต)))
782, 64, 7, 77mp3an 1462 . . . . . . . . . . . . . 14 (๐ด ยทih ((๐ถ ยทโ„Ž ๐ด) +โ„Ž ๐ต)) = ((๐ด ยทih (๐ถ ยทโ„Ž ๐ด)) + (๐ด ยทih ๐ต))
79 his5 30077 . . . . . . . . . . . . . . . 16 ((๐ถ โˆˆ โ„‚ โˆง ๐ด โˆˆ โ„‹ โˆง ๐ด โˆˆ โ„‹) โ†’ (๐ด ยทih (๐ถ ยทโ„Ž ๐ด)) = ((โˆ—โ€˜๐ถ) ยท (๐ด ยทih ๐ด)))
801, 2, 2, 79mp3an 1462 . . . . . . . . . . . . . . 15 (๐ด ยทih (๐ถ ยทโ„Ž ๐ด)) = ((โˆ—โ€˜๐ถ) ยท (๐ด ยทih ๐ด))
8180oveq1i 7371 . . . . . . . . . . . . . 14 ((๐ด ยทih (๐ถ ยทโ„Ž ๐ด)) + (๐ด ยทih ๐ต)) = (((โˆ—โ€˜๐ถ) ยท (๐ด ยทih ๐ด)) + (๐ด ยทih ๐ต))
8278, 81eqtri 2761 . . . . . . . . . . . . 13 (๐ด ยทih ((๐ถ ยทโ„Ž ๐ด) +โ„Ž ๐ต)) = (((โˆ—โ€˜๐ถ) ยท (๐ด ยทih ๐ด)) + (๐ด ยทih ๐ต))
8382oveq2i 7372 . . . . . . . . . . . 12 (๐ถ ยท (๐ด ยทih ((๐ถ ยทโ„Ž ๐ด) +โ„Ž ๐ต))) = (๐ถ ยท (((โˆ—โ€˜๐ถ) ยท (๐ด ยทih ๐ด)) + (๐ด ยทih ๐ต)))
841, 59, 14adddii 11175 . . . . . . . . . . . 12 (๐ถ ยท (((โˆ—โ€˜๐ถ) ยท (๐ด ยทih ๐ด)) + (๐ด ยทih ๐ต))) = ((๐ถ ยท ((โˆ—โ€˜๐ถ) ยท (๐ด ยทih ๐ด))) + (๐ถ ยท (๐ด ยทih ๐ต)))
8576, 83, 843eqtri 2765 . . . . . . . . . . 11 ((๐ถ ยทโ„Ž ๐ด) ยทih ((๐ถ ยทโ„Ž ๐ด) +โ„Ž ๐ต)) = ((๐ถ ยท ((โˆ—โ€˜๐ถ) ยท (๐ด ยทih ๐ด))) + (๐ถ ยท (๐ด ยทih ๐ต)))
86 his7 30081 . . . . . . . . . . . . 13 ((๐ต โˆˆ โ„‹ โˆง (๐ถ ยทโ„Ž ๐ด) โˆˆ โ„‹ โˆง ๐ต โˆˆ โ„‹) โ†’ (๐ต ยทih ((๐ถ ยทโ„Ž ๐ด) +โ„Ž ๐ต)) = ((๐ต ยทih (๐ถ ยทโ„Ž ๐ด)) + (๐ต ยทih ๐ต)))
877, 64, 7, 86mp3an 1462 . . . . . . . . . . . 12 (๐ต ยทih ((๐ถ ยทโ„Ž ๐ด) +โ„Ž ๐ต)) = ((๐ต ยทih (๐ถ ยทโ„Ž ๐ด)) + (๐ต ยทih ๐ต))
88 his5 30077 . . . . . . . . . . . . . . 15 ((๐ถ โˆˆ โ„‚ โˆง ๐ต โˆˆ โ„‹ โˆง ๐ด โˆˆ โ„‹) โ†’ (๐ต ยทih (๐ถ ยทโ„Ž ๐ด)) = ((โˆ—โ€˜๐ถ) ยท (๐ต ยทih ๐ด)))
891, 7, 2, 88mp3an 1462 . . . . . . . . . . . . . 14 (๐ต ยทih (๐ถ ยทโ„Ž ๐ด)) = ((โˆ—โ€˜๐ถ) ยท (๐ต ยทih ๐ด))
901, 14cjmuli 15083 . . . . . . . . . . . . . . 15 (โˆ—โ€˜(๐ถ ยท (๐ด ยทih ๐ต))) = ((โˆ—โ€˜๐ถ) ยท (โˆ—โ€˜(๐ด ยทih ๐ต)))
917, 2his1i 30091 . . . . . . . . . . . . . . . 16 (๐ต ยทih ๐ด) = (โˆ—โ€˜(๐ด ยทih ๐ต))
9291oveq2i 7372 . . . . . . . . . . . . . . 15 ((โˆ—โ€˜๐ถ) ยท (๐ต ยทih ๐ด)) = ((โˆ—โ€˜๐ถ) ยท (โˆ—โ€˜(๐ด ยทih ๐ต)))
9390, 92eqtr4i 2764 . . . . . . . . . . . . . 14 (โˆ—โ€˜(๐ถ ยท (๐ด ยทih ๐ต))) = ((โˆ—โ€˜๐ถ) ยท (๐ต ยทih ๐ด))
9489, 93eqtr4i 2764 . . . . . . . . . . . . 13 (๐ต ยทih (๐ถ ยทโ„Ž ๐ด)) = (โˆ—โ€˜(๐ถ ยท (๐ด ยทih ๐ต)))
9594oveq1i 7371 . . . . . . . . . . . 12 ((๐ต ยทih (๐ถ ยทโ„Ž ๐ด)) + (๐ต ยทih ๐ต)) = ((โˆ—โ€˜(๐ถ ยท (๐ด ยทih ๐ต))) + (๐ต ยทih ๐ต))
9687, 95eqtri 2761 . . . . . . . . . . 11 (๐ต ยทih ((๐ถ ยทโ„Ž ๐ด) +โ„Ž ๐ต)) = ((โˆ—โ€˜(๐ถ ยท (๐ด ยทih ๐ต))) + (๐ต ยทih ๐ต))
9785, 96oveq12i 7373 . . . . . . . . . 10 (((๐ถ ยทโ„Ž ๐ด) ยทih ((๐ถ ยทโ„Ž ๐ด) +โ„Ž ๐ต)) + (๐ต ยทih ((๐ถ ยทโ„Ž ๐ด) +โ„Ž ๐ต))) = (((๐ถ ยท ((โˆ—โ€˜๐ถ) ยท (๐ด ยทih ๐ด))) + (๐ถ ยท (๐ด ยทih ๐ต))) + ((โˆ—โ€˜(๐ถ ยท (๐ด ยทih ๐ต))) + (๐ต ยทih ๐ต)))
9872, 74, 973eqtrri 2766 . . . . . . . . 9 (((๐ถ ยท ((โˆ—โ€˜๐ถ) ยท (๐ด ยทih ๐ด))) + (๐ถ ยท (๐ด ยทih ๐ต))) + ((โˆ—โ€˜(๐ถ ยท (๐ด ยทih ๐ต))) + (๐ต ยทih ๐ต))) = ((๐‘‡โ€˜((๐ถ ยทโ„Ž ๐ด) +โ„Ž ๐ต)) ยทih (๐‘‡โ€˜((๐ถ ยทโ„Ž ๐ด) +โ„Ž ๐ต)))
993lnopli 30959 . . . . . . . . . . . 12 ((๐ถ โˆˆ โ„‚ โˆง ๐ด โˆˆ โ„‹ โˆง ๐ต โˆˆ โ„‹) โ†’ (๐‘‡โ€˜((๐ถ ยทโ„Ž ๐ด) +โ„Ž ๐ต)) = ((๐ถ ยทโ„Ž (๐‘‡โ€˜๐ด)) +โ„Ž (๐‘‡โ€˜๐ต)))
1001, 2, 7, 99mp3an 1462 . . . . . . . . . . 11 (๐‘‡โ€˜((๐ถ ยทโ„Ž ๐ด) +โ„Ž ๐ต)) = ((๐ถ ยทโ„Ž (๐‘‡โ€˜๐ด)) +โ„Ž (๐‘‡โ€˜๐ต))
101100, 100oveq12i 7373 . . . . . . . . . 10 ((๐‘‡โ€˜((๐ถ ยทโ„Ž ๐ด) +โ„Ž ๐ต)) ยทih (๐‘‡โ€˜((๐ถ ยทโ„Ž ๐ด) +โ„Ž ๐ต))) = (((๐ถ ยทโ„Ž (๐‘‡โ€˜๐ด)) +โ„Ž (๐‘‡โ€˜๐ต)) ยทih ((๐ถ ยทโ„Ž (๐‘‡โ€˜๐ด)) +โ„Ž (๐‘‡โ€˜๐ต)))
1021, 6hvmulcli 30005 . . . . . . . . . . 11 (๐ถ ยทโ„Ž (๐‘‡โ€˜๐ด)) โˆˆ โ„‹
103102, 9hvaddcli 30009 . . . . . . . . . . 11 ((๐ถ ยทโ„Ž (๐‘‡โ€˜๐ด)) +โ„Ž (๐‘‡โ€˜๐ต)) โˆˆ โ„‹
104 ax-his2 30074 . . . . . . . . . . 11 (((๐ถ ยทโ„Ž (๐‘‡โ€˜๐ด)) โˆˆ โ„‹ โˆง (๐‘‡โ€˜๐ต) โˆˆ โ„‹ โˆง ((๐ถ ยทโ„Ž (๐‘‡โ€˜๐ด)) +โ„Ž (๐‘‡โ€˜๐ต)) โˆˆ โ„‹) โ†’ (((๐ถ ยทโ„Ž (๐‘‡โ€˜๐ด)) +โ„Ž (๐‘‡โ€˜๐ต)) ยทih ((๐ถ ยทโ„Ž (๐‘‡โ€˜๐ด)) +โ„Ž (๐‘‡โ€˜๐ต))) = (((๐ถ ยทโ„Ž (๐‘‡โ€˜๐ด)) ยทih ((๐ถ ยทโ„Ž (๐‘‡โ€˜๐ด)) +โ„Ž (๐‘‡โ€˜๐ต))) + ((๐‘‡โ€˜๐ต) ยทih ((๐ถ ยทโ„Ž (๐‘‡โ€˜๐ด)) +โ„Ž (๐‘‡โ€˜๐ต)))))
105102, 9, 103, 104mp3an 1462 . . . . . . . . . 10 (((๐ถ ยทโ„Ž (๐‘‡โ€˜๐ด)) +โ„Ž (๐‘‡โ€˜๐ต)) ยทih ((๐ถ ยทโ„Ž (๐‘‡โ€˜๐ด)) +โ„Ž (๐‘‡โ€˜๐ต))) = (((๐ถ ยทโ„Ž (๐‘‡โ€˜๐ด)) ยทih ((๐ถ ยทโ„Ž (๐‘‡โ€˜๐ด)) +โ„Ž (๐‘‡โ€˜๐ต))) + ((๐‘‡โ€˜๐ต) ยทih ((๐ถ ยทโ„Ž (๐‘‡โ€˜๐ด)) +โ„Ž (๐‘‡โ€˜๐ต))))
106101, 105eqtri 2761 . . . . . . . . 9 ((๐‘‡โ€˜((๐ถ ยทโ„Ž ๐ด) +โ„Ž ๐ต)) ยทih (๐‘‡โ€˜((๐ถ ยทโ„Ž ๐ด) +โ„Ž ๐ต))) = (((๐ถ ยทโ„Ž (๐‘‡โ€˜๐ด)) ยทih ((๐ถ ยทโ„Ž (๐‘‡โ€˜๐ด)) +โ„Ž (๐‘‡โ€˜๐ต))) + ((๐‘‡โ€˜๐ต) ยทih ((๐ถ ยทโ„Ž (๐‘‡โ€˜๐ด)) +โ„Ž (๐‘‡โ€˜๐ต))))
107 ax-his3 30075 . . . . . . . . . . . 12 ((๐ถ โˆˆ โ„‚ โˆง (๐‘‡โ€˜๐ด) โˆˆ โ„‹ โˆง ((๐ถ ยทโ„Ž (๐‘‡โ€˜๐ด)) +โ„Ž (๐‘‡โ€˜๐ต)) โˆˆ โ„‹) โ†’ ((๐ถ ยทโ„Ž (๐‘‡โ€˜๐ด)) ยทih ((๐ถ ยทโ„Ž (๐‘‡โ€˜๐ด)) +โ„Ž (๐‘‡โ€˜๐ต))) = (๐ถ ยท ((๐‘‡โ€˜๐ด) ยทih ((๐ถ ยทโ„Ž (๐‘‡โ€˜๐ด)) +โ„Ž (๐‘‡โ€˜๐ต)))))
1081, 6, 103, 107mp3an 1462 . . . . . . . . . . 11 ((๐ถ ยทโ„Ž (๐‘‡โ€˜๐ด)) ยทih ((๐ถ ยทโ„Ž (๐‘‡โ€˜๐ด)) +โ„Ž (๐‘‡โ€˜๐ต))) = (๐ถ ยท ((๐‘‡โ€˜๐ด) ยทih ((๐ถ ยทโ„Ž (๐‘‡โ€˜๐ด)) +โ„Ž (๐‘‡โ€˜๐ต))))
109 his7 30081 . . . . . . . . . . . . . 14 (((๐‘‡โ€˜๐ด) โˆˆ โ„‹ โˆง (๐ถ ยทโ„Ž (๐‘‡โ€˜๐ด)) โˆˆ โ„‹ โˆง (๐‘‡โ€˜๐ต) โˆˆ โ„‹) โ†’ ((๐‘‡โ€˜๐ด) ยทih ((๐ถ ยทโ„Ž (๐‘‡โ€˜๐ด)) +โ„Ž (๐‘‡โ€˜๐ต))) = (((๐‘‡โ€˜๐ด) ยทih (๐ถ ยทโ„Ž (๐‘‡โ€˜๐ด))) + ((๐‘‡โ€˜๐ด) ยทih (๐‘‡โ€˜๐ต))))
1106, 102, 9, 109mp3an 1462 . . . . . . . . . . . . 13 ((๐‘‡โ€˜๐ด) ยทih ((๐ถ ยทโ„Ž (๐‘‡โ€˜๐ด)) +โ„Ž (๐‘‡โ€˜๐ต))) = (((๐‘‡โ€˜๐ด) ยทih (๐ถ ยทโ„Ž (๐‘‡โ€˜๐ด))) + ((๐‘‡โ€˜๐ด) ยทih (๐‘‡โ€˜๐ต)))
111 his5 30077 . . . . . . . . . . . . . . 15 ((๐ถ โˆˆ โ„‚ โˆง (๐‘‡โ€˜๐ด) โˆˆ โ„‹ โˆง (๐‘‡โ€˜๐ด) โˆˆ โ„‹) โ†’ ((๐‘‡โ€˜๐ด) ยทih (๐ถ ยทโ„Ž (๐‘‡โ€˜๐ด))) = ((โˆ—โ€˜๐ถ) ยท ((๐‘‡โ€˜๐ด) ยทih (๐‘‡โ€˜๐ด))))
1121, 6, 6, 111mp3an 1462 . . . . . . . . . . . . . 14 ((๐‘‡โ€˜๐ด) ยทih (๐ถ ยทโ„Ž (๐‘‡โ€˜๐ด))) = ((โˆ—โ€˜๐ถ) ยท ((๐‘‡โ€˜๐ด) ยทih (๐‘‡โ€˜๐ด)))
113112oveq1i 7371 . . . . . . . . . . . . 13 (((๐‘‡โ€˜๐ด) ยทih (๐ถ ยทโ„Ž (๐‘‡โ€˜๐ด))) + ((๐‘‡โ€˜๐ด) ยทih (๐‘‡โ€˜๐ต))) = (((โˆ—โ€˜๐ถ) ยท ((๐‘‡โ€˜๐ด) ยทih (๐‘‡โ€˜๐ด))) + ((๐‘‡โ€˜๐ด) ยทih (๐‘‡โ€˜๐ต)))
114110, 113eqtri 2761 . . . . . . . . . . . 12 ((๐‘‡โ€˜๐ด) ยทih ((๐ถ ยทโ„Ž (๐‘‡โ€˜๐ด)) +โ„Ž (๐‘‡โ€˜๐ต))) = (((โˆ—โ€˜๐ถ) ยท ((๐‘‡โ€˜๐ด) ยทih (๐‘‡โ€˜๐ด))) + ((๐‘‡โ€˜๐ด) ยทih (๐‘‡โ€˜๐ต)))
115114oveq2i 7372 . . . . . . . . . . 11 (๐ถ ยท ((๐‘‡โ€˜๐ด) ยทih ((๐ถ ยทโ„Ž (๐‘‡โ€˜๐ด)) +โ„Ž (๐‘‡โ€˜๐ต)))) = (๐ถ ยท (((โˆ—โ€˜๐ถ) ยท ((๐‘‡โ€˜๐ด) ยทih (๐‘‡โ€˜๐ด))) + ((๐‘‡โ€˜๐ด) ยทih (๐‘‡โ€˜๐ต))))
1161, 53, 10adddii 11175 . . . . . . . . . . 11 (๐ถ ยท (((โˆ—โ€˜๐ถ) ยท ((๐‘‡โ€˜๐ด) ยทih (๐‘‡โ€˜๐ด))) + ((๐‘‡โ€˜๐ด) ยทih (๐‘‡โ€˜๐ต)))) = ((๐ถ ยท ((โˆ—โ€˜๐ถ) ยท ((๐‘‡โ€˜๐ด) ยทih (๐‘‡โ€˜๐ด)))) + (๐ถ ยท ((๐‘‡โ€˜๐ด) ยทih (๐‘‡โ€˜๐ต))))
117108, 115, 1163eqtri 2765 . . . . . . . . . 10 ((๐ถ ยทโ„Ž (๐‘‡โ€˜๐ด)) ยทih ((๐ถ ยทโ„Ž (๐‘‡โ€˜๐ด)) +โ„Ž (๐‘‡โ€˜๐ต))) = ((๐ถ ยท ((โˆ—โ€˜๐ถ) ยท ((๐‘‡โ€˜๐ด) ยทih (๐‘‡โ€˜๐ด)))) + (๐ถ ยท ((๐‘‡โ€˜๐ด) ยทih (๐‘‡โ€˜๐ต))))
118 his7 30081 . . . . . . . . . . . 12 (((๐‘‡โ€˜๐ต) โˆˆ โ„‹ โˆง (๐ถ ยทโ„Ž (๐‘‡โ€˜๐ด)) โˆˆ โ„‹ โˆง (๐‘‡โ€˜๐ต) โˆˆ โ„‹) โ†’ ((๐‘‡โ€˜๐ต) ยทih ((๐ถ ยทโ„Ž (๐‘‡โ€˜๐ด)) +โ„Ž (๐‘‡โ€˜๐ต))) = (((๐‘‡โ€˜๐ต) ยทih (๐ถ ยทโ„Ž (๐‘‡โ€˜๐ด))) + ((๐‘‡โ€˜๐ต) ยทih (๐‘‡โ€˜๐ต))))
1199, 102, 9, 118mp3an 1462 . . . . . . . . . . 11 ((๐‘‡โ€˜๐ต) ยทih ((๐ถ ยทโ„Ž (๐‘‡โ€˜๐ด)) +โ„Ž (๐‘‡โ€˜๐ต))) = (((๐‘‡โ€˜๐ต) ยทih (๐ถ ยทโ„Ž (๐‘‡โ€˜๐ด))) + ((๐‘‡โ€˜๐ต) ยทih (๐‘‡โ€˜๐ต)))
120 his5 30077 . . . . . . . . . . . . . 14 ((๐ถ โˆˆ โ„‚ โˆง (๐‘‡โ€˜๐ต) โˆˆ โ„‹ โˆง (๐‘‡โ€˜๐ด) โˆˆ โ„‹) โ†’ ((๐‘‡โ€˜๐ต) ยทih (๐ถ ยทโ„Ž (๐‘‡โ€˜๐ด))) = ((โˆ—โ€˜๐ถ) ยท ((๐‘‡โ€˜๐ต) ยทih (๐‘‡โ€˜๐ด))))
1211, 9, 6, 120mp3an 1462 . . . . . . . . . . . . 13 ((๐‘‡โ€˜๐ต) ยทih (๐ถ ยทโ„Ž (๐‘‡โ€˜๐ด))) = ((โˆ—โ€˜๐ถ) ยท ((๐‘‡โ€˜๐ต) ยทih (๐‘‡โ€˜๐ด)))
1221, 10cjmuli 15083 . . . . . . . . . . . . . 14 (โˆ—โ€˜(๐ถ ยท ((๐‘‡โ€˜๐ด) ยทih (๐‘‡โ€˜๐ต)))) = ((โˆ—โ€˜๐ถ) ยท (โˆ—โ€˜((๐‘‡โ€˜๐ด) ยทih (๐‘‡โ€˜๐ต))))
1239, 6his1i 30091 . . . . . . . . . . . . . . 15 ((๐‘‡โ€˜๐ต) ยทih (๐‘‡โ€˜๐ด)) = (โˆ—โ€˜((๐‘‡โ€˜๐ด) ยทih (๐‘‡โ€˜๐ต)))
124123oveq2i 7372 . . . . . . . . . . . . . 14 ((โˆ—โ€˜๐ถ) ยท ((๐‘‡โ€˜๐ต) ยทih (๐‘‡โ€˜๐ด))) = ((โˆ—โ€˜๐ถ) ยท (โˆ—โ€˜((๐‘‡โ€˜๐ด) ยทih (๐‘‡โ€˜๐ต))))
125122, 124eqtr4i 2764 . . . . . . . . . . . . 13 (โˆ—โ€˜(๐ถ ยท ((๐‘‡โ€˜๐ด) ยทih (๐‘‡โ€˜๐ต)))) = ((โˆ—โ€˜๐ถ) ยท ((๐‘‡โ€˜๐ต) ยทih (๐‘‡โ€˜๐ด)))
126121, 125eqtr4i 2764 . . . . . . . . . . . 12 ((๐‘‡โ€˜๐ต) ยทih (๐ถ ยทโ„Ž (๐‘‡โ€˜๐ด))) = (โˆ—โ€˜(๐ถ ยท ((๐‘‡โ€˜๐ด) ยทih (๐‘‡โ€˜๐ต))))
127126oveq1i 7371 . . . . . . . . . . 11 (((๐‘‡โ€˜๐ต) ยทih (๐ถ ยทโ„Ž (๐‘‡โ€˜๐ด))) + ((๐‘‡โ€˜๐ต) ยทih (๐‘‡โ€˜๐ต))) = ((โˆ—โ€˜(๐ถ ยท ((๐‘‡โ€˜๐ด) ยทih (๐‘‡โ€˜๐ต)))) + ((๐‘‡โ€˜๐ต) ยทih (๐‘‡โ€˜๐ต)))
128119, 127eqtri 2761 . . . . . . . . . 10 ((๐‘‡โ€˜๐ต) ยทih ((๐ถ ยทโ„Ž (๐‘‡โ€˜๐ด)) +โ„Ž (๐‘‡โ€˜๐ต))) = ((โˆ—โ€˜(๐ถ ยท ((๐‘‡โ€˜๐ด) ยทih (๐‘‡โ€˜๐ต)))) + ((๐‘‡โ€˜๐ต) ยทih (๐‘‡โ€˜๐ต)))
129117, 128oveq12i 7373 . . . . . . . . 9 (((๐ถ ยทโ„Ž (๐‘‡โ€˜๐ด)) ยทih ((๐ถ ยทโ„Ž (๐‘‡โ€˜๐ด)) +โ„Ž (๐‘‡โ€˜๐ต))) + ((๐‘‡โ€˜๐ต) ยทih ((๐ถ ยทโ„Ž (๐‘‡โ€˜๐ด)) +โ„Ž (๐‘‡โ€˜๐ต)))) = (((๐ถ ยท ((โˆ—โ€˜๐ถ) ยท ((๐‘‡โ€˜๐ด) ยทih (๐‘‡โ€˜๐ด)))) + (๐ถ ยท ((๐‘‡โ€˜๐ด) ยทih (๐‘‡โ€˜๐ต)))) + ((โˆ—โ€˜(๐ถ ยท ((๐‘‡โ€˜๐ด) ยทih (๐‘‡โ€˜๐ต)))) + ((๐‘‡โ€˜๐ต) ยทih (๐‘‡โ€˜๐ต))))
13098, 106, 1293eqtrri 2766 . . . . . . . 8 (((๐ถ ยท ((โˆ—โ€˜๐ถ) ยท ((๐‘‡โ€˜๐ด) ยทih (๐‘‡โ€˜๐ด)))) + (๐ถ ยท ((๐‘‡โ€˜๐ด) ยทih (๐‘‡โ€˜๐ต)))) + ((โˆ—โ€˜(๐ถ ยท ((๐‘‡โ€˜๐ด) ยทih (๐‘‡โ€˜๐ต)))) + ((๐‘‡โ€˜๐ต) ยทih (๐‘‡โ€˜๐ต)))) = (((๐ถ ยท ((โˆ—โ€˜๐ถ) ยท (๐ด ยทih ๐ด))) + (๐ถ ยท (๐ด ยทih ๐ต))) + ((โˆ—โ€˜(๐ถ ยท (๐ด ยทih ๐ต))) + (๐ต ยทih ๐ต)))
13163, 130eqtr4i 2764 . . . . . . 7 (((๐ถ ยท ((โˆ—โ€˜๐ถ) ยท (๐ด ยทih ๐ด))) + (๐ต ยทih ๐ต)) + ((๐ถ ยท (๐ด ยทih ๐ต)) + (โˆ—โ€˜(๐ถ ยท (๐ด ยทih ๐ต))))) = (((๐ถ ยท ((โˆ—โ€˜๐ถ) ยท ((๐‘‡โ€˜๐ด) ยทih (๐‘‡โ€˜๐ด)))) + (๐ถ ยท ((๐‘‡โ€˜๐ด) ยทih (๐‘‡โ€˜๐ต)))) + ((โˆ—โ€˜(๐ถ ยท ((๐‘‡โ€˜๐ด) ยทih (๐‘‡โ€˜๐ต)))) + ((๐‘‡โ€˜๐ต) ยทih (๐‘‡โ€˜๐ต))))
13257, 131eqtr4i 2764 . . . . . 6 (((๐ถ ยท ((โˆ—โ€˜๐ถ) ยท ((๐‘‡โ€˜๐ด) ยทih (๐‘‡โ€˜๐ด)))) + ((๐‘‡โ€˜๐ต) ยทih (๐‘‡โ€˜๐ต))) + ((๐ถ ยท ((๐‘‡โ€˜๐ด) ยทih (๐‘‡โ€˜๐ต))) + (โˆ—โ€˜(๐ถ ยท ((๐‘‡โ€˜๐ด) ยทih (๐‘‡โ€˜๐ต)))))) = (((๐ถ ยท ((โˆ—โ€˜๐ถ) ยท (๐ด ยทih ๐ด))) + (๐ต ยทih ๐ต)) + ((๐ถ ยท (๐ด ยทih ๐ต)) + (โˆ—โ€˜(๐ถ ยท (๐ด ยทih ๐ต)))))
13350, 132eqtr3i 2763 . . . . 5 (((๐ถ ยท ((โˆ—โ€˜๐ถ) ยท (๐ด ยทih ๐ด))) + (๐ต ยทih ๐ต)) + ((๐ถ ยท ((๐‘‡โ€˜๐ด) ยทih (๐‘‡โ€˜๐ต))) + (โˆ—โ€˜(๐ถ ยท ((๐‘‡โ€˜๐ด) ยทih (๐‘‡โ€˜๐ต)))))) = (((๐ถ ยท ((โˆ—โ€˜๐ถ) ยท (๐ด ยทih ๐ด))) + (๐ต ยทih ๐ต)) + ((๐ถ ยท (๐ด ยทih ๐ต)) + (โˆ—โ€˜(๐ถ ยท (๐ด ยทih ๐ต)))))
13460, 61addcli 11169 . . . . . 6 ((๐ถ ยท ((โˆ—โ€˜๐ถ) ยท (๐ด ยทih ๐ด))) + (๐ต ยทih ๐ต)) โˆˆ โ„‚
13511, 56addcli 11169 . . . . . 6 ((๐ถ ยท ((๐‘‡โ€˜๐ด) ยทih (๐‘‡โ€˜๐ต))) + (โˆ—โ€˜(๐ถ ยท ((๐‘‡โ€˜๐ด) ยทih (๐‘‡โ€˜๐ต))))) โˆˆ โ„‚
13615, 62addcli 11169 . . . . . 6 ((๐ถ ยท (๐ด ยทih ๐ต)) + (โˆ—โ€˜(๐ถ ยท (๐ด ยทih ๐ต)))) โˆˆ โ„‚
137134, 135, 136addcani 11356 . . . . 5 ((((๐ถ ยท ((โˆ—โ€˜๐ถ) ยท (๐ด ยทih ๐ด))) + (๐ต ยทih ๐ต)) + ((๐ถ ยท ((๐‘‡โ€˜๐ด) ยทih (๐‘‡โ€˜๐ต))) + (โˆ—โ€˜(๐ถ ยท ((๐‘‡โ€˜๐ด) ยทih (๐‘‡โ€˜๐ต)))))) = (((๐ถ ยท ((โˆ—โ€˜๐ถ) ยท (๐ด ยทih ๐ด))) + (๐ต ยทih ๐ต)) + ((๐ถ ยท (๐ด ยทih ๐ต)) + (โˆ—โ€˜(๐ถ ยท (๐ด ยทih ๐ต))))) โ†” ((๐ถ ยท ((๐‘‡โ€˜๐ด) ยทih (๐‘‡โ€˜๐ต))) + (โˆ—โ€˜(๐ถ ยท ((๐‘‡โ€˜๐ด) ยทih (๐‘‡โ€˜๐ต))))) = ((๐ถ ยท (๐ด ยทih ๐ต)) + (โˆ—โ€˜(๐ถ ยท (๐ด ยทih ๐ต)))))
138133, 137mpbi 229 . . . 4 ((๐ถ ยท ((๐‘‡โ€˜๐ด) ยทih (๐‘‡โ€˜๐ต))) + (โˆ—โ€˜(๐ถ ยท ((๐‘‡โ€˜๐ด) ยทih (๐‘‡โ€˜๐ต))))) = ((๐ถ ยท (๐ด ยทih ๐ต)) + (โˆ—โ€˜(๐ถ ยท (๐ด ยทih ๐ต))))
139138oveq1i 7371 . . 3 (((๐ถ ยท ((๐‘‡โ€˜๐ด) ยทih (๐‘‡โ€˜๐ต))) + (โˆ—โ€˜(๐ถ ยท ((๐‘‡โ€˜๐ด) ยทih (๐‘‡โ€˜๐ต))))) / 2) = (((๐ถ ยท (๐ด ยทih ๐ต)) + (โˆ—โ€˜(๐ถ ยท (๐ด ยทih ๐ต)))) / 2)
14017, 139eqtr4i 2764 . 2 (โ„œโ€˜(๐ถ ยท (๐ด ยทih ๐ต))) = (((๐ถ ยท ((๐‘‡โ€˜๐ด) ยทih (๐‘‡โ€˜๐ต))) + (โˆ—โ€˜(๐ถ ยท ((๐‘‡โ€˜๐ด) ยทih (๐‘‡โ€˜๐ต))))) / 2)
14113, 140eqtr4i 2764 1 (โ„œโ€˜(๐ถ ยท ((๐‘‡โ€˜๐ด) ยทih (๐‘‡โ€˜๐ต)))) = (โ„œโ€˜(๐ถ ยท (๐ด ยทih ๐ต)))
Colors of variables: wff setvar class
Syntax hints:   = wceq 1542   โˆˆ wcel 2107  โˆ€wral 3061  โ€˜cfv 6500  (class class class)co 7361  โ„‚cc 11057   + caddc 11062   ยท cmul 11064   / cdiv 11820  2c2 12216  โ†‘cexp 13976  โˆ—ccj 14990  โ„œcre 14991   โ„‹chba 29910   +โ„Ž cva 29911   ยทโ„Ž csm 29912   ยทih csp 29913  normโ„Žcno 29914  LinOpclo 29938
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-10 2138  ax-11 2155  ax-12 2172  ax-ext 2704  ax-sep 5260  ax-nul 5267  ax-pow 5324  ax-pr 5388  ax-un 7676  ax-cnex 11115  ax-resscn 11116  ax-1cn 11117  ax-icn 11118  ax-addcl 11119  ax-addrcl 11120  ax-mulcl 11121  ax-mulrcl 11122  ax-mulcom 11123  ax-addass 11124  ax-mulass 11125  ax-distr 11126  ax-i2m1 11127  ax-1ne0 11128  ax-1rid 11129  ax-rnegex 11130  ax-rrecex 11131  ax-cnre 11132  ax-pre-lttri 11133  ax-pre-lttrn 11134  ax-pre-ltadd 11135  ax-pre-mulgt0 11136  ax-pre-sup 11137  ax-hilex 29990  ax-hfvadd 29991  ax-hv0cl 29994  ax-hfvmul 29996  ax-hvmul0 30001  ax-hfi 30070  ax-his1 30073  ax-his2 30074  ax-his3 30075  ax-his4 30076
This theorem depends on definitions:  df-bi 206  df-an 398  df-or 847  df-3or 1089  df-3an 1090  df-tru 1545  df-fal 1555  df-ex 1783  df-nf 1787  df-sb 2069  df-mo 2535  df-eu 2564  df-clab 2711  df-cleq 2725  df-clel 2811  df-nfc 2886  df-ne 2941  df-nel 3047  df-ral 3062  df-rex 3071  df-rmo 3352  df-reu 3353  df-rab 3407  df-v 3449  df-sbc 3744  df-csb 3860  df-dif 3917  df-un 3919  df-in 3921  df-ss 3931  df-pss 3933  df-nul 4287  df-if 4491  df-pw 4566  df-sn 4591  df-pr 4593  df-op 4597  df-uni 4870  df-iun 4960  df-br 5110  df-opab 5172  df-mpt 5193  df-tr 5227  df-id 5535  df-eprel 5541  df-po 5549  df-so 5550  df-fr 5592  df-we 5594  df-xp 5643  df-rel 5644  df-cnv 5645  df-co 5646  df-dm 5647  df-rn 5648  df-res 5649  df-ima 5650  df-pred 6257  df-ord 6324  df-on 6325  df-lim 6326  df-suc 6327  df-iota 6452  df-fun 6502  df-fn 6503  df-f 6504  df-f1 6505  df-fo 6506  df-f1o 6507  df-fv 6508  df-riota 7317  df-ov 7364  df-oprab 7365  df-mpo 7366  df-om 7807  df-2nd 7926  df-frecs 8216  df-wrecs 8247  df-recs 8321  df-rdg 8360  df-er 8654  df-map 8773  df-en 8890  df-dom 8891  df-sdom 8892  df-sup 9386  df-pnf 11199  df-mnf 11200  df-xr 11201  df-ltxr 11202  df-le 11203  df-sub 11395  df-neg 11396  df-div 11821  df-nn 12162  df-2 12224  df-3 12225  df-n0 12422  df-z 12508  df-uz 12772  df-rp 12924  df-seq 13916  df-exp 13977  df-cj 14993  df-re 14994  df-im 14995  df-sqrt 15129  df-hnorm 29959  df-lnop 30832
This theorem is referenced by:  lnopunilem2  31002
  Copyright terms: Public domain W3C validator