Step | Hyp | Ref
| Expression |
1 | | addcl 11138 |
. . . . . . . 8
โข ((๐ด โ โ โง ๐ต โ โ) โ (๐ด + ๐ต) โ โ) |
2 | 1 | anim1i 616 |
. . . . . . 7
โข (((๐ด โ โ โง ๐ต โ โ) โง ๐: โโถ โ)
โ ((๐ด + ๐ต) โ โ โง ๐: โโถ
โ)) |
3 | 2 | 3impa 1111 |
. . . . . 6
โข ((๐ด โ โ โง ๐ต โ โ โง ๐: โโถ โ)
โ ((๐ด + ๐ต) โ โ โง ๐: โโถ
โ)) |
4 | | homval 30725 |
. . . . . . 7
โข (((๐ด + ๐ต) โ โ โง ๐: โโถ โ โง ๐ฅ โ โ) โ (((๐ด + ๐ต) ยทop ๐)โ๐ฅ) = ((๐ด + ๐ต) ยทโ (๐โ๐ฅ))) |
5 | 4 | 3expa 1119 |
. . . . . 6
โข ((((๐ด + ๐ต) โ โ โง ๐: โโถ โ) โง ๐ฅ โ โ) โ (((๐ด + ๐ต) ยทop ๐)โ๐ฅ) = ((๐ด + ๐ต) ยทโ (๐โ๐ฅ))) |
6 | 3, 5 | sylan 581 |
. . . . 5
โข (((๐ด โ โ โง ๐ต โ โ โง ๐: โโถ โ) โง
๐ฅ โ โ) โ
(((๐ด + ๐ต) ยทop ๐)โ๐ฅ) = ((๐ด + ๐ต) ยทโ (๐โ๐ฅ))) |
7 | | homval 30725 |
. . . . . . . . 9
โข ((๐ด โ โ โง ๐: โโถ โ โง
๐ฅ โ โ) โ
((๐ด
ยทop ๐)โ๐ฅ) = (๐ด ยทโ (๐โ๐ฅ))) |
8 | 7 | 3expa 1119 |
. . . . . . . 8
โข (((๐ด โ โ โง ๐: โโถ โ) โง
๐ฅ โ โ) โ
((๐ด
ยทop ๐)โ๐ฅ) = (๐ด ยทโ (๐โ๐ฅ))) |
9 | 8 | 3adantl2 1168 |
. . . . . . 7
โข (((๐ด โ โ โง ๐ต โ โ โง ๐: โโถ โ) โง
๐ฅ โ โ) โ
((๐ด
ยทop ๐)โ๐ฅ) = (๐ด ยทโ (๐โ๐ฅ))) |
10 | | homval 30725 |
. . . . . . . . 9
โข ((๐ต โ โ โง ๐: โโถ โ โง
๐ฅ โ โ) โ
((๐ต
ยทop ๐)โ๐ฅ) = (๐ต ยทโ (๐โ๐ฅ))) |
11 | 10 | 3expa 1119 |
. . . . . . . 8
โข (((๐ต โ โ โง ๐: โโถ โ) โง
๐ฅ โ โ) โ
((๐ต
ยทop ๐)โ๐ฅ) = (๐ต ยทโ (๐โ๐ฅ))) |
12 | 11 | 3adantl1 1167 |
. . . . . . 7
โข (((๐ด โ โ โง ๐ต โ โ โง ๐: โโถ โ) โง
๐ฅ โ โ) โ
((๐ต
ยทop ๐)โ๐ฅ) = (๐ต ยทโ (๐โ๐ฅ))) |
13 | 9, 12 | oveq12d 7376 |
. . . . . 6
โข (((๐ด โ โ โง ๐ต โ โ โง ๐: โโถ โ) โง
๐ฅ โ โ) โ
(((๐ด
ยทop ๐)โ๐ฅ) +โ ((๐ต ยทop ๐)โ๐ฅ)) = ((๐ด ยทโ (๐โ๐ฅ)) +โ (๐ต ยทโ (๐โ๐ฅ)))) |
14 | | ffvelcdm 7033 |
. . . . . . . . . 10
โข ((๐: โโถ โ โง
๐ฅ โ โ) โ
(๐โ๐ฅ) โ โ) |
15 | | ax-hvdistr2 29993 |
. . . . . . . . . 10
โข ((๐ด โ โ โง ๐ต โ โ โง (๐โ๐ฅ) โ โ) โ ((๐ด + ๐ต) ยทโ (๐โ๐ฅ)) = ((๐ด ยทโ (๐โ๐ฅ)) +โ (๐ต ยทโ (๐โ๐ฅ)))) |
16 | 14, 15 | syl3an3 1166 |
. . . . . . . . 9
โข ((๐ด โ โ โง ๐ต โ โ โง (๐: โโถ โ โง
๐ฅ โ โ)) โ
((๐ด + ๐ต) ยทโ (๐โ๐ฅ)) = ((๐ด ยทโ (๐โ๐ฅ)) +โ (๐ต ยทโ (๐โ๐ฅ)))) |
17 | 16 | 3exp 1120 |
. . . . . . . 8
โข (๐ด โ โ โ (๐ต โ โ โ ((๐: โโถ โ โง
๐ฅ โ โ) โ
((๐ด + ๐ต) ยทโ (๐โ๐ฅ)) = ((๐ด ยทโ (๐โ๐ฅ)) +โ (๐ต ยทโ (๐โ๐ฅ)))))) |
18 | 17 | exp4a 433 |
. . . . . . 7
โข (๐ด โ โ โ (๐ต โ โ โ (๐: โโถ โ โ
(๐ฅ โ โ โ
((๐ด + ๐ต) ยทโ (๐โ๐ฅ)) = ((๐ด ยทโ (๐โ๐ฅ)) +โ (๐ต ยทโ (๐โ๐ฅ))))))) |
19 | 18 | 3imp1 1348 |
. . . . . 6
โข (((๐ด โ โ โง ๐ต โ โ โง ๐: โโถ โ) โง
๐ฅ โ โ) โ
((๐ด + ๐ต) ยทโ (๐โ๐ฅ)) = ((๐ด ยทโ (๐โ๐ฅ)) +โ (๐ต ยทโ (๐โ๐ฅ)))) |
20 | 13, 19 | eqtr4d 2776 |
. . . . 5
โข (((๐ด โ โ โง ๐ต โ โ โง ๐: โโถ โ) โง
๐ฅ โ โ) โ
(((๐ด
ยทop ๐)โ๐ฅ) +โ ((๐ต ยทop ๐)โ๐ฅ)) = ((๐ด + ๐ต) ยทโ (๐โ๐ฅ))) |
21 | 6, 20 | eqtr4d 2776 |
. . . 4
โข (((๐ด โ โ โง ๐ต โ โ โง ๐: โโถ โ) โง
๐ฅ โ โ) โ
(((๐ด + ๐ต) ยทop ๐)โ๐ฅ) = (((๐ด ยทop ๐)โ๐ฅ) +โ ((๐ต ยทop ๐)โ๐ฅ))) |
22 | | homulcl 30743 |
. . . . . . 7
โข ((๐ด โ โ โง ๐: โโถ โ)
โ (๐ด
ยทop ๐): โโถ โ) |
23 | | homulcl 30743 |
. . . . . . 7
โข ((๐ต โ โ โง ๐: โโถ โ)
โ (๐ต
ยทop ๐): โโถ โ) |
24 | 22, 23 | anim12i 614 |
. . . . . 6
โข (((๐ด โ โ โง ๐: โโถ โ) โง
(๐ต โ โ โง
๐: โโถ
โ)) โ ((๐ด
ยทop ๐): โโถ โ โง (๐ต ยทop
๐): โโถ
โ)) |
25 | 24 | 3impdir 1352 |
. . . . 5
โข ((๐ด โ โ โง ๐ต โ โ โง ๐: โโถ โ)
โ ((๐ด
ยทop ๐): โโถ โ โง (๐ต ยทop
๐): โโถ
โ)) |
26 | | hosval 30724 |
. . . . . 6
โข (((๐ด ยทop
๐): โโถ โ
โง (๐ต
ยทop ๐): โโถ โ โง ๐ฅ โ โ) โ (((๐ด ยทop
๐) +op (๐ต ยทop
๐))โ๐ฅ) = (((๐ด ยทop ๐)โ๐ฅ) +โ ((๐ต ยทop ๐)โ๐ฅ))) |
27 | 26 | 3expa 1119 |
. . . . 5
โข ((((๐ด ยทop
๐): โโถ โ
โง (๐ต
ยทop ๐): โโถ โ) โง ๐ฅ โ โ) โ (((๐ด ยทop
๐) +op (๐ต ยทop
๐))โ๐ฅ) = (((๐ด ยทop ๐)โ๐ฅ) +โ ((๐ต ยทop ๐)โ๐ฅ))) |
28 | 25, 27 | sylan 581 |
. . . 4
โข (((๐ด โ โ โง ๐ต โ โ โง ๐: โโถ โ) โง
๐ฅ โ โ) โ
(((๐ด
ยทop ๐) +op (๐ต ยทop ๐))โ๐ฅ) = (((๐ด ยทop ๐)โ๐ฅ) +โ ((๐ต ยทop ๐)โ๐ฅ))) |
29 | 21, 28 | eqtr4d 2776 |
. . 3
โข (((๐ด โ โ โง ๐ต โ โ โง ๐: โโถ โ) โง
๐ฅ โ โ) โ
(((๐ด + ๐ต) ยทop ๐)โ๐ฅ) = (((๐ด ยทop ๐) +op (๐ต ยทop
๐))โ๐ฅ)) |
30 | 29 | ralrimiva 3140 |
. 2
โข ((๐ด โ โ โง ๐ต โ โ โง ๐: โโถ โ)
โ โ๐ฅ โ
โ (((๐ด + ๐ต) ยทop
๐)โ๐ฅ) = (((๐ด ยทop ๐) +op (๐ต ยทop
๐))โ๐ฅ)) |
31 | | homulcl 30743 |
. . . 4
โข (((๐ด + ๐ต) โ โ โง ๐: โโถ โ) โ ((๐ด + ๐ต) ยทop ๐): โโถ
โ) |
32 | 1, 31 | stoic3 1779 |
. . 3
โข ((๐ด โ โ โง ๐ต โ โ โง ๐: โโถ โ)
โ ((๐ด + ๐ต) ยทop
๐): โโถ
โ) |
33 | | hoaddcl 30742 |
. . . . 5
โข (((๐ด ยทop
๐): โโถ โ
โง (๐ต
ยทop ๐): โโถ โ) โ ((๐ด ยทop
๐) +op (๐ต ยทop
๐)): โโถ
โ) |
34 | 22, 23, 33 | syl2an 597 |
. . . 4
โข (((๐ด โ โ โง ๐: โโถ โ) โง
(๐ต โ โ โง
๐: โโถ
โ)) โ ((๐ด
ยทop ๐) +op (๐ต ยทop ๐)): โโถ
โ) |
35 | 34 | 3impdir 1352 |
. . 3
โข ((๐ด โ โ โง ๐ต โ โ โง ๐: โโถ โ)
โ ((๐ด
ยทop ๐) +op (๐ต ยทop ๐)): โโถ
โ) |
36 | | hoeq 30744 |
. . 3
โข ((((๐ด + ๐ต) ยทop ๐): โโถ โ โง
((๐ด
ยทop ๐) +op (๐ต ยทop ๐)): โโถ โ)
โ (โ๐ฅ โ
โ (((๐ด + ๐ต) ยทop
๐)โ๐ฅ) = (((๐ด ยทop ๐) +op (๐ต ยทop
๐))โ๐ฅ) โ ((๐ด + ๐ต) ยทop ๐) = ((๐ด ยทop ๐) +op (๐ต ยทop
๐)))) |
37 | 32, 35, 36 | syl2anc 585 |
. 2
โข ((๐ด โ โ โง ๐ต โ โ โง ๐: โโถ โ)
โ (โ๐ฅ โ
โ (((๐ด + ๐ต) ยทop
๐)โ๐ฅ) = (((๐ด ยทop ๐) +op (๐ต ยทop
๐))โ๐ฅ) โ ((๐ด + ๐ต) ยทop ๐) = ((๐ด ยทop ๐) +op (๐ต ยทop
๐)))) |
38 | 30, 37 | mpbid 231 |
1
โข ((๐ด โ โ โง ๐ต โ โ โง ๐: โโถ โ)
โ ((๐ด + ๐ต) ยทop
๐) = ((๐ด ยทop ๐) +op (๐ต ยทop
๐))) |