Step | Hyp | Ref
| Expression |
1 | | ovex 7391 |
. . . 4
β’
(((braβπ΄)βπ΅) Β· ((braβπΆ)βπ₯)) β V |
2 | | eqid 2733 |
. . . 4
β’ (π₯ β β β¦
(((braβπ΄)βπ΅) Β· ((braβπΆ)βπ₯))) = (π₯ β β β¦ (((braβπ΄)βπ΅) Β· ((braβπΆ)βπ₯))) |
3 | 1, 2 | fnmpti 6645 |
. . 3
β’ (π₯ β β β¦
(((braβπ΄)βπ΅) Β· ((braβπΆ)βπ₯))) Fn β |
4 | | bracl 30933 |
. . . . . 6
β’ ((π΄ β β β§ π΅ β β) β
((braβπ΄)βπ΅) β
β) |
5 | | brafn 30931 |
. . . . . 6
β’ (πΆ β β β
(braβπΆ):
ββΆβ) |
6 | | hfmmval 30723 |
. . . . . 6
β’
((((braβπ΄)βπ΅) β β β§ (braβπΆ): ββΆβ)
β (((braβπ΄)βπ΅) Β·fn
(braβπΆ)) = (π₯ β β β¦
(((braβπ΄)βπ΅) Β· ((braβπΆ)βπ₯)))) |
7 | 4, 5, 6 | syl2an 597 |
. . . . 5
β’ (((π΄ β β β§ π΅ β β) β§ πΆ β β) β
(((braβπ΄)βπ΅) Β·fn
(braβπΆ)) = (π₯ β β β¦
(((braβπ΄)βπ΅) Β· ((braβπΆ)βπ₯)))) |
8 | 7 | 3impa 1111 |
. . . 4
β’ ((π΄ β β β§ π΅ β β β§ πΆ β β) β
(((braβπ΄)βπ΅) Β·fn
(braβπΆ)) = (π₯ β β β¦
(((braβπ΄)βπ΅) Β· ((braβπΆ)βπ₯)))) |
9 | 8 | fneq1d 6596 |
. . 3
β’ ((π΄ β β β§ π΅ β β β§ πΆ β β) β
((((braβπ΄)βπ΅) Β·fn
(braβπΆ)) Fn β
β (π₯ β β
β¦ (((braβπ΄)βπ΅) Β· ((braβπΆ)βπ₯))) Fn β)) |
10 | 3, 9 | mpbiri 258 |
. 2
β’ ((π΄ β β β§ π΅ β β β§ πΆ β β) β
(((braβπ΄)βπ΅) Β·fn
(braβπΆ)) Fn
β) |
11 | | brafn 30931 |
. . . . 5
β’ (π΄ β β β
(braβπ΄):
ββΆβ) |
12 | | kbop 30937 |
. . . . 5
β’ ((π΅ β β β§ πΆ β β) β (π΅ ketbra πΆ): ββΆ β) |
13 | | fco 6693 |
. . . . 5
β’
(((braβπ΄):
ββΆβ β§ (π΅ ketbra πΆ): ββΆ β) β
((braβπ΄) β
(π΅ ketbra πΆ)): ββΆβ) |
14 | 11, 12, 13 | syl2an 597 |
. . . 4
β’ ((π΄ β β β§ (π΅ β β β§ πΆ β β)) β
((braβπ΄) β
(π΅ ketbra πΆ)): ββΆβ) |
15 | 14 | 3impb 1116 |
. . 3
β’ ((π΄ β β β§ π΅ β β β§ πΆ β β) β
((braβπ΄) β
(π΅ ketbra πΆ)): ββΆβ) |
16 | 15 | ffnd 6670 |
. 2
β’ ((π΄ β β β§ π΅ β β β§ πΆ β β) β
((braβπ΄) β
(π΅ ketbra πΆ)) Fn β) |
17 | | simpl1 1192 |
. . . . 5
β’ (((π΄ β β β§ π΅ β β β§ πΆ β β) β§ π₯ β β) β π΄ β
β) |
18 | | simpl2 1193 |
. . . . 5
β’ (((π΄ β β β§ π΅ β β β§ πΆ β β) β§ π₯ β β) β π΅ β
β) |
19 | | braval 30928 |
. . . . 5
β’ ((π΄ β β β§ π΅ β β) β
((braβπ΄)βπ΅) = (π΅ Β·ih π΄)) |
20 | 17, 18, 19 | syl2anc 585 |
. . . 4
β’ (((π΄ β β β§ π΅ β β β§ πΆ β β) β§ π₯ β β) β
((braβπ΄)βπ΅) = (π΅ Β·ih π΄)) |
21 | | simpl3 1194 |
. . . . 5
β’ (((π΄ β β β§ π΅ β β β§ πΆ β β) β§ π₯ β β) β πΆ β
β) |
22 | | simpr 486 |
. . . . 5
β’ (((π΄ β β β§ π΅ β β β§ πΆ β β) β§ π₯ β β) β π₯ β
β) |
23 | | braval 30928 |
. . . . 5
β’ ((πΆ β β β§ π₯ β β) β
((braβπΆ)βπ₯) = (π₯ Β·ih πΆ)) |
24 | 21, 22, 23 | syl2anc 585 |
. . . 4
β’ (((π΄ β β β§ π΅ β β β§ πΆ β β) β§ π₯ β β) β
((braβπΆ)βπ₯) = (π₯ Β·ih πΆ)) |
25 | 20, 24 | oveq12d 7376 |
. . 3
β’ (((π΄ β β β§ π΅ β β β§ πΆ β β) β§ π₯ β β) β
(((braβπ΄)βπ΅) Β· ((braβπΆ)βπ₯)) = ((π΅ Β·ih π΄) Β· (π₯ Β·ih πΆ))) |
26 | | hicl 30064 |
. . . . . 6
β’ ((π΅ β β β§ π΄ β β) β (π΅
Β·ih π΄) β β) |
27 | 18, 17, 26 | syl2anc 585 |
. . . . 5
β’ (((π΄ β β β§ π΅ β β β§ πΆ β β) β§ π₯ β β) β (π΅
Β·ih π΄) β β) |
28 | 20, 27 | eqeltrd 2834 |
. . . 4
β’ (((π΄ β β β§ π΅ β β β§ πΆ β β) β§ π₯ β β) β
((braβπ΄)βπ΅) β
β) |
29 | 21, 5 | syl 17 |
. . . 4
β’ (((π΄ β β β§ π΅ β β β§ πΆ β β) β§ π₯ β β) β
(braβπΆ):
ββΆβ) |
30 | | hfmval 30728 |
. . . 4
β’
((((braβπ΄)βπ΅) β β β§ (braβπΆ): ββΆβ β§
π₯ β β) β
((((braβπ΄)βπ΅) Β·fn
(braβπΆ))βπ₯) = (((braβπ΄)βπ΅) Β· ((braβπΆ)βπ₯))) |
31 | 28, 29, 22, 30 | syl3anc 1372 |
. . 3
β’ (((π΄ β β β§ π΅ β β β§ πΆ β β) β§ π₯ β β) β
((((braβπ΄)βπ΅) Β·fn
(braβπΆ))βπ₯) = (((braβπ΄)βπ΅) Β· ((braβπΆ)βπ₯))) |
32 | | hicl 30064 |
. . . . . 6
β’ ((π₯ β β β§ πΆ β β) β (π₯
Β·ih πΆ) β β) |
33 | 22, 21, 32 | syl2anc 585 |
. . . . 5
β’ (((π΄ β β β§ π΅ β β β§ πΆ β β) β§ π₯ β β) β (π₯
Β·ih πΆ) β β) |
34 | | ax-his3 30068 |
. . . . 5
β’ (((π₯
Β·ih πΆ) β β β§ π΅ β β β§ π΄ β β) β (((π₯
Β·ih πΆ) Β·β π΅)
Β·ih π΄) = ((π₯ Β·ih πΆ) Β· (π΅ Β·ih π΄))) |
35 | 33, 18, 17, 34 | syl3anc 1372 |
. . . 4
β’ (((π΄ β β β§ π΅ β β β§ πΆ β β) β§ π₯ β β) β (((π₯
Β·ih πΆ) Β·β π΅)
Β·ih π΄) = ((π₯ Β·ih πΆ) Β· (π΅ Β·ih π΄))) |
36 | 12 | 3adant1 1131 |
. . . . . 6
β’ ((π΄ β β β§ π΅ β β β§ πΆ β β) β (π΅ ketbra πΆ): ββΆ β) |
37 | | fvco3 6941 |
. . . . . 6
β’ (((π΅ ketbra πΆ): ββΆ β β§ π₯ β β) β
(((braβπ΄) β
(π΅ ketbra πΆ))βπ₯) = ((braβπ΄)β((π΅ ketbra πΆ)βπ₯))) |
38 | 36, 37 | sylan 581 |
. . . . 5
β’ (((π΄ β β β§ π΅ β β β§ πΆ β β) β§ π₯ β β) β
(((braβπ΄) β
(π΅ ketbra πΆ))βπ₯) = ((braβπ΄)β((π΅ ketbra πΆ)βπ₯))) |
39 | | kbval 30938 |
. . . . . . 7
β’ ((π΅ β β β§ πΆ β β β§ π₯ β β) β ((π΅ ketbra πΆ)βπ₯) = ((π₯ Β·ih πΆ)
Β·β π΅)) |
40 | 18, 21, 22, 39 | syl3anc 1372 |
. . . . . 6
β’ (((π΄ β β β§ π΅ β β β§ πΆ β β) β§ π₯ β β) β ((π΅ ketbra πΆ)βπ₯) = ((π₯ Β·ih πΆ)
Β·β π΅)) |
41 | 40 | fveq2d 6847 |
. . . . 5
β’ (((π΄ β β β§ π΅ β β β§ πΆ β β) β§ π₯ β β) β
((braβπ΄)β((π΅ ketbra πΆ)βπ₯)) = ((braβπ΄)β((π₯ Β·ih πΆ)
Β·β π΅))) |
42 | | hvmulcl 29997 |
. . . . . . 7
β’ (((π₯
Β·ih πΆ) β β β§ π΅ β β) β ((π₯ Β·ih πΆ)
Β·β π΅) β β) |
43 | 33, 18, 42 | syl2anc 585 |
. . . . . 6
β’ (((π΄ β β β§ π΅ β β β§ πΆ β β) β§ π₯ β β) β ((π₯
Β·ih πΆ) Β·β π΅) β
β) |
44 | | braval 30928 |
. . . . . 6
β’ ((π΄ β β β§ ((π₯
Β·ih πΆ) Β·β π΅) β β) β
((braβπ΄)β((π₯ Β·ih πΆ)
Β·β π΅)) = (((π₯ Β·ih πΆ)
Β·β π΅) Β·ih π΄)) |
45 | 17, 43, 44 | syl2anc 585 |
. . . . 5
β’ (((π΄ β β β§ π΅ β β β§ πΆ β β) β§ π₯ β β) β
((braβπ΄)β((π₯ Β·ih πΆ)
Β·β π΅)) = (((π₯ Β·ih πΆ)
Β·β π΅) Β·ih π΄)) |
46 | 38, 41, 45 | 3eqtrd 2777 |
. . . 4
β’ (((π΄ β β β§ π΅ β β β§ πΆ β β) β§ π₯ β β) β
(((braβπ΄) β
(π΅ ketbra πΆ))βπ₯) = (((π₯ Β·ih πΆ)
Β·β π΅) Β·ih π΄)) |
47 | 27, 33 | mulcomd 11181 |
. . . 4
β’ (((π΄ β β β§ π΅ β β β§ πΆ β β) β§ π₯ β β) β ((π΅
Β·ih π΄) Β· (π₯ Β·ih πΆ)) = ((π₯ Β·ih πΆ) Β· (π΅ Β·ih π΄))) |
48 | 35, 46, 47 | 3eqtr4d 2783 |
. . 3
β’ (((π΄ β β β§ π΅ β β β§ πΆ β β) β§ π₯ β β) β
(((braβπ΄) β
(π΅ ketbra πΆ))βπ₯) = ((π΅ Β·ih π΄) Β· (π₯ Β·ih πΆ))) |
49 | 25, 31, 48 | 3eqtr4d 2783 |
. 2
β’ (((π΄ β β β§ π΅ β β β§ πΆ β β) β§ π₯ β β) β
((((braβπ΄)βπ΅) Β·fn
(braβπΆ))βπ₯) = (((braβπ΄) β (π΅ ketbra πΆ))βπ₯)) |
50 | 10, 16, 49 | eqfnfvd 6986 |
1
β’ ((π΄ β β β§ π΅ β β β§ πΆ β β) β
(((braβπ΄)βπ΅) Β·fn
(braβπΆ)) =
((braβπ΄) β
(π΅ ketbra πΆ))) |