Step Hyp Ref
Expression 1 dfcnqs 9540 . 2
2 mulcnsrec 9542 . 2
3 mulcnsrec 9542 . 2
4 mulcnsrec 9542 . 2
5 mulcnsrec 9542 . 2
6 mulclsr 9482 . . . . 5
7 m1r 9480 . . . . . 6
8 mulclsr 9482 . . . . . 6
9 mulclsr 9482 . . . . . 6
10 7 , 8 , 9 sylancr 663 . . . . 5
11 addclsr 9481 . . . . 5
12 6 , 10 , 11 syl2an 477 . . . 4
13 12 an4s 826 . . 3
14 mulclsr 9482 . . . . 5
15 mulclsr 9482 . . . . 5
16 addclsr 9481 . . . . 5
17 14 , 15 , 16 syl2anr 478 . . . 4
18 17 an42s 827 . . 3
19 13 , 18 jca 532 . 2
20 mulclsr 9482 . . . . 5
21 mulclsr 9482 . . . . . 6
22 mulclsr 9482 . . . . . 6
23 7 , 21 , 22 sylancr 663 . . . . 5
24 addclsr 9481 . . . . 5
25 20 , 23 , 24 syl2an 477 . . . 4
26 25 an4s 826 . . 3
27 mulclsr 9482 . . . . 5
28 mulclsr 9482 . . . . 5
29 addclsr 9481 . . . . 5
30 27 , 28 , 29 syl2anr 478 . . . 4
31 30 an42s 827 . . 3
32 26 , 31 jca 532 . 2
33 ovex 6324 . . . 4
34 ovex 6324 . . . 4
35 ovex 6324 . . . 4
36 addcomsr 9485 . . . 4
37 addasssr 9486 . . . 4
38 ovex 6324 . . . 4
39 33 , 34 , 35 , 36 , 37 , 38 caov42 6508 . . 3
40 distrsr 9489 . . . 4
41 distrsr 9489 . . . . . 6
42 41 oveq2i 6307 . . . . 5
43 distrsr 9489 . . . . 5
44 42 , 43 eqtri 2486 . . . 4
45 40 , 44 oveq12i 6308 . . 3
46 vex 3112 . . . . . 6
47 7 elexi 3119 . . . . . 6
48 vex 3112 . . . . . 6
49 mulcomsr 9487 . . . . . 6
50 distrsr 9489 . . . . . 6
51 ovex 6324 . . . . . 6
52 vex 3112 . . . . . 6
53 mulasssr 9488 . . . . . 6
54 46 , 47 , 48 , 49 , 50 , 51 , 52 , 53 caovdilem 6510 . . . . 5
55 mulasssr 9488 . . . . . . 7
56 55 oveq2i 6307 . . . . . 6
57 56 oveq2i 6307 . . . . 5
58 54 , 57 eqtri 2486 . . . 4
59 vex 3112 . . . . . . 7
60 vex 3112 . . . . . . 7
61 vex 3112 . . . . . . 7
62 59 , 46 , 48 , 49 , 50 , 60 , 61 , 53 caovdilem 6510 . . . . . 6
63 62 oveq2i 6307 . . . . 5
64 distrsr 9489 . . . . . 6
65 ovex 6324 . . . . . . . 8
66 47 , 46 , 65 , 49 , 53 caov12 6503 . . . . . . 7
67 66 oveq2i 6307 . . . . . 6
68 64 , 67 eqtri 2486 . . . . 5
69 63 , 68 eqtri 2486 . . . 4
70 58 , 69 oveq12i 6308 . . 3
71 39 , 45 , 70 3eqtr4ri 2497 . 2
72 ovex 6324 . . . 4
73 ovex 6324 . . . 4
74 ovex 6324 . . . 4
75 ovex 6324 . . . 4
76 72 , 73 , 74 , 36 , 37 , 75 caov42 6508 . . 3
77 distrsr 9489 . . . 4
78 distrsr 9489 . . . 4
79 77 , 78 oveq12i 6308 . . 3
80 59 , 46 , 48 , 49 , 50 , 60 , 52 , 53 caovdilem 6510 . . . 4
81 46 , 47 , 48 , 49 , 50 , 51 , 61 , 53 caovdilem 6510 . . . . 5
82 mulasssr 9488 . . . . . . . 8
83 82 oveq2i 6307 . . . . . . 7
84 47 , 59 , 65 , 49 , 53 caov12 6503 . . . . . . 7
85 83 , 84 eqtri 2486 . . . . . 6
86 85 oveq2i 6307 . . . . 5
87 81 , 86 eqtri 2486 . . . 4
88 80 , 87 oveq12i 6308 . . 3
89 76 , 79 , 88 3eqtr4ri 2497 . 2
90 1 , 2 , 3 , 4 , 5 , 19 ,
32 , 71 , 89 ecovass 7437 1
