Step |
Hyp |
Ref |
Expression |
1 |
|
mdetuni.a |
โข ๐ด = ( ๐ Mat ๐
) |
2 |
|
mdetuni.b |
โข ๐ต = ( Base โ ๐ด ) |
3 |
|
mdetuni.k |
โข ๐พ = ( Base โ ๐
) |
4 |
|
mdetuni.0g |
โข 0 = ( 0g โ ๐
) |
5 |
|
mdetuni.1r |
โข 1 = ( 1r โ ๐
) |
6 |
|
mdetuni.pg |
โข + = ( +g โ ๐
) |
7 |
|
mdetuni.tg |
โข ยท = ( .r โ ๐
) |
8 |
|
mdetuni.n |
โข ( ๐ โ ๐ โ Fin ) |
9 |
|
mdetuni.r |
โข ( ๐ โ ๐
โ Ring ) |
10 |
|
mdetuni.ff |
โข ( ๐ โ ๐ท : ๐ต โถ ๐พ ) |
11 |
|
mdetuni.al |
โข ( ๐ โ โ ๐ฅ โ ๐ต โ ๐ฆ โ ๐ โ ๐ง โ ๐ ( ( ๐ฆ โ ๐ง โง โ ๐ค โ ๐ ( ๐ฆ ๐ฅ ๐ค ) = ( ๐ง ๐ฅ ๐ค ) ) โ ( ๐ท โ ๐ฅ ) = 0 ) ) |
12 |
|
mdetuni.li |
โข ( ๐ โ โ ๐ฅ โ ๐ต โ ๐ฆ โ ๐ต โ ๐ง โ ๐ต โ ๐ค โ ๐ ( ( ( ๐ฅ โพ ( { ๐ค } ร ๐ ) ) = ( ( ๐ฆ โพ ( { ๐ค } ร ๐ ) ) โf + ( ๐ง โพ ( { ๐ค } ร ๐ ) ) ) โง ( ๐ฅ โพ ( ( ๐ โ { ๐ค } ) ร ๐ ) ) = ( ๐ฆ โพ ( ( ๐ โ { ๐ค } ) ร ๐ ) ) โง ( ๐ฅ โพ ( ( ๐ โ { ๐ค } ) ร ๐ ) ) = ( ๐ง โพ ( ( ๐ โ { ๐ค } ) ร ๐ ) ) ) โ ( ๐ท โ ๐ฅ ) = ( ( ๐ท โ ๐ฆ ) + ( ๐ท โ ๐ง ) ) ) ) |
13 |
|
mdetuni.sc |
โข ( ๐ โ โ ๐ฅ โ ๐ต โ ๐ฆ โ ๐พ โ ๐ง โ ๐ต โ ๐ค โ ๐ ( ( ( ๐ฅ โพ ( { ๐ค } ร ๐ ) ) = ( ( ( { ๐ค } ร ๐ ) ร { ๐ฆ } ) โf ยท ( ๐ง โพ ( { ๐ค } ร ๐ ) ) ) โง ( ๐ฅ โพ ( ( ๐ โ { ๐ค } ) ร ๐ ) ) = ( ๐ง โพ ( ( ๐ โ { ๐ค } ) ร ๐ ) ) ) โ ( ๐ท โ ๐ฅ ) = ( ๐ฆ ยท ( ๐ท โ ๐ง ) ) ) ) |
14 |
|
simp32 |
โข ( ( ๐ โง ( ๐ธ โ ๐ต โง ๐น โ ๐พ โง ๐บ โ ๐ต ) โง ( ๐ป โ ๐ โง ( ๐ธ โพ ( { ๐ป } ร ๐ ) ) = ( ( ( { ๐ป } ร ๐ ) ร { ๐น } ) โf ยท ( ๐บ โพ ( { ๐ป } ร ๐ ) ) ) โง ( ๐ธ โพ ( ( ๐ โ { ๐ป } ) ร ๐ ) ) = ( ๐บ โพ ( ( ๐ โ { ๐ป } ) ร ๐ ) ) ) ) โ ( ๐ธ โพ ( { ๐ป } ร ๐ ) ) = ( ( ( { ๐ป } ร ๐ ) ร { ๐น } ) โf ยท ( ๐บ โพ ( { ๐ป } ร ๐ ) ) ) ) |
15 |
|
simp33 |
โข ( ( ๐ โง ( ๐ธ โ ๐ต โง ๐น โ ๐พ โง ๐บ โ ๐ต ) โง ( ๐ป โ ๐ โง ( ๐ธ โพ ( { ๐ป } ร ๐ ) ) = ( ( ( { ๐ป } ร ๐ ) ร { ๐น } ) โf ยท ( ๐บ โพ ( { ๐ป } ร ๐ ) ) ) โง ( ๐ธ โพ ( ( ๐ โ { ๐ป } ) ร ๐ ) ) = ( ๐บ โพ ( ( ๐ โ { ๐ป } ) ร ๐ ) ) ) ) โ ( ๐ธ โพ ( ( ๐ โ { ๐ป } ) ร ๐ ) ) = ( ๐บ โพ ( ( ๐ โ { ๐ป } ) ร ๐ ) ) ) |
16 |
|
simp1 |
โข ( ( ๐ป โ ๐ โง ( ๐ธ โพ ( { ๐ป } ร ๐ ) ) = ( ( ( { ๐ป } ร ๐ ) ร { ๐น } ) โf ยท ( ๐บ โพ ( { ๐ป } ร ๐ ) ) ) โง ( ๐ธ โพ ( ( ๐ โ { ๐ป } ) ร ๐ ) ) = ( ๐บ โพ ( ( ๐ โ { ๐ป } ) ร ๐ ) ) ) โ ๐ป โ ๐ ) |
17 |
|
simp23 |
โข ( ( ๐ โง ( ๐ธ โ ๐ต โง ๐น โ ๐พ โง ๐บ โ ๐ต ) โง ๐ป โ ๐ ) โ ๐บ โ ๐ต ) |
18 |
|
simp3 |
โข ( ( ๐ โง ( ๐ธ โ ๐ต โง ๐น โ ๐พ โง ๐บ โ ๐ต ) โง ๐ป โ ๐ ) โ ๐ป โ ๐ ) |
19 |
|
simp21 |
โข ( ( ๐ โง ( ๐ธ โ ๐ต โง ๐น โ ๐พ โง ๐บ โ ๐ต ) โง ๐ป โ ๐ ) โ ๐ธ โ ๐ต ) |
20 |
|
simp22 |
โข ( ( ๐ โง ( ๐ธ โ ๐ต โง ๐น โ ๐พ โง ๐บ โ ๐ต ) โง ๐ป โ ๐ ) โ ๐น โ ๐พ ) |
21 |
13
|
3ad2ant1 |
โข ( ( ๐ โง ( ๐ธ โ ๐ต โง ๐น โ ๐พ โง ๐บ โ ๐ต ) โง ๐ป โ ๐ ) โ โ ๐ฅ โ ๐ต โ ๐ฆ โ ๐พ โ ๐ง โ ๐ต โ ๐ค โ ๐ ( ( ( ๐ฅ โพ ( { ๐ค } ร ๐ ) ) = ( ( ( { ๐ค } ร ๐ ) ร { ๐ฆ } ) โf ยท ( ๐ง โพ ( { ๐ค } ร ๐ ) ) ) โง ( ๐ฅ โพ ( ( ๐ โ { ๐ค } ) ร ๐ ) ) = ( ๐ง โพ ( ( ๐ โ { ๐ค } ) ร ๐ ) ) ) โ ( ๐ท โ ๐ฅ ) = ( ๐ฆ ยท ( ๐ท โ ๐ง ) ) ) ) |
22 |
|
reseq1 |
โข ( ๐ฅ = ๐ธ โ ( ๐ฅ โพ ( { ๐ค } ร ๐ ) ) = ( ๐ธ โพ ( { ๐ค } ร ๐ ) ) ) |
23 |
22
|
eqeq1d |
โข ( ๐ฅ = ๐ธ โ ( ( ๐ฅ โพ ( { ๐ค } ร ๐ ) ) = ( ( ( { ๐ค } ร ๐ ) ร { ๐ฆ } ) โf ยท ( ๐ง โพ ( { ๐ค } ร ๐ ) ) ) โ ( ๐ธ โพ ( { ๐ค } ร ๐ ) ) = ( ( ( { ๐ค } ร ๐ ) ร { ๐ฆ } ) โf ยท ( ๐ง โพ ( { ๐ค } ร ๐ ) ) ) ) ) |
24 |
|
reseq1 |
โข ( ๐ฅ = ๐ธ โ ( ๐ฅ โพ ( ( ๐ โ { ๐ค } ) ร ๐ ) ) = ( ๐ธ โพ ( ( ๐ โ { ๐ค } ) ร ๐ ) ) ) |
25 |
24
|
eqeq1d |
โข ( ๐ฅ = ๐ธ โ ( ( ๐ฅ โพ ( ( ๐ โ { ๐ค } ) ร ๐ ) ) = ( ๐ง โพ ( ( ๐ โ { ๐ค } ) ร ๐ ) ) โ ( ๐ธ โพ ( ( ๐ โ { ๐ค } ) ร ๐ ) ) = ( ๐ง โพ ( ( ๐ โ { ๐ค } ) ร ๐ ) ) ) ) |
26 |
23 25
|
anbi12d |
โข ( ๐ฅ = ๐ธ โ ( ( ( ๐ฅ โพ ( { ๐ค } ร ๐ ) ) = ( ( ( { ๐ค } ร ๐ ) ร { ๐ฆ } ) โf ยท ( ๐ง โพ ( { ๐ค } ร ๐ ) ) ) โง ( ๐ฅ โพ ( ( ๐ โ { ๐ค } ) ร ๐ ) ) = ( ๐ง โพ ( ( ๐ โ { ๐ค } ) ร ๐ ) ) ) โ ( ( ๐ธ โพ ( { ๐ค } ร ๐ ) ) = ( ( ( { ๐ค } ร ๐ ) ร { ๐ฆ } ) โf ยท ( ๐ง โพ ( { ๐ค } ร ๐ ) ) ) โง ( ๐ธ โพ ( ( ๐ โ { ๐ค } ) ร ๐ ) ) = ( ๐ง โพ ( ( ๐ โ { ๐ค } ) ร ๐ ) ) ) ) ) |
27 |
|
fveqeq2 |
โข ( ๐ฅ = ๐ธ โ ( ( ๐ท โ ๐ฅ ) = ( ๐ฆ ยท ( ๐ท โ ๐ง ) ) โ ( ๐ท โ ๐ธ ) = ( ๐ฆ ยท ( ๐ท โ ๐ง ) ) ) ) |
28 |
26 27
|
imbi12d |
โข ( ๐ฅ = ๐ธ โ ( ( ( ( ๐ฅ โพ ( { ๐ค } ร ๐ ) ) = ( ( ( { ๐ค } ร ๐ ) ร { ๐ฆ } ) โf ยท ( ๐ง โพ ( { ๐ค } ร ๐ ) ) ) โง ( ๐ฅ โพ ( ( ๐ โ { ๐ค } ) ร ๐ ) ) = ( ๐ง โพ ( ( ๐ โ { ๐ค } ) ร ๐ ) ) ) โ ( ๐ท โ ๐ฅ ) = ( ๐ฆ ยท ( ๐ท โ ๐ง ) ) ) โ ( ( ( ๐ธ โพ ( { ๐ค } ร ๐ ) ) = ( ( ( { ๐ค } ร ๐ ) ร { ๐ฆ } ) โf ยท ( ๐ง โพ ( { ๐ค } ร ๐ ) ) ) โง ( ๐ธ โพ ( ( ๐ โ { ๐ค } ) ร ๐ ) ) = ( ๐ง โพ ( ( ๐ โ { ๐ค } ) ร ๐ ) ) ) โ ( ๐ท โ ๐ธ ) = ( ๐ฆ ยท ( ๐ท โ ๐ง ) ) ) ) ) |
29 |
28
|
2ralbidv |
โข ( ๐ฅ = ๐ธ โ ( โ ๐ง โ ๐ต โ ๐ค โ ๐ ( ( ( ๐ฅ โพ ( { ๐ค } ร ๐ ) ) = ( ( ( { ๐ค } ร ๐ ) ร { ๐ฆ } ) โf ยท ( ๐ง โพ ( { ๐ค } ร ๐ ) ) ) โง ( ๐ฅ โพ ( ( ๐ โ { ๐ค } ) ร ๐ ) ) = ( ๐ง โพ ( ( ๐ โ { ๐ค } ) ร ๐ ) ) ) โ ( ๐ท โ ๐ฅ ) = ( ๐ฆ ยท ( ๐ท โ ๐ง ) ) ) โ โ ๐ง โ ๐ต โ ๐ค โ ๐ ( ( ( ๐ธ โพ ( { ๐ค } ร ๐ ) ) = ( ( ( { ๐ค } ร ๐ ) ร { ๐ฆ } ) โf ยท ( ๐ง โพ ( { ๐ค } ร ๐ ) ) ) โง ( ๐ธ โพ ( ( ๐ โ { ๐ค } ) ร ๐ ) ) = ( ๐ง โพ ( ( ๐ โ { ๐ค } ) ร ๐ ) ) ) โ ( ๐ท โ ๐ธ ) = ( ๐ฆ ยท ( ๐ท โ ๐ง ) ) ) ) ) |
30 |
|
sneq |
โข ( ๐ฆ = ๐น โ { ๐ฆ } = { ๐น } ) |
31 |
30
|
xpeq2d |
โข ( ๐ฆ = ๐น โ ( ( { ๐ค } ร ๐ ) ร { ๐ฆ } ) = ( ( { ๐ค } ร ๐ ) ร { ๐น } ) ) |
32 |
31
|
oveq1d |
โข ( ๐ฆ = ๐น โ ( ( ( { ๐ค } ร ๐ ) ร { ๐ฆ } ) โf ยท ( ๐ง โพ ( { ๐ค } ร ๐ ) ) ) = ( ( ( { ๐ค } ร ๐ ) ร { ๐น } ) โf ยท ( ๐ง โพ ( { ๐ค } ร ๐ ) ) ) ) |
33 |
32
|
eqeq2d |
โข ( ๐ฆ = ๐น โ ( ( ๐ธ โพ ( { ๐ค } ร ๐ ) ) = ( ( ( { ๐ค } ร ๐ ) ร { ๐ฆ } ) โf ยท ( ๐ง โพ ( { ๐ค } ร ๐ ) ) ) โ ( ๐ธ โพ ( { ๐ค } ร ๐ ) ) = ( ( ( { ๐ค } ร ๐ ) ร { ๐น } ) โf ยท ( ๐ง โพ ( { ๐ค } ร ๐ ) ) ) ) ) |
34 |
33
|
anbi1d |
โข ( ๐ฆ = ๐น โ ( ( ( ๐ธ โพ ( { ๐ค } ร ๐ ) ) = ( ( ( { ๐ค } ร ๐ ) ร { ๐ฆ } ) โf ยท ( ๐ง โพ ( { ๐ค } ร ๐ ) ) ) โง ( ๐ธ โพ ( ( ๐ โ { ๐ค } ) ร ๐ ) ) = ( ๐ง โพ ( ( ๐ โ { ๐ค } ) ร ๐ ) ) ) โ ( ( ๐ธ โพ ( { ๐ค } ร ๐ ) ) = ( ( ( { ๐ค } ร ๐ ) ร { ๐น } ) โf ยท ( ๐ง โพ ( { ๐ค } ร ๐ ) ) ) โง ( ๐ธ โพ ( ( ๐ โ { ๐ค } ) ร ๐ ) ) = ( ๐ง โพ ( ( ๐ โ { ๐ค } ) ร ๐ ) ) ) ) ) |
35 |
|
oveq1 |
โข ( ๐ฆ = ๐น โ ( ๐ฆ ยท ( ๐ท โ ๐ง ) ) = ( ๐น ยท ( ๐ท โ ๐ง ) ) ) |
36 |
35
|
eqeq2d |
โข ( ๐ฆ = ๐น โ ( ( ๐ท โ ๐ธ ) = ( ๐ฆ ยท ( ๐ท โ ๐ง ) ) โ ( ๐ท โ ๐ธ ) = ( ๐น ยท ( ๐ท โ ๐ง ) ) ) ) |
37 |
34 36
|
imbi12d |
โข ( ๐ฆ = ๐น โ ( ( ( ( ๐ธ โพ ( { ๐ค } ร ๐ ) ) = ( ( ( { ๐ค } ร ๐ ) ร { ๐ฆ } ) โf ยท ( ๐ง โพ ( { ๐ค } ร ๐ ) ) ) โง ( ๐ธ โพ ( ( ๐ โ { ๐ค } ) ร ๐ ) ) = ( ๐ง โพ ( ( ๐ โ { ๐ค } ) ร ๐ ) ) ) โ ( ๐ท โ ๐ธ ) = ( ๐ฆ ยท ( ๐ท โ ๐ง ) ) ) โ ( ( ( ๐ธ โพ ( { ๐ค } ร ๐ ) ) = ( ( ( { ๐ค } ร ๐ ) ร { ๐น } ) โf ยท ( ๐ง โพ ( { ๐ค } ร ๐ ) ) ) โง ( ๐ธ โพ ( ( ๐ โ { ๐ค } ) ร ๐ ) ) = ( ๐ง โพ ( ( ๐ โ { ๐ค } ) ร ๐ ) ) ) โ ( ๐ท โ ๐ธ ) = ( ๐น ยท ( ๐ท โ ๐ง ) ) ) ) ) |
38 |
37
|
2ralbidv |
โข ( ๐ฆ = ๐น โ ( โ ๐ง โ ๐ต โ ๐ค โ ๐ ( ( ( ๐ธ โพ ( { ๐ค } ร ๐ ) ) = ( ( ( { ๐ค } ร ๐ ) ร { ๐ฆ } ) โf ยท ( ๐ง โพ ( { ๐ค } ร ๐ ) ) ) โง ( ๐ธ โพ ( ( ๐ โ { ๐ค } ) ร ๐ ) ) = ( ๐ง โพ ( ( ๐ โ { ๐ค } ) ร ๐ ) ) ) โ ( ๐ท โ ๐ธ ) = ( ๐ฆ ยท ( ๐ท โ ๐ง ) ) ) โ โ ๐ง โ ๐ต โ ๐ค โ ๐ ( ( ( ๐ธ โพ ( { ๐ค } ร ๐ ) ) = ( ( ( { ๐ค } ร ๐ ) ร { ๐น } ) โf ยท ( ๐ง โพ ( { ๐ค } ร ๐ ) ) ) โง ( ๐ธ โพ ( ( ๐ โ { ๐ค } ) ร ๐ ) ) = ( ๐ง โพ ( ( ๐ โ { ๐ค } ) ร ๐ ) ) ) โ ( ๐ท โ ๐ธ ) = ( ๐น ยท ( ๐ท โ ๐ง ) ) ) ) ) |
39 |
29 38
|
rspc2va |
โข ( ( ( ๐ธ โ ๐ต โง ๐น โ ๐พ ) โง โ ๐ฅ โ ๐ต โ ๐ฆ โ ๐พ โ ๐ง โ ๐ต โ ๐ค โ ๐ ( ( ( ๐ฅ โพ ( { ๐ค } ร ๐ ) ) = ( ( ( { ๐ค } ร ๐ ) ร { ๐ฆ } ) โf ยท ( ๐ง โพ ( { ๐ค } ร ๐ ) ) ) โง ( ๐ฅ โพ ( ( ๐ โ { ๐ค } ) ร ๐ ) ) = ( ๐ง โพ ( ( ๐ โ { ๐ค } ) ร ๐ ) ) ) โ ( ๐ท โ ๐ฅ ) = ( ๐ฆ ยท ( ๐ท โ ๐ง ) ) ) ) โ โ ๐ง โ ๐ต โ ๐ค โ ๐ ( ( ( ๐ธ โพ ( { ๐ค } ร ๐ ) ) = ( ( ( { ๐ค } ร ๐ ) ร { ๐น } ) โf ยท ( ๐ง โพ ( { ๐ค } ร ๐ ) ) ) โง ( ๐ธ โพ ( ( ๐ โ { ๐ค } ) ร ๐ ) ) = ( ๐ง โพ ( ( ๐ โ { ๐ค } ) ร ๐ ) ) ) โ ( ๐ท โ ๐ธ ) = ( ๐น ยท ( ๐ท โ ๐ง ) ) ) ) |
40 |
19 20 21 39
|
syl21anc |
โข ( ( ๐ โง ( ๐ธ โ ๐ต โง ๐น โ ๐พ โง ๐บ โ ๐ต ) โง ๐ป โ ๐ ) โ โ ๐ง โ ๐ต โ ๐ค โ ๐ ( ( ( ๐ธ โพ ( { ๐ค } ร ๐ ) ) = ( ( ( { ๐ค } ร ๐ ) ร { ๐น } ) โf ยท ( ๐ง โพ ( { ๐ค } ร ๐ ) ) ) โง ( ๐ธ โพ ( ( ๐ โ { ๐ค } ) ร ๐ ) ) = ( ๐ง โพ ( ( ๐ โ { ๐ค } ) ร ๐ ) ) ) โ ( ๐ท โ ๐ธ ) = ( ๐น ยท ( ๐ท โ ๐ง ) ) ) ) |
41 |
|
reseq1 |
โข ( ๐ง = ๐บ โ ( ๐ง โพ ( { ๐ค } ร ๐ ) ) = ( ๐บ โพ ( { ๐ค } ร ๐ ) ) ) |
42 |
41
|
oveq2d |
โข ( ๐ง = ๐บ โ ( ( ( { ๐ค } ร ๐ ) ร { ๐น } ) โf ยท ( ๐ง โพ ( { ๐ค } ร ๐ ) ) ) = ( ( ( { ๐ค } ร ๐ ) ร { ๐น } ) โf ยท ( ๐บ โพ ( { ๐ค } ร ๐ ) ) ) ) |
43 |
42
|
eqeq2d |
โข ( ๐ง = ๐บ โ ( ( ๐ธ โพ ( { ๐ค } ร ๐ ) ) = ( ( ( { ๐ค } ร ๐ ) ร { ๐น } ) โf ยท ( ๐ง โพ ( { ๐ค } ร ๐ ) ) ) โ ( ๐ธ โพ ( { ๐ค } ร ๐ ) ) = ( ( ( { ๐ค } ร ๐ ) ร { ๐น } ) โf ยท ( ๐บ โพ ( { ๐ค } ร ๐ ) ) ) ) ) |
44 |
|
reseq1 |
โข ( ๐ง = ๐บ โ ( ๐ง โพ ( ( ๐ โ { ๐ค } ) ร ๐ ) ) = ( ๐บ โพ ( ( ๐ โ { ๐ค } ) ร ๐ ) ) ) |
45 |
44
|
eqeq2d |
โข ( ๐ง = ๐บ โ ( ( ๐ธ โพ ( ( ๐ โ { ๐ค } ) ร ๐ ) ) = ( ๐ง โพ ( ( ๐ โ { ๐ค } ) ร ๐ ) ) โ ( ๐ธ โพ ( ( ๐ โ { ๐ค } ) ร ๐ ) ) = ( ๐บ โพ ( ( ๐ โ { ๐ค } ) ร ๐ ) ) ) ) |
46 |
43 45
|
anbi12d |
โข ( ๐ง = ๐บ โ ( ( ( ๐ธ โพ ( { ๐ค } ร ๐ ) ) = ( ( ( { ๐ค } ร ๐ ) ร { ๐น } ) โf ยท ( ๐ง โพ ( { ๐ค } ร ๐ ) ) ) โง ( ๐ธ โพ ( ( ๐ โ { ๐ค } ) ร ๐ ) ) = ( ๐ง โพ ( ( ๐ โ { ๐ค } ) ร ๐ ) ) ) โ ( ( ๐ธ โพ ( { ๐ค } ร ๐ ) ) = ( ( ( { ๐ค } ร ๐ ) ร { ๐น } ) โf ยท ( ๐บ โพ ( { ๐ค } ร ๐ ) ) ) โง ( ๐ธ โพ ( ( ๐ โ { ๐ค } ) ร ๐ ) ) = ( ๐บ โพ ( ( ๐ โ { ๐ค } ) ร ๐ ) ) ) ) ) |
47 |
|
fveq2 |
โข ( ๐ง = ๐บ โ ( ๐ท โ ๐ง ) = ( ๐ท โ ๐บ ) ) |
48 |
47
|
oveq2d |
โข ( ๐ง = ๐บ โ ( ๐น ยท ( ๐ท โ ๐ง ) ) = ( ๐น ยท ( ๐ท โ ๐บ ) ) ) |
49 |
48
|
eqeq2d |
โข ( ๐ง = ๐บ โ ( ( ๐ท โ ๐ธ ) = ( ๐น ยท ( ๐ท โ ๐ง ) ) โ ( ๐ท โ ๐ธ ) = ( ๐น ยท ( ๐ท โ ๐บ ) ) ) ) |
50 |
46 49
|
imbi12d |
โข ( ๐ง = ๐บ โ ( ( ( ( ๐ธ โพ ( { ๐ค } ร ๐ ) ) = ( ( ( { ๐ค } ร ๐ ) ร { ๐น } ) โf ยท ( ๐ง โพ ( { ๐ค } ร ๐ ) ) ) โง ( ๐ธ โพ ( ( ๐ โ { ๐ค } ) ร ๐ ) ) = ( ๐ง โพ ( ( ๐ โ { ๐ค } ) ร ๐ ) ) ) โ ( ๐ท โ ๐ธ ) = ( ๐น ยท ( ๐ท โ ๐ง ) ) ) โ ( ( ( ๐ธ โพ ( { ๐ค } ร ๐ ) ) = ( ( ( { ๐ค } ร ๐ ) ร { ๐น } ) โf ยท ( ๐บ โพ ( { ๐ค } ร ๐ ) ) ) โง ( ๐ธ โพ ( ( ๐ โ { ๐ค } ) ร ๐ ) ) = ( ๐บ โพ ( ( ๐ โ { ๐ค } ) ร ๐ ) ) ) โ ( ๐ท โ ๐ธ ) = ( ๐น ยท ( ๐ท โ ๐บ ) ) ) ) ) |
51 |
|
sneq |
โข ( ๐ค = ๐ป โ { ๐ค } = { ๐ป } ) |
52 |
51
|
xpeq1d |
โข ( ๐ค = ๐ป โ ( { ๐ค } ร ๐ ) = ( { ๐ป } ร ๐ ) ) |
53 |
52
|
reseq2d |
โข ( ๐ค = ๐ป โ ( ๐ธ โพ ( { ๐ค } ร ๐ ) ) = ( ๐ธ โพ ( { ๐ป } ร ๐ ) ) ) |
54 |
52
|
xpeq1d |
โข ( ๐ค = ๐ป โ ( ( { ๐ค } ร ๐ ) ร { ๐น } ) = ( ( { ๐ป } ร ๐ ) ร { ๐น } ) ) |
55 |
52
|
reseq2d |
โข ( ๐ค = ๐ป โ ( ๐บ โพ ( { ๐ค } ร ๐ ) ) = ( ๐บ โพ ( { ๐ป } ร ๐ ) ) ) |
56 |
54 55
|
oveq12d |
โข ( ๐ค = ๐ป โ ( ( ( { ๐ค } ร ๐ ) ร { ๐น } ) โf ยท ( ๐บ โพ ( { ๐ค } ร ๐ ) ) ) = ( ( ( { ๐ป } ร ๐ ) ร { ๐น } ) โf ยท ( ๐บ โพ ( { ๐ป } ร ๐ ) ) ) ) |
57 |
53 56
|
eqeq12d |
โข ( ๐ค = ๐ป โ ( ( ๐ธ โพ ( { ๐ค } ร ๐ ) ) = ( ( ( { ๐ค } ร ๐ ) ร { ๐น } ) โf ยท ( ๐บ โพ ( { ๐ค } ร ๐ ) ) ) โ ( ๐ธ โพ ( { ๐ป } ร ๐ ) ) = ( ( ( { ๐ป } ร ๐ ) ร { ๐น } ) โf ยท ( ๐บ โพ ( { ๐ป } ร ๐ ) ) ) ) ) |
58 |
51
|
difeq2d |
โข ( ๐ค = ๐ป โ ( ๐ โ { ๐ค } ) = ( ๐ โ { ๐ป } ) ) |
59 |
58
|
xpeq1d |
โข ( ๐ค = ๐ป โ ( ( ๐ โ { ๐ค } ) ร ๐ ) = ( ( ๐ โ { ๐ป } ) ร ๐ ) ) |
60 |
59
|
reseq2d |
โข ( ๐ค = ๐ป โ ( ๐ธ โพ ( ( ๐ โ { ๐ค } ) ร ๐ ) ) = ( ๐ธ โพ ( ( ๐ โ { ๐ป } ) ร ๐ ) ) ) |
61 |
59
|
reseq2d |
โข ( ๐ค = ๐ป โ ( ๐บ โพ ( ( ๐ โ { ๐ค } ) ร ๐ ) ) = ( ๐บ โพ ( ( ๐ โ { ๐ป } ) ร ๐ ) ) ) |
62 |
60 61
|
eqeq12d |
โข ( ๐ค = ๐ป โ ( ( ๐ธ โพ ( ( ๐ โ { ๐ค } ) ร ๐ ) ) = ( ๐บ โพ ( ( ๐ โ { ๐ค } ) ร ๐ ) ) โ ( ๐ธ โพ ( ( ๐ โ { ๐ป } ) ร ๐ ) ) = ( ๐บ โพ ( ( ๐ โ { ๐ป } ) ร ๐ ) ) ) ) |
63 |
57 62
|
anbi12d |
โข ( ๐ค = ๐ป โ ( ( ( ๐ธ โพ ( { ๐ค } ร ๐ ) ) = ( ( ( { ๐ค } ร ๐ ) ร { ๐น } ) โf ยท ( ๐บ โพ ( { ๐ค } ร ๐ ) ) ) โง ( ๐ธ โพ ( ( ๐ โ { ๐ค } ) ร ๐ ) ) = ( ๐บ โพ ( ( ๐ โ { ๐ค } ) ร ๐ ) ) ) โ ( ( ๐ธ โพ ( { ๐ป } ร ๐ ) ) = ( ( ( { ๐ป } ร ๐ ) ร { ๐น } ) โf ยท ( ๐บ โพ ( { ๐ป } ร ๐ ) ) ) โง ( ๐ธ โพ ( ( ๐ โ { ๐ป } ) ร ๐ ) ) = ( ๐บ โพ ( ( ๐ โ { ๐ป } ) ร ๐ ) ) ) ) ) |
64 |
63
|
imbi1d |
โข ( ๐ค = ๐ป โ ( ( ( ( ๐ธ โพ ( { ๐ค } ร ๐ ) ) = ( ( ( { ๐ค } ร ๐ ) ร { ๐น } ) โf ยท ( ๐บ โพ ( { ๐ค } ร ๐ ) ) ) โง ( ๐ธ โพ ( ( ๐ โ { ๐ค } ) ร ๐ ) ) = ( ๐บ โพ ( ( ๐ โ { ๐ค } ) ร ๐ ) ) ) โ ( ๐ท โ ๐ธ ) = ( ๐น ยท ( ๐ท โ ๐บ ) ) ) โ ( ( ( ๐ธ โพ ( { ๐ป } ร ๐ ) ) = ( ( ( { ๐ป } ร ๐ ) ร { ๐น } ) โf ยท ( ๐บ โพ ( { ๐ป } ร ๐ ) ) ) โง ( ๐ธ โพ ( ( ๐ โ { ๐ป } ) ร ๐ ) ) = ( ๐บ โพ ( ( ๐ โ { ๐ป } ) ร ๐ ) ) ) โ ( ๐ท โ ๐ธ ) = ( ๐น ยท ( ๐ท โ ๐บ ) ) ) ) ) |
65 |
50 64
|
rspc2va |
โข ( ( ( ๐บ โ ๐ต โง ๐ป โ ๐ ) โง โ ๐ง โ ๐ต โ ๐ค โ ๐ ( ( ( ๐ธ โพ ( { ๐ค } ร ๐ ) ) = ( ( ( { ๐ค } ร ๐ ) ร { ๐น } ) โf ยท ( ๐ง โพ ( { ๐ค } ร ๐ ) ) ) โง ( ๐ธ โพ ( ( ๐ โ { ๐ค } ) ร ๐ ) ) = ( ๐ง โพ ( ( ๐ โ { ๐ค } ) ร ๐ ) ) ) โ ( ๐ท โ ๐ธ ) = ( ๐น ยท ( ๐ท โ ๐ง ) ) ) ) โ ( ( ( ๐ธ โพ ( { ๐ป } ร ๐ ) ) = ( ( ( { ๐ป } ร ๐ ) ร { ๐น } ) โf ยท ( ๐บ โพ ( { ๐ป } ร ๐ ) ) ) โง ( ๐ธ โพ ( ( ๐ โ { ๐ป } ) ร ๐ ) ) = ( ๐บ โพ ( ( ๐ โ { ๐ป } ) ร ๐ ) ) ) โ ( ๐ท โ ๐ธ ) = ( ๐น ยท ( ๐ท โ ๐บ ) ) ) ) |
66 |
17 18 40 65
|
syl21anc |
โข ( ( ๐ โง ( ๐ธ โ ๐ต โง ๐น โ ๐พ โง ๐บ โ ๐ต ) โง ๐ป โ ๐ ) โ ( ( ( ๐ธ โพ ( { ๐ป } ร ๐ ) ) = ( ( ( { ๐ป } ร ๐ ) ร { ๐น } ) โf ยท ( ๐บ โพ ( { ๐ป } ร ๐ ) ) ) โง ( ๐ธ โพ ( ( ๐ โ { ๐ป } ) ร ๐ ) ) = ( ๐บ โพ ( ( ๐ โ { ๐ป } ) ร ๐ ) ) ) โ ( ๐ท โ ๐ธ ) = ( ๐น ยท ( ๐ท โ ๐บ ) ) ) ) |
67 |
16 66
|
syl3an3 |
โข ( ( ๐ โง ( ๐ธ โ ๐ต โง ๐น โ ๐พ โง ๐บ โ ๐ต ) โง ( ๐ป โ ๐ โง ( ๐ธ โพ ( { ๐ป } ร ๐ ) ) = ( ( ( { ๐ป } ร ๐ ) ร { ๐น } ) โf ยท ( ๐บ โพ ( { ๐ป } ร ๐ ) ) ) โง ( ๐ธ โพ ( ( ๐ โ { ๐ป } ) ร ๐ ) ) = ( ๐บ โพ ( ( ๐ โ { ๐ป } ) ร ๐ ) ) ) ) โ ( ( ( ๐ธ โพ ( { ๐ป } ร ๐ ) ) = ( ( ( { ๐ป } ร ๐ ) ร { ๐น } ) โf ยท ( ๐บ โพ ( { ๐ป } ร ๐ ) ) ) โง ( ๐ธ โพ ( ( ๐ โ { ๐ป } ) ร ๐ ) ) = ( ๐บ โพ ( ( ๐ โ { ๐ป } ) ร ๐ ) ) ) โ ( ๐ท โ ๐ธ ) = ( ๐น ยท ( ๐ท โ ๐บ ) ) ) ) |
68 |
14 15 67
|
mp2and |
โข ( ( ๐ โง ( ๐ธ โ ๐ต โง ๐น โ ๐พ โง ๐บ โ ๐ต ) โง ( ๐ป โ ๐ โง ( ๐ธ โพ ( { ๐ป } ร ๐ ) ) = ( ( ( { ๐ป } ร ๐ ) ร { ๐น } ) โf ยท ( ๐บ โพ ( { ๐ป } ร ๐ ) ) ) โง ( ๐ธ โพ ( ( ๐ โ { ๐ป } ) ร ๐ ) ) = ( ๐บ โพ ( ( ๐ โ { ๐ป } ) ร ๐ ) ) ) ) โ ( ๐ท โ ๐ธ ) = ( ๐น ยท ( ๐ท โ ๐บ ) ) ) |