Step | Hyp | Ref
| Expression |
1 | | simp2 1138 |
. . . . . . 7
โข ((๐ โง ๐ฅ โ ๐ผ โง ๐ฆ โ ๐ฝ) โ ๐ฅ โ ๐ผ) |
2 | | evlslem4.x |
. . . . . . . 8
โข ((๐ โง ๐ฅ โ ๐ผ) โ ๐ โ ๐ต) |
3 | 2 | 3adant3 1133 |
. . . . . . 7
โข ((๐ โง ๐ฅ โ ๐ผ โง ๐ฆ โ ๐ฝ) โ ๐ โ ๐ต) |
4 | | eqid 2733 |
. . . . . . . 8
โข (๐ฅ โ ๐ผ โฆ ๐) = (๐ฅ โ ๐ผ โฆ ๐) |
5 | 4 | fvmpt2 7010 |
. . . . . . 7
โข ((๐ฅ โ ๐ผ โง ๐ โ ๐ต) โ ((๐ฅ โ ๐ผ โฆ ๐)โ๐ฅ) = ๐) |
6 | 1, 3, 5 | syl2anc 585 |
. . . . . 6
โข ((๐ โง ๐ฅ โ ๐ผ โง ๐ฆ โ ๐ฝ) โ ((๐ฅ โ ๐ผ โฆ ๐)โ๐ฅ) = ๐) |
7 | | simp3 1139 |
. . . . . . 7
โข ((๐ โง ๐ฅ โ ๐ผ โง ๐ฆ โ ๐ฝ) โ ๐ฆ โ ๐ฝ) |
8 | | evlslem4.y |
. . . . . . 7
โข ((๐ โง ๐ฆ โ ๐ฝ) โ ๐ โ ๐ต) |
9 | | eqid 2733 |
. . . . . . . 8
โข (๐ฆ โ ๐ฝ โฆ ๐) = (๐ฆ โ ๐ฝ โฆ ๐) |
10 | 9 | fvmpt2 7010 |
. . . . . . 7
โข ((๐ฆ โ ๐ฝ โง ๐ โ ๐ต) โ ((๐ฆ โ ๐ฝ โฆ ๐)โ๐ฆ) = ๐) |
11 | 7, 8, 10 | 3imp3i2an 1346 |
. . . . . 6
โข ((๐ โง ๐ฅ โ ๐ผ โง ๐ฆ โ ๐ฝ) โ ((๐ฆ โ ๐ฝ โฆ ๐)โ๐ฆ) = ๐) |
12 | 6, 11 | oveq12d 7427 |
. . . . 5
โข ((๐ โง ๐ฅ โ ๐ผ โง ๐ฆ โ ๐ฝ) โ (((๐ฅ โ ๐ผ โฆ ๐)โ๐ฅ) ยท ((๐ฆ โ ๐ฝ โฆ ๐)โ๐ฆ)) = (๐ ยท ๐)) |
13 | 12 | mpoeq3dva 7486 |
. . . 4
โข (๐ โ (๐ฅ โ ๐ผ, ๐ฆ โ ๐ฝ โฆ (((๐ฅ โ ๐ผ โฆ ๐)โ๐ฅ) ยท ((๐ฆ โ ๐ฝ โฆ ๐)โ๐ฆ))) = (๐ฅ โ ๐ผ, ๐ฆ โ ๐ฝ โฆ (๐ ยท ๐))) |
14 | | nfcv 2904 |
. . . . . 6
โข
โฒ๐(((๐ฅ โ ๐ผ โฆ ๐)โ๐ฅ) ยท ((๐ฆ โ ๐ฝ โฆ ๐)โ๐ฆ)) |
15 | | nfcv 2904 |
. . . . . 6
โข
โฒ๐(((๐ฅ โ ๐ผ โฆ ๐)โ๐ฅ) ยท ((๐ฆ โ ๐ฝ โฆ ๐)โ๐ฆ)) |
16 | | nffvmpt1 6903 |
. . . . . . 7
โข
โฒ๐ฅ((๐ฅ โ ๐ผ โฆ ๐)โ๐) |
17 | | nfcv 2904 |
. . . . . . 7
โข
โฒ๐ฅ
ยท |
18 | | nfcv 2904 |
. . . . . . 7
โข
โฒ๐ฅ((๐ฆ โ ๐ฝ โฆ ๐)โ๐) |
19 | 16, 17, 18 | nfov 7439 |
. . . . . 6
โข
โฒ๐ฅ(((๐ฅ โ ๐ผ โฆ ๐)โ๐) ยท ((๐ฆ โ ๐ฝ โฆ ๐)โ๐)) |
20 | | nfcv 2904 |
. . . . . . 7
โข
โฒ๐ฆ((๐ฅ โ ๐ผ โฆ ๐)โ๐) |
21 | | nfcv 2904 |
. . . . . . 7
โข
โฒ๐ฆ
ยท |
22 | | nffvmpt1 6903 |
. . . . . . 7
โข
โฒ๐ฆ((๐ฆ โ ๐ฝ โฆ ๐)โ๐) |
23 | 20, 21, 22 | nfov 7439 |
. . . . . 6
โข
โฒ๐ฆ(((๐ฅ โ ๐ผ โฆ ๐)โ๐) ยท ((๐ฆ โ ๐ฝ โฆ ๐)โ๐)) |
24 | | fveq2 6892 |
. . . . . . 7
โข (๐ฅ = ๐ โ ((๐ฅ โ ๐ผ โฆ ๐)โ๐ฅ) = ((๐ฅ โ ๐ผ โฆ ๐)โ๐)) |
25 | | fveq2 6892 |
. . . . . . 7
โข (๐ฆ = ๐ โ ((๐ฆ โ ๐ฝ โฆ ๐)โ๐ฆ) = ((๐ฆ โ ๐ฝ โฆ ๐)โ๐)) |
26 | 24, 25 | oveqan12d 7428 |
. . . . . 6
โข ((๐ฅ = ๐ โง ๐ฆ = ๐) โ (((๐ฅ โ ๐ผ โฆ ๐)โ๐ฅ) ยท ((๐ฆ โ ๐ฝ โฆ ๐)โ๐ฆ)) = (((๐ฅ โ ๐ผ โฆ ๐)โ๐) ยท ((๐ฆ โ ๐ฝ โฆ ๐)โ๐))) |
27 | 14, 15, 19, 23, 26 | cbvmpo 7503 |
. . . . 5
โข (๐ฅ โ ๐ผ, ๐ฆ โ ๐ฝ โฆ (((๐ฅ โ ๐ผ โฆ ๐)โ๐ฅ) ยท ((๐ฆ โ ๐ฝ โฆ ๐)โ๐ฆ))) = (๐ โ ๐ผ, ๐ โ ๐ฝ โฆ (((๐ฅ โ ๐ผ โฆ ๐)โ๐) ยท ((๐ฆ โ ๐ฝ โฆ ๐)โ๐))) |
28 | | vex 3479 |
. . . . . . . 8
โข ๐ โ V |
29 | | vex 3479 |
. . . . . . . 8
โข ๐ โ V |
30 | 28, 29 | eqop2 8018 |
. . . . . . 7
โข (๐ง = โจ๐, ๐โฉ โ (๐ง โ (V ร V) โง ((1st
โ๐ง) = ๐ โง (2nd
โ๐ง) = ๐))) |
31 | | fveq2 6892 |
. . . . . . . 8
โข
((1st โ๐ง) = ๐ โ ((๐ฅ โ ๐ผ โฆ ๐)โ(1st โ๐ง)) = ((๐ฅ โ ๐ผ โฆ ๐)โ๐)) |
32 | | fveq2 6892 |
. . . . . . . 8
โข
((2nd โ๐ง) = ๐ โ ((๐ฆ โ ๐ฝ โฆ ๐)โ(2nd โ๐ง)) = ((๐ฆ โ ๐ฝ โฆ ๐)โ๐)) |
33 | 31, 32 | oveqan12d 7428 |
. . . . . . 7
โข
(((1st โ๐ง) = ๐ โง (2nd โ๐ง) = ๐) โ (((๐ฅ โ ๐ผ โฆ ๐)โ(1st โ๐ง)) ยท ((๐ฆ โ ๐ฝ โฆ ๐)โ(2nd โ๐ง))) = (((๐ฅ โ ๐ผ โฆ ๐)โ๐) ยท ((๐ฆ โ ๐ฝ โฆ ๐)โ๐))) |
34 | 30, 33 | simplbiim 506 |
. . . . . 6
โข (๐ง = โจ๐, ๐โฉ โ (((๐ฅ โ ๐ผ โฆ ๐)โ(1st โ๐ง)) ยท ((๐ฆ โ ๐ฝ โฆ ๐)โ(2nd โ๐ง))) = (((๐ฅ โ ๐ผ โฆ ๐)โ๐) ยท ((๐ฆ โ ๐ฝ โฆ ๐)โ๐))) |
35 | 34 | mpompt 7522 |
. . . . 5
โข (๐ง โ (๐ผ ร ๐ฝ) โฆ (((๐ฅ โ ๐ผ โฆ ๐)โ(1st โ๐ง)) ยท ((๐ฆ โ ๐ฝ โฆ ๐)โ(2nd โ๐ง)))) = (๐ โ ๐ผ, ๐ โ ๐ฝ โฆ (((๐ฅ โ ๐ผ โฆ ๐)โ๐) ยท ((๐ฆ โ ๐ฝ โฆ ๐)โ๐))) |
36 | 27, 35 | eqtr4i 2764 |
. . . 4
โข (๐ฅ โ ๐ผ, ๐ฆ โ ๐ฝ โฆ (((๐ฅ โ ๐ผ โฆ ๐)โ๐ฅ) ยท ((๐ฆ โ ๐ฝ โฆ ๐)โ๐ฆ))) = (๐ง โ (๐ผ ร ๐ฝ) โฆ (((๐ฅ โ ๐ผ โฆ ๐)โ(1st โ๐ง)) ยท ((๐ฆ โ ๐ฝ โฆ ๐)โ(2nd โ๐ง)))) |
37 | 13, 36 | eqtr3di 2788 |
. . 3
โข (๐ โ (๐ฅ โ ๐ผ, ๐ฆ โ ๐ฝ โฆ (๐ ยท ๐)) = (๐ง โ (๐ผ ร ๐ฝ) โฆ (((๐ฅ โ ๐ผ โฆ ๐)โ(1st โ๐ง)) ยท ((๐ฆ โ ๐ฝ โฆ ๐)โ(2nd โ๐ง))))) |
38 | 37 | oveq1d 7424 |
. 2
โข (๐ โ ((๐ฅ โ ๐ผ, ๐ฆ โ ๐ฝ โฆ (๐ ยท ๐)) supp 0 ) = ((๐ง โ (๐ผ ร ๐ฝ) โฆ (((๐ฅ โ ๐ผ โฆ ๐)โ(1st โ๐ง)) ยท ((๐ฆ โ ๐ฝ โฆ ๐)โ(2nd โ๐ง)))) supp 0 )) |
39 | | difxp 6164 |
. . . . . 6
โข ((๐ผ ร ๐ฝ) โ (((๐ฅ โ ๐ผ โฆ ๐) supp 0 ) ร ((๐ฆ โ ๐ฝ โฆ ๐) supp 0 ))) = (((๐ผ โ ((๐ฅ โ ๐ผ โฆ ๐) supp 0 )) ร ๐ฝ) โช (๐ผ ร (๐ฝ โ ((๐ฆ โ ๐ฝ โฆ ๐) supp 0 )))) |
40 | 39 | eleq2i 2826 |
. . . . 5
โข (๐ง โ ((๐ผ ร ๐ฝ) โ (((๐ฅ โ ๐ผ โฆ ๐) supp 0 ) ร ((๐ฆ โ ๐ฝ โฆ ๐) supp 0 ))) โ ๐ง โ (((๐ผ โ ((๐ฅ โ ๐ผ โฆ ๐) supp 0 )) ร ๐ฝ) โช (๐ผ ร (๐ฝ โ ((๐ฆ โ ๐ฝ โฆ ๐) supp 0 ))))) |
41 | | elun 4149 |
. . . . 5
โข (๐ง โ (((๐ผ โ ((๐ฅ โ ๐ผ โฆ ๐) supp 0 )) ร ๐ฝ) โช (๐ผ ร (๐ฝ โ ((๐ฆ โ ๐ฝ โฆ ๐) supp 0 )))) โ (๐ง โ ((๐ผ โ ((๐ฅ โ ๐ผ โฆ ๐) supp 0 )) ร ๐ฝ) โจ ๐ง โ (๐ผ ร (๐ฝ โ ((๐ฆ โ ๐ฝ โฆ ๐) supp 0 ))))) |
42 | 40, 41 | bitri 275 |
. . . 4
โข (๐ง โ ((๐ผ ร ๐ฝ) โ (((๐ฅ โ ๐ผ โฆ ๐) supp 0 ) ร ((๐ฆ โ ๐ฝ โฆ ๐) supp 0 ))) โ (๐ง โ ((๐ผ โ ((๐ฅ โ ๐ผ โฆ ๐) supp 0 )) ร ๐ฝ) โจ ๐ง โ (๐ผ ร (๐ฝ โ ((๐ฆ โ ๐ฝ โฆ ๐) supp 0 ))))) |
43 | | xp1st 8007 |
. . . . . . . 8
โข (๐ง โ ((๐ผ โ ((๐ฅ โ ๐ผ โฆ ๐) supp 0 )) ร ๐ฝ) โ (1st
โ๐ง) โ (๐ผ โ ((๐ฅ โ ๐ผ โฆ ๐) supp 0 ))) |
44 | 2 | fmpttd 7115 |
. . . . . . . . 9
โข (๐ โ (๐ฅ โ ๐ผ โฆ ๐):๐ผโถ๐ต) |
45 | | ssidd 4006 |
. . . . . . . . 9
โข (๐ โ ((๐ฅ โ ๐ผ โฆ ๐) supp 0 ) โ ((๐ฅ โ ๐ผ โฆ ๐) supp 0 )) |
46 | | evlslem4.i |
. . . . . . . . 9
โข (๐ โ ๐ผ โ ๐) |
47 | | evlslem4.z |
. . . . . . . . . . 11
โข 0 =
(0gโ๐
) |
48 | 47 | fvexi 6906 |
. . . . . . . . . 10
โข 0 โ
V |
49 | 48 | a1i 11 |
. . . . . . . . 9
โข (๐ โ 0 โ V) |
50 | 44, 45, 46, 49 | suppssr 8181 |
. . . . . . . 8
โข ((๐ โง (1st
โ๐ง) โ (๐ผ โ ((๐ฅ โ ๐ผ โฆ ๐) supp 0 ))) โ ((๐ฅ โ ๐ผ โฆ ๐)โ(1st โ๐ง)) = 0 ) |
51 | 43, 50 | sylan2 594 |
. . . . . . 7
โข ((๐ โง ๐ง โ ((๐ผ โ ((๐ฅ โ ๐ผ โฆ ๐) supp 0 )) ร ๐ฝ)) โ ((๐ฅ โ ๐ผ โฆ ๐)โ(1st โ๐ง)) = 0 ) |
52 | 51 | oveq1d 7424 |
. . . . . 6
โข ((๐ โง ๐ง โ ((๐ผ โ ((๐ฅ โ ๐ผ โฆ ๐) supp 0 )) ร ๐ฝ)) โ (((๐ฅ โ ๐ผ โฆ ๐)โ(1st โ๐ง)) ยท ((๐ฆ โ ๐ฝ โฆ ๐)โ(2nd โ๐ง))) = ( 0 ยท ((๐ฆ โ ๐ฝ โฆ ๐)โ(2nd โ๐ง)))) |
53 | | evlslem4.r |
. . . . . . 7
โข (๐ โ ๐
โ Ring) |
54 | 8 | fmpttd 7115 |
. . . . . . . 8
โข (๐ โ (๐ฆ โ ๐ฝ โฆ ๐):๐ฝโถ๐ต) |
55 | | xp2nd 8008 |
. . . . . . . 8
โข (๐ง โ ((๐ผ โ ((๐ฅ โ ๐ผ โฆ ๐) supp 0 )) ร ๐ฝ) โ (2nd
โ๐ง) โ ๐ฝ) |
56 | | ffvelcdm 7084 |
. . . . . . . 8
โข (((๐ฆ โ ๐ฝ โฆ ๐):๐ฝโถ๐ต โง (2nd โ๐ง) โ ๐ฝ) โ ((๐ฆ โ ๐ฝ โฆ ๐)โ(2nd โ๐ง)) โ ๐ต) |
57 | 54, 55, 56 | syl2an 597 |
. . . . . . 7
โข ((๐ โง ๐ง โ ((๐ผ โ ((๐ฅ โ ๐ผ โฆ ๐) supp 0 )) ร ๐ฝ)) โ ((๐ฆ โ ๐ฝ โฆ ๐)โ(2nd โ๐ง)) โ ๐ต) |
58 | | evlslem4.b |
. . . . . . . 8
โข ๐ต = (Baseโ๐
) |
59 | | evlslem4.t |
. . . . . . . 8
โข ยท =
(.rโ๐
) |
60 | 58, 59, 47 | ringlz 20107 |
. . . . . . 7
โข ((๐
โ Ring โง ((๐ฆ โ ๐ฝ โฆ ๐)โ(2nd โ๐ง)) โ ๐ต) โ ( 0 ยท ((๐ฆ โ ๐ฝ โฆ ๐)โ(2nd โ๐ง))) = 0 ) |
61 | 53, 57, 60 | syl2an2r 684 |
. . . . . 6
โข ((๐ โง ๐ง โ ((๐ผ โ ((๐ฅ โ ๐ผ โฆ ๐) supp 0 )) ร ๐ฝ)) โ ( 0 ยท ((๐ฆ โ ๐ฝ โฆ ๐)โ(2nd โ๐ง))) = 0 ) |
62 | 52, 61 | eqtrd 2773 |
. . . . 5
โข ((๐ โง ๐ง โ ((๐ผ โ ((๐ฅ โ ๐ผ โฆ ๐) supp 0 )) ร ๐ฝ)) โ (((๐ฅ โ ๐ผ โฆ ๐)โ(1st โ๐ง)) ยท ((๐ฆ โ ๐ฝ โฆ ๐)โ(2nd โ๐ง))) = 0 ) |
63 | | xp2nd 8008 |
. . . . . . . 8
โข (๐ง โ (๐ผ ร (๐ฝ โ ((๐ฆ โ ๐ฝ โฆ ๐) supp 0 ))) โ (2nd
โ๐ง) โ (๐ฝ โ ((๐ฆ โ ๐ฝ โฆ ๐) supp 0 ))) |
64 | | ssidd 4006 |
. . . . . . . . 9
โข (๐ โ ((๐ฆ โ ๐ฝ โฆ ๐) supp 0 ) โ ((๐ฆ โ ๐ฝ โฆ ๐) supp 0 )) |
65 | | evlslem4.j |
. . . . . . . . 9
โข (๐ โ ๐ฝ โ ๐) |
66 | 54, 64, 65, 49 | suppssr 8181 |
. . . . . . . 8
โข ((๐ โง (2nd
โ๐ง) โ (๐ฝ โ ((๐ฆ โ ๐ฝ โฆ ๐) supp 0 ))) โ ((๐ฆ โ ๐ฝ โฆ ๐)โ(2nd โ๐ง)) = 0 ) |
67 | 63, 66 | sylan2 594 |
. . . . . . 7
โข ((๐ โง ๐ง โ (๐ผ ร (๐ฝ โ ((๐ฆ โ ๐ฝ โฆ ๐) supp 0 )))) โ ((๐ฆ โ ๐ฝ โฆ ๐)โ(2nd โ๐ง)) = 0 ) |
68 | 67 | oveq2d 7425 |
. . . . . 6
โข ((๐ โง ๐ง โ (๐ผ ร (๐ฝ โ ((๐ฆ โ ๐ฝ โฆ ๐) supp 0 )))) โ (((๐ฅ โ ๐ผ โฆ ๐)โ(1st โ๐ง)) ยท ((๐ฆ โ ๐ฝ โฆ ๐)โ(2nd โ๐ง))) = (((๐ฅ โ ๐ผ โฆ ๐)โ(1st โ๐ง)) ยท 0 )) |
69 | | xp1st 8007 |
. . . . . . . 8
โข (๐ง โ (๐ผ ร (๐ฝ โ ((๐ฆ โ ๐ฝ โฆ ๐) supp 0 ))) โ (1st
โ๐ง) โ ๐ผ) |
70 | | ffvelcdm 7084 |
. . . . . . . 8
โข (((๐ฅ โ ๐ผ โฆ ๐):๐ผโถ๐ต โง (1st โ๐ง) โ ๐ผ) โ ((๐ฅ โ ๐ผ โฆ ๐)โ(1st โ๐ง)) โ ๐ต) |
71 | 44, 69, 70 | syl2an 597 |
. . . . . . 7
โข ((๐ โง ๐ง โ (๐ผ ร (๐ฝ โ ((๐ฆ โ ๐ฝ โฆ ๐) supp 0 )))) โ ((๐ฅ โ ๐ผ โฆ ๐)โ(1st โ๐ง)) โ ๐ต) |
72 | 58, 59, 47 | ringrz 20108 |
. . . . . . 7
โข ((๐
โ Ring โง ((๐ฅ โ ๐ผ โฆ ๐)โ(1st โ๐ง)) โ ๐ต) โ (((๐ฅ โ ๐ผ โฆ ๐)โ(1st โ๐ง)) ยท 0 ) = 0 ) |
73 | 53, 71, 72 | syl2an2r 684 |
. . . . . 6
โข ((๐ โง ๐ง โ (๐ผ ร (๐ฝ โ ((๐ฆ โ ๐ฝ โฆ ๐) supp 0 )))) โ (((๐ฅ โ ๐ผ โฆ ๐)โ(1st โ๐ง)) ยท 0 ) = 0 ) |
74 | 68, 73 | eqtrd 2773 |
. . . . 5
โข ((๐ โง ๐ง โ (๐ผ ร (๐ฝ โ ((๐ฆ โ ๐ฝ โฆ ๐) supp 0 )))) โ (((๐ฅ โ ๐ผ โฆ ๐)โ(1st โ๐ง)) ยท ((๐ฆ โ ๐ฝ โฆ ๐)โ(2nd โ๐ง))) = 0 ) |
75 | 62, 74 | jaodan 957 |
. . . 4
โข ((๐ โง (๐ง โ ((๐ผ โ ((๐ฅ โ ๐ผ โฆ ๐) supp 0 )) ร ๐ฝ) โจ ๐ง โ (๐ผ ร (๐ฝ โ ((๐ฆ โ ๐ฝ โฆ ๐) supp 0 ))))) โ (((๐ฅ โ ๐ผ โฆ ๐)โ(1st โ๐ง)) ยท ((๐ฆ โ ๐ฝ โฆ ๐)โ(2nd โ๐ง))) = 0 ) |
76 | 42, 75 | sylan2b 595 |
. . 3
โข ((๐ โง ๐ง โ ((๐ผ ร ๐ฝ) โ (((๐ฅ โ ๐ผ โฆ ๐) supp 0 ) ร ((๐ฆ โ ๐ฝ โฆ ๐) supp 0 )))) โ (((๐ฅ โ ๐ผ โฆ ๐)โ(1st โ๐ง)) ยท ((๐ฆ โ ๐ฝ โฆ ๐)โ(2nd โ๐ง))) = 0 ) |
77 | 46, 65 | xpexd 7738 |
. . 3
โข (๐ โ (๐ผ ร ๐ฝ) โ V) |
78 | 76, 77 | suppss2 8185 |
. 2
โข (๐ โ ((๐ง โ (๐ผ ร ๐ฝ) โฆ (((๐ฅ โ ๐ผ โฆ ๐)โ(1st โ๐ง)) ยท ((๐ฆ โ ๐ฝ โฆ ๐)โ(2nd โ๐ง)))) supp 0 ) โ (((๐ฅ โ ๐ผ โฆ ๐) supp 0 ) ร ((๐ฆ โ ๐ฝ โฆ ๐) supp 0 ))) |
79 | 38, 78 | eqsstrd 4021 |
1
โข (๐ โ ((๐ฅ โ ๐ผ, ๐ฆ โ ๐ฝ โฆ (๐ ยท ๐)) supp 0 ) โ (((๐ฅ โ ๐ผ โฆ ๐) supp 0 ) ร ((๐ฆ โ ๐ฝ โฆ ๐) supp 0 ))) |