Step | Hyp | Ref
| Expression |
1 | | mamufval.f |
. 2
โข ๐น = (๐
maMul โจ๐, ๐, ๐โฉ) |
2 | | df-mamu 21685 |
. . . 4
โข maMul =
(๐ โ V, ๐ โ V โฆ
โฆ(1st โ(1st โ๐)) / ๐โฆโฆ(2nd
โ(1st โ๐)) / ๐โฆโฆ(2nd
โ๐) / ๐โฆ(๐ฅ โ ((Baseโ๐) โm (๐ ร ๐)), ๐ฆ โ ((Baseโ๐) โm (๐ ร ๐)) โฆ (๐ โ ๐, ๐ โ ๐ โฆ (๐ ฮฃg (๐ โ ๐ โฆ ((๐๐ฅ๐)(.rโ๐)(๐๐ฆ๐))))))) |
3 | 2 | a1i 11 |
. . 3
โข (๐ โ maMul = (๐ โ V, ๐ โ V โฆ
โฆ(1st โ(1st โ๐)) / ๐โฆโฆ(2nd
โ(1st โ๐)) / ๐โฆโฆ(2nd
โ๐) / ๐โฆ(๐ฅ โ ((Baseโ๐) โm (๐ ร ๐)), ๐ฆ โ ((Baseโ๐) โm (๐ ร ๐)) โฆ (๐ โ ๐, ๐ โ ๐ โฆ (๐ ฮฃg (๐ โ ๐ โฆ ((๐๐ฅ๐)(.rโ๐)(๐๐ฆ๐)))))))) |
4 | | fvex 6852 |
. . . . 5
โข
(1st โ(1st โ๐)) โ V |
5 | | fvex 6852 |
. . . . 5
โข
(2nd โ(1st โ๐)) โ V |
6 | | fvex 6852 |
. . . . . . 7
โข
(2nd โ๐) โ V |
7 | | eqidd 2738 |
. . . . . . . 8
โข (๐ = (2nd โ๐) โ ((Baseโ๐) โm (๐ ร ๐)) = ((Baseโ๐) โm (๐ ร ๐))) |
8 | | xpeq2 5652 |
. . . . . . . . 9
โข (๐ = (2nd โ๐) โ (๐ ร ๐) = (๐ ร (2nd โ๐))) |
9 | 8 | oveq2d 7367 |
. . . . . . . 8
โข (๐ = (2nd โ๐) โ ((Baseโ๐) โm (๐ ร ๐)) = ((Baseโ๐) โm (๐ ร (2nd โ๐)))) |
10 | | eqidd 2738 |
. . . . . . . . 9
โข (๐ = (2nd โ๐) โ ๐ = ๐) |
11 | | id 22 |
. . . . . . . . 9
โข (๐ = (2nd โ๐) โ ๐ = (2nd โ๐)) |
12 | | eqidd 2738 |
. . . . . . . . 9
โข (๐ = (2nd โ๐) โ (๐ ฮฃg (๐ โ ๐ โฆ ((๐๐ฅ๐)(.rโ๐)(๐๐ฆ๐)))) = (๐ ฮฃg (๐ โ ๐ โฆ ((๐๐ฅ๐)(.rโ๐)(๐๐ฆ๐))))) |
13 | 10, 11, 12 | mpoeq123dv 7426 |
. . . . . . . 8
โข (๐ = (2nd โ๐) โ (๐ โ ๐, ๐ โ ๐ โฆ (๐ ฮฃg (๐ โ ๐ โฆ ((๐๐ฅ๐)(.rโ๐)(๐๐ฆ๐))))) = (๐ โ ๐, ๐ โ (2nd โ๐) โฆ (๐ ฮฃg (๐ โ ๐ โฆ ((๐๐ฅ๐)(.rโ๐)(๐๐ฆ๐)))))) |
14 | 7, 9, 13 | mpoeq123dv 7426 |
. . . . . . 7
โข (๐ = (2nd โ๐) โ (๐ฅ โ ((Baseโ๐) โm (๐ ร ๐)), ๐ฆ โ ((Baseโ๐) โm (๐ ร ๐)) โฆ (๐ โ ๐, ๐ โ ๐ โฆ (๐ ฮฃg (๐ โ ๐ โฆ ((๐๐ฅ๐)(.rโ๐)(๐๐ฆ๐)))))) = (๐ฅ โ ((Baseโ๐) โm (๐ ร ๐)), ๐ฆ โ ((Baseโ๐) โm (๐ ร (2nd โ๐))) โฆ (๐ โ ๐, ๐ โ (2nd โ๐) โฆ (๐ ฮฃg (๐ โ ๐ โฆ ((๐๐ฅ๐)(.rโ๐)(๐๐ฆ๐))))))) |
15 | 6, 14 | csbie 3889 |
. . . . . 6
โข
โฆ(2nd โ๐) / ๐โฆ(๐ฅ โ ((Baseโ๐) โm (๐ ร ๐)), ๐ฆ โ ((Baseโ๐) โm (๐ ร ๐)) โฆ (๐ โ ๐, ๐ โ ๐ โฆ (๐ ฮฃg (๐ โ ๐ โฆ ((๐๐ฅ๐)(.rโ๐)(๐๐ฆ๐)))))) = (๐ฅ โ ((Baseโ๐) โm (๐ ร ๐)), ๐ฆ โ ((Baseโ๐) โm (๐ ร (2nd โ๐))) โฆ (๐ โ ๐, ๐ โ (2nd โ๐) โฆ (๐ ฮฃg (๐ โ ๐ โฆ ((๐๐ฅ๐)(.rโ๐)(๐๐ฆ๐)))))) |
16 | | xpeq12 5656 |
. . . . . . . 8
โข ((๐ = (1st
โ(1st โ๐)) โง ๐ = (2nd โ(1st
โ๐))) โ (๐ ร ๐) = ((1st โ(1st
โ๐)) ร
(2nd โ(1st โ๐)))) |
17 | 16 | oveq2d 7367 |
. . . . . . 7
โข ((๐ = (1st
โ(1st โ๐)) โง ๐ = (2nd โ(1st
โ๐))) โ
((Baseโ๐)
โm (๐
ร ๐)) =
((Baseโ๐)
โm ((1st โ(1st โ๐)) ร (2nd
โ(1st โ๐))))) |
18 | | simpr 485 |
. . . . . . . . 9
โข ((๐ = (1st
โ(1st โ๐)) โง ๐ = (2nd โ(1st
โ๐))) โ ๐ = (2nd
โ(1st โ๐))) |
19 | 18 | xpeq1d 5660 |
. . . . . . . 8
โข ((๐ = (1st
โ(1st โ๐)) โง ๐ = (2nd โ(1st
โ๐))) โ (๐ ร (2nd
โ๐)) =
((2nd โ(1st โ๐)) ร (2nd โ๐))) |
20 | 19 | oveq2d 7367 |
. . . . . . 7
โข ((๐ = (1st
โ(1st โ๐)) โง ๐ = (2nd โ(1st
โ๐))) โ
((Baseโ๐)
โm (๐
ร (2nd โ๐))) = ((Baseโ๐) โm ((2nd
โ(1st โ๐)) ร (2nd โ๐)))) |
21 | | id 22 |
. . . . . . . . 9
โข (๐ = (1st
โ(1st โ๐)) โ ๐ = (1st โ(1st
โ๐))) |
22 | 21 | adantr 481 |
. . . . . . . 8
โข ((๐ = (1st
โ(1st โ๐)) โง ๐ = (2nd โ(1st
โ๐))) โ ๐ = (1st
โ(1st โ๐))) |
23 | | eqidd 2738 |
. . . . . . . 8
โข ((๐ = (1st
โ(1st โ๐)) โง ๐ = (2nd โ(1st
โ๐))) โ
(2nd โ๐) =
(2nd โ๐)) |
24 | | eqidd 2738 |
. . . . . . . . . 10
โข ((๐ = (1st
โ(1st โ๐)) โง ๐ = (2nd โ(1st
โ๐))) โ ((๐๐ฅ๐)(.rโ๐)(๐๐ฆ๐)) = ((๐๐ฅ๐)(.rโ๐)(๐๐ฆ๐))) |
25 | 18, 24 | mpteq12dv 5194 |
. . . . . . . . 9
โข ((๐ = (1st
โ(1st โ๐)) โง ๐ = (2nd โ(1st
โ๐))) โ (๐ โ ๐ โฆ ((๐๐ฅ๐)(.rโ๐)(๐๐ฆ๐))) = (๐ โ (2nd
โ(1st โ๐)) โฆ ((๐๐ฅ๐)(.rโ๐)(๐๐ฆ๐)))) |
26 | 25 | oveq2d 7367 |
. . . . . . . 8
โข ((๐ = (1st
โ(1st โ๐)) โง ๐ = (2nd โ(1st
โ๐))) โ (๐ ฮฃg
(๐ โ ๐ โฆ ((๐๐ฅ๐)(.rโ๐)(๐๐ฆ๐)))) = (๐ ฮฃg (๐ โ (2nd
โ(1st โ๐)) โฆ ((๐๐ฅ๐)(.rโ๐)(๐๐ฆ๐))))) |
27 | 22, 23, 26 | mpoeq123dv 7426 |
. . . . . . 7
โข ((๐ = (1st
โ(1st โ๐)) โง ๐ = (2nd โ(1st
โ๐))) โ (๐ โ ๐, ๐ โ (2nd โ๐) โฆ (๐ ฮฃg (๐ โ ๐ โฆ ((๐๐ฅ๐)(.rโ๐)(๐๐ฆ๐))))) = (๐ โ (1st
โ(1st โ๐)), ๐ โ (2nd โ๐) โฆ (๐ ฮฃg (๐ โ (2nd
โ(1st โ๐)) โฆ ((๐๐ฅ๐)(.rโ๐)(๐๐ฆ๐)))))) |
28 | 17, 20, 27 | mpoeq123dv 7426 |
. . . . . 6
โข ((๐ = (1st
โ(1st โ๐)) โง ๐ = (2nd โ(1st
โ๐))) โ (๐ฅ โ ((Baseโ๐) โm (๐ ร ๐)), ๐ฆ โ ((Baseโ๐) โm (๐ ร (2nd โ๐))) โฆ (๐ โ ๐, ๐ โ (2nd โ๐) โฆ (๐ ฮฃg (๐ โ ๐ โฆ ((๐๐ฅ๐)(.rโ๐)(๐๐ฆ๐)))))) = (๐ฅ โ ((Baseโ๐) โm ((1st
โ(1st โ๐)) ร (2nd
โ(1st โ๐)))), ๐ฆ โ ((Baseโ๐) โm ((2nd
โ(1st โ๐)) ร (2nd โ๐))) โฆ (๐ โ (1st
โ(1st โ๐)), ๐ โ (2nd โ๐) โฆ (๐ ฮฃg (๐ โ (2nd
โ(1st โ๐)) โฆ ((๐๐ฅ๐)(.rโ๐)(๐๐ฆ๐))))))) |
29 | 15, 28 | eqtrid 2789 |
. . . . 5
โข ((๐ = (1st
โ(1st โ๐)) โง ๐ = (2nd โ(1st
โ๐))) โ
โฆ(2nd โ๐) / ๐โฆ(๐ฅ โ ((Baseโ๐) โm (๐ ร ๐)), ๐ฆ โ ((Baseโ๐) โm (๐ ร ๐)) โฆ (๐ โ ๐, ๐ โ ๐ โฆ (๐ ฮฃg (๐ โ ๐ โฆ ((๐๐ฅ๐)(.rโ๐)(๐๐ฆ๐)))))) = (๐ฅ โ ((Baseโ๐) โm ((1st
โ(1st โ๐)) ร (2nd
โ(1st โ๐)))), ๐ฆ โ ((Baseโ๐) โm ((2nd
โ(1st โ๐)) ร (2nd โ๐))) โฆ (๐ โ (1st
โ(1st โ๐)), ๐ โ (2nd โ๐) โฆ (๐ ฮฃg (๐ โ (2nd
โ(1st โ๐)) โฆ ((๐๐ฅ๐)(.rโ๐)(๐๐ฆ๐))))))) |
30 | 4, 5, 29 | csbie2 3895 |
. . . 4
โข
โฆ(1st โ(1st โ๐)) / ๐โฆโฆ(2nd
โ(1st โ๐)) / ๐โฆโฆ(2nd
โ๐) / ๐โฆ(๐ฅ โ ((Baseโ๐) โm (๐ ร ๐)), ๐ฆ โ ((Baseโ๐) โm (๐ ร ๐)) โฆ (๐ โ ๐, ๐ โ ๐ โฆ (๐ ฮฃg (๐ โ ๐ โฆ ((๐๐ฅ๐)(.rโ๐)(๐๐ฆ๐)))))) = (๐ฅ โ ((Baseโ๐) โm ((1st
โ(1st โ๐)) ร (2nd
โ(1st โ๐)))), ๐ฆ โ ((Baseโ๐) โm ((2nd
โ(1st โ๐)) ร (2nd โ๐))) โฆ (๐ โ (1st
โ(1st โ๐)), ๐ โ (2nd โ๐) โฆ (๐ ฮฃg (๐ โ (2nd
โ(1st โ๐)) โฆ ((๐๐ฅ๐)(.rโ๐)(๐๐ฆ๐)))))) |
31 | | simprl 769 |
. . . . . . . 8
โข ((๐ โง (๐ = ๐
โง ๐ = โจ๐, ๐, ๐โฉ)) โ ๐ = ๐
) |
32 | 31 | fveq2d 6843 |
. . . . . . 7
โข ((๐ โง (๐ = ๐
โง ๐ = โจ๐, ๐, ๐โฉ)) โ (Baseโ๐) = (Baseโ๐
)) |
33 | | mamufval.b |
. . . . . . 7
โข ๐ต = (Baseโ๐
) |
34 | 32, 33 | eqtr4di 2795 |
. . . . . 6
โข ((๐ โง (๐ = ๐
โง ๐ = โจ๐, ๐, ๐โฉ)) โ (Baseโ๐) = ๐ต) |
35 | | fveq2 6839 |
. . . . . . . . . 10
โข (๐ = โจ๐, ๐, ๐โฉ โ (1st โ๐) = (1st
โโจ๐, ๐, ๐โฉ)) |
36 | 35 | fveq2d 6843 |
. . . . . . . . 9
โข (๐ = โจ๐, ๐, ๐โฉ โ (1st
โ(1st โ๐)) = (1st โ(1st
โโจ๐, ๐, ๐โฉ))) |
37 | 36 | ad2antll 727 |
. . . . . . . 8
โข ((๐ โง (๐ = ๐
โง ๐ = โจ๐, ๐, ๐โฉ)) โ (1st
โ(1st โ๐)) = (1st โ(1st
โโจ๐, ๐, ๐โฉ))) |
38 | | mamufval.m |
. . . . . . . . . 10
โข (๐ โ ๐ โ Fin) |
39 | | mamufval.n |
. . . . . . . . . 10
โข (๐ โ ๐ โ Fin) |
40 | | mamufval.p |
. . . . . . . . . 10
โข (๐ โ ๐ โ Fin) |
41 | | ot1stg 7927 |
. . . . . . . . . 10
โข ((๐ โ Fin โง ๐ โ Fin โง ๐ โ Fin) โ
(1st โ(1st โโจ๐, ๐, ๐โฉ)) = ๐) |
42 | 38, 39, 40, 41 | syl3anc 1371 |
. . . . . . . . 9
โข (๐ โ (1st
โ(1st โโจ๐, ๐, ๐โฉ)) = ๐) |
43 | 42 | adantr 481 |
. . . . . . . 8
โข ((๐ โง (๐ = ๐
โง ๐ = โจ๐, ๐, ๐โฉ)) โ (1st
โ(1st โโจ๐, ๐, ๐โฉ)) = ๐) |
44 | 37, 43 | eqtrd 2777 |
. . . . . . 7
โข ((๐ โง (๐ = ๐
โง ๐ = โจ๐, ๐, ๐โฉ)) โ (1st
โ(1st โ๐)) = ๐) |
45 | 35 | fveq2d 6843 |
. . . . . . . . 9
โข (๐ = โจ๐, ๐, ๐โฉ โ (2nd
โ(1st โ๐)) = (2nd โ(1st
โโจ๐, ๐, ๐โฉ))) |
46 | 45 | ad2antll 727 |
. . . . . . . 8
โข ((๐ โง (๐ = ๐
โง ๐ = โจ๐, ๐, ๐โฉ)) โ (2nd
โ(1st โ๐)) = (2nd โ(1st
โโจ๐, ๐, ๐โฉ))) |
47 | | ot2ndg 7928 |
. . . . . . . . . 10
โข ((๐ โ Fin โง ๐ โ Fin โง ๐ โ Fin) โ
(2nd โ(1st โโจ๐, ๐, ๐โฉ)) = ๐) |
48 | 38, 39, 40, 47 | syl3anc 1371 |
. . . . . . . . 9
โข (๐ โ (2nd
โ(1st โโจ๐, ๐, ๐โฉ)) = ๐) |
49 | 48 | adantr 481 |
. . . . . . . 8
โข ((๐ โง (๐ = ๐
โง ๐ = โจ๐, ๐, ๐โฉ)) โ (2nd
โ(1st โโจ๐, ๐, ๐โฉ)) = ๐) |
50 | 46, 49 | eqtrd 2777 |
. . . . . . 7
โข ((๐ โง (๐ = ๐
โง ๐ = โจ๐, ๐, ๐โฉ)) โ (2nd
โ(1st โ๐)) = ๐) |
51 | 44, 50 | xpeq12d 5662 |
. . . . . 6
โข ((๐ โง (๐ = ๐
โง ๐ = โจ๐, ๐, ๐โฉ)) โ ((1st
โ(1st โ๐)) ร (2nd
โ(1st โ๐))) = (๐ ร ๐)) |
52 | 34, 51 | oveq12d 7369 |
. . . . 5
โข ((๐ โง (๐ = ๐
โง ๐ = โจ๐, ๐, ๐โฉ)) โ ((Baseโ๐) โm
((1st โ(1st โ๐)) ร (2nd
โ(1st โ๐)))) = (๐ต โm (๐ ร ๐))) |
53 | | fveq2 6839 |
. . . . . . . . 9
โข (๐ = โจ๐, ๐, ๐โฉ โ (2nd โ๐) = (2nd
โโจ๐, ๐, ๐โฉ)) |
54 | 53 | ad2antll 727 |
. . . . . . . 8
โข ((๐ โง (๐ = ๐
โง ๐ = โจ๐, ๐, ๐โฉ)) โ (2nd โ๐) = (2nd
โโจ๐, ๐, ๐โฉ)) |
55 | | ot3rdg 7929 |
. . . . . . . . . 10
โข (๐ โ Fin โ
(2nd โโจ๐, ๐, ๐โฉ) = ๐) |
56 | 40, 55 | syl 17 |
. . . . . . . . 9
โข (๐ โ (2nd
โโจ๐, ๐, ๐โฉ) = ๐) |
57 | 56 | adantr 481 |
. . . . . . . 8
โข ((๐ โง (๐ = ๐
โง ๐ = โจ๐, ๐, ๐โฉ)) โ (2nd
โโจ๐, ๐, ๐โฉ) = ๐) |
58 | 54, 57 | eqtrd 2777 |
. . . . . . 7
โข ((๐ โง (๐ = ๐
โง ๐ = โจ๐, ๐, ๐โฉ)) โ (2nd โ๐) = ๐) |
59 | 50, 58 | xpeq12d 5662 |
. . . . . 6
โข ((๐ โง (๐ = ๐
โง ๐ = โจ๐, ๐, ๐โฉ)) โ ((2nd
โ(1st โ๐)) ร (2nd โ๐)) = (๐ ร ๐)) |
60 | 34, 59 | oveq12d 7369 |
. . . . 5
โข ((๐ โง (๐ = ๐
โง ๐ = โจ๐, ๐, ๐โฉ)) โ ((Baseโ๐) โm
((2nd โ(1st โ๐)) ร (2nd โ๐))) = (๐ต โm (๐ ร ๐))) |
61 | 31 | fveq2d 6843 |
. . . . . . . . . 10
โข ((๐ โง (๐ = ๐
โง ๐ = โจ๐, ๐, ๐โฉ)) โ (.rโ๐) = (.rโ๐
)) |
62 | | mamufval.t |
. . . . . . . . . 10
โข ยท =
(.rโ๐
) |
63 | 61, 62 | eqtr4di 2795 |
. . . . . . . . 9
โข ((๐ โง (๐ = ๐
โง ๐ = โจ๐, ๐, ๐โฉ)) โ (.rโ๐) = ยท ) |
64 | 63 | oveqd 7368 |
. . . . . . . 8
โข ((๐ โง (๐ = ๐
โง ๐ = โจ๐, ๐, ๐โฉ)) โ ((๐๐ฅ๐)(.rโ๐)(๐๐ฆ๐)) = ((๐๐ฅ๐) ยท (๐๐ฆ๐))) |
65 | 50, 64 | mpteq12dv 5194 |
. . . . . . 7
โข ((๐ โง (๐ = ๐
โง ๐ = โจ๐, ๐, ๐โฉ)) โ (๐ โ (2nd
โ(1st โ๐)) โฆ ((๐๐ฅ๐)(.rโ๐)(๐๐ฆ๐))) = (๐ โ ๐ โฆ ((๐๐ฅ๐) ยท (๐๐ฆ๐)))) |
66 | 31, 65 | oveq12d 7369 |
. . . . . 6
โข ((๐ โง (๐ = ๐
โง ๐ = โจ๐, ๐, ๐โฉ)) โ (๐ ฮฃg (๐ โ (2nd
โ(1st โ๐)) โฆ ((๐๐ฅ๐)(.rโ๐)(๐๐ฆ๐)))) = (๐
ฮฃg (๐ โ ๐ โฆ ((๐๐ฅ๐) ยท (๐๐ฆ๐))))) |
67 | 44, 58, 66 | mpoeq123dv 7426 |
. . . . 5
โข ((๐ โง (๐ = ๐
โง ๐ = โจ๐, ๐, ๐โฉ)) โ (๐ โ (1st
โ(1st โ๐)), ๐ โ (2nd โ๐) โฆ (๐ ฮฃg (๐ โ (2nd
โ(1st โ๐)) โฆ ((๐๐ฅ๐)(.rโ๐)(๐๐ฆ๐))))) = (๐ โ ๐, ๐ โ ๐ โฆ (๐
ฮฃg (๐ โ ๐ โฆ ((๐๐ฅ๐) ยท (๐๐ฆ๐)))))) |
68 | 52, 60, 67 | mpoeq123dv 7426 |
. . . 4
โข ((๐ โง (๐ = ๐
โง ๐ = โจ๐, ๐, ๐โฉ)) โ (๐ฅ โ ((Baseโ๐) โm ((1st
โ(1st โ๐)) ร (2nd
โ(1st โ๐)))), ๐ฆ โ ((Baseโ๐) โm ((2nd
โ(1st โ๐)) ร (2nd โ๐))) โฆ (๐ โ (1st
โ(1st โ๐)), ๐ โ (2nd โ๐) โฆ (๐ ฮฃg (๐ โ (2nd
โ(1st โ๐)) โฆ ((๐๐ฅ๐)(.rโ๐)(๐๐ฆ๐)))))) = (๐ฅ โ (๐ต โm (๐ ร ๐)), ๐ฆ โ (๐ต โm (๐ ร ๐)) โฆ (๐ โ ๐, ๐ โ ๐ โฆ (๐
ฮฃg (๐ โ ๐ โฆ ((๐๐ฅ๐) ยท (๐๐ฆ๐))))))) |
69 | 30, 68 | eqtrid 2789 |
. . 3
โข ((๐ โง (๐ = ๐
โง ๐ = โจ๐, ๐, ๐โฉ)) โ
โฆ(1st โ(1st โ๐)) / ๐โฆโฆ(2nd
โ(1st โ๐)) / ๐โฆโฆ(2nd
โ๐) / ๐โฆ(๐ฅ โ ((Baseโ๐) โm (๐ ร ๐)), ๐ฆ โ ((Baseโ๐) โm (๐ ร ๐)) โฆ (๐ โ ๐, ๐ โ ๐ โฆ (๐ ฮฃg (๐ โ ๐ โฆ ((๐๐ฅ๐)(.rโ๐)(๐๐ฆ๐)))))) = (๐ฅ โ (๐ต โm (๐ ร ๐)), ๐ฆ โ (๐ต โm (๐ ร ๐)) โฆ (๐ โ ๐, ๐ โ ๐ โฆ (๐
ฮฃg (๐ โ ๐ โฆ ((๐๐ฅ๐) ยท (๐๐ฆ๐))))))) |
70 | | mamufval.r |
. . . 4
โข (๐ โ ๐
โ ๐) |
71 | 70 | elexd 3463 |
. . 3
โข (๐ โ ๐
โ V) |
72 | | otex 5420 |
. . . 4
โข
โจ๐, ๐, ๐โฉ โ V |
73 | 72 | a1i 11 |
. . 3
โข (๐ โ โจ๐, ๐, ๐โฉ โ V) |
74 | | ovex 7384 |
. . . . 5
โข (๐ต โm (๐ ร ๐)) โ V |
75 | | ovex 7384 |
. . . . 5
โข (๐ต โm (๐ ร ๐)) โ V |
76 | 74, 75 | mpoex 8004 |
. . . 4
โข (๐ฅ โ (๐ต โm (๐ ร ๐)), ๐ฆ โ (๐ต โm (๐ ร ๐)) โฆ (๐ โ ๐, ๐ โ ๐ โฆ (๐
ฮฃg (๐ โ ๐ โฆ ((๐๐ฅ๐) ยท (๐๐ฆ๐)))))) โ V |
77 | 76 | a1i 11 |
. . 3
โข (๐ โ (๐ฅ โ (๐ต โm (๐ ร ๐)), ๐ฆ โ (๐ต โm (๐ ร ๐)) โฆ (๐ โ ๐, ๐ โ ๐ โฆ (๐
ฮฃg (๐ โ ๐ โฆ ((๐๐ฅ๐) ยท (๐๐ฆ๐)))))) โ V) |
78 | 3, 69, 71, 73, 77 | ovmpod 7501 |
. 2
โข (๐ โ (๐
maMul โจ๐, ๐, ๐โฉ) = (๐ฅ โ (๐ต โm (๐ ร ๐)), ๐ฆ โ (๐ต โm (๐ ร ๐)) โฆ (๐ โ ๐, ๐ โ ๐ โฆ (๐
ฮฃg (๐ โ ๐ โฆ ((๐๐ฅ๐) ยท (๐๐ฆ๐))))))) |
79 | 1, 78 | eqtrid 2789 |
1
โข (๐ โ ๐น = (๐ฅ โ (๐ต โm (๐ ร ๐)), ๐ฆ โ (๐ต โm (๐ ร ๐)) โฆ (๐ โ ๐, ๐ โ ๐ โฆ (๐
ฮฃg (๐ โ ๐ โฆ ((๐๐ฅ๐) ยท (๐๐ฆ๐))))))) |