Step |
Hyp |
Ref |
Expression |
1 |
|
distrnq |
|- ( A .Q ( ( *Q ` ( 1Q +Q 1Q ) ) +Q ( *Q ` ( 1Q +Q 1Q ) ) ) ) = ( ( A .Q ( *Q ` ( 1Q +Q 1Q ) ) ) +Q ( A .Q ( *Q ` ( 1Q +Q 1Q ) ) ) ) |
2 |
|
distrnq |
|- ( ( 1Q +Q 1Q ) .Q ( ( *Q ` ( 1Q +Q 1Q ) ) +Q ( *Q ` ( 1Q +Q 1Q ) ) ) ) = ( ( ( 1Q +Q 1Q ) .Q ( *Q ` ( 1Q +Q 1Q ) ) ) +Q ( ( 1Q +Q 1Q ) .Q ( *Q ` ( 1Q +Q 1Q ) ) ) ) |
3 |
|
1nq |
|- 1Q e. Q. |
4 |
|
addclnq |
|- ( ( 1Q e. Q. /\ 1Q e. Q. ) -> ( 1Q +Q 1Q ) e. Q. ) |
5 |
3 3 4
|
mp2an |
|- ( 1Q +Q 1Q ) e. Q. |
6 |
|
recidnq |
|- ( ( 1Q +Q 1Q ) e. Q. -> ( ( 1Q +Q 1Q ) .Q ( *Q ` ( 1Q +Q 1Q ) ) ) = 1Q ) |
7 |
5 6
|
ax-mp |
|- ( ( 1Q +Q 1Q ) .Q ( *Q ` ( 1Q +Q 1Q ) ) ) = 1Q |
8 |
7 7
|
oveq12i |
|- ( ( ( 1Q +Q 1Q ) .Q ( *Q ` ( 1Q +Q 1Q ) ) ) +Q ( ( 1Q +Q 1Q ) .Q ( *Q ` ( 1Q +Q 1Q ) ) ) ) = ( 1Q +Q 1Q ) |
9 |
2 8
|
eqtri |
|- ( ( 1Q +Q 1Q ) .Q ( ( *Q ` ( 1Q +Q 1Q ) ) +Q ( *Q ` ( 1Q +Q 1Q ) ) ) ) = ( 1Q +Q 1Q ) |
10 |
9
|
oveq1i |
|- ( ( ( 1Q +Q 1Q ) .Q ( ( *Q ` ( 1Q +Q 1Q ) ) +Q ( *Q ` ( 1Q +Q 1Q ) ) ) ) .Q ( *Q ` ( 1Q +Q 1Q ) ) ) = ( ( 1Q +Q 1Q ) .Q ( *Q ` ( 1Q +Q 1Q ) ) ) |
11 |
7
|
oveq2i |
|- ( ( ( *Q ` ( 1Q +Q 1Q ) ) +Q ( *Q ` ( 1Q +Q 1Q ) ) ) .Q ( ( 1Q +Q 1Q ) .Q ( *Q ` ( 1Q +Q 1Q ) ) ) ) = ( ( ( *Q ` ( 1Q +Q 1Q ) ) +Q ( *Q ` ( 1Q +Q 1Q ) ) ) .Q 1Q ) |
12 |
|
mulassnq |
|- ( ( ( ( *Q ` ( 1Q +Q 1Q ) ) +Q ( *Q ` ( 1Q +Q 1Q ) ) ) .Q ( 1Q +Q 1Q ) ) .Q ( *Q ` ( 1Q +Q 1Q ) ) ) = ( ( ( *Q ` ( 1Q +Q 1Q ) ) +Q ( *Q ` ( 1Q +Q 1Q ) ) ) .Q ( ( 1Q +Q 1Q ) .Q ( *Q ` ( 1Q +Q 1Q ) ) ) ) |
13 |
|
mulcomnq |
|- ( ( ( *Q ` ( 1Q +Q 1Q ) ) +Q ( *Q ` ( 1Q +Q 1Q ) ) ) .Q ( 1Q +Q 1Q ) ) = ( ( 1Q +Q 1Q ) .Q ( ( *Q ` ( 1Q +Q 1Q ) ) +Q ( *Q ` ( 1Q +Q 1Q ) ) ) ) |
14 |
13
|
oveq1i |
|- ( ( ( ( *Q ` ( 1Q +Q 1Q ) ) +Q ( *Q ` ( 1Q +Q 1Q ) ) ) .Q ( 1Q +Q 1Q ) ) .Q ( *Q ` ( 1Q +Q 1Q ) ) ) = ( ( ( 1Q +Q 1Q ) .Q ( ( *Q ` ( 1Q +Q 1Q ) ) +Q ( *Q ` ( 1Q +Q 1Q ) ) ) ) .Q ( *Q ` ( 1Q +Q 1Q ) ) ) |
15 |
12 14
|
eqtr3i |
|- ( ( ( *Q ` ( 1Q +Q 1Q ) ) +Q ( *Q ` ( 1Q +Q 1Q ) ) ) .Q ( ( 1Q +Q 1Q ) .Q ( *Q ` ( 1Q +Q 1Q ) ) ) ) = ( ( ( 1Q +Q 1Q ) .Q ( ( *Q ` ( 1Q +Q 1Q ) ) +Q ( *Q ` ( 1Q +Q 1Q ) ) ) ) .Q ( *Q ` ( 1Q +Q 1Q ) ) ) |
16 |
|
recclnq |
|- ( ( 1Q +Q 1Q ) e. Q. -> ( *Q ` ( 1Q +Q 1Q ) ) e. Q. ) |
17 |
|
addclnq |
|- ( ( ( *Q ` ( 1Q +Q 1Q ) ) e. Q. /\ ( *Q ` ( 1Q +Q 1Q ) ) e. Q. ) -> ( ( *Q ` ( 1Q +Q 1Q ) ) +Q ( *Q ` ( 1Q +Q 1Q ) ) ) e. Q. ) |
18 |
16 16 17
|
syl2anc |
|- ( ( 1Q +Q 1Q ) e. Q. -> ( ( *Q ` ( 1Q +Q 1Q ) ) +Q ( *Q ` ( 1Q +Q 1Q ) ) ) e. Q. ) |
19 |
|
mulidnq |
|- ( ( ( *Q ` ( 1Q +Q 1Q ) ) +Q ( *Q ` ( 1Q +Q 1Q ) ) ) e. Q. -> ( ( ( *Q ` ( 1Q +Q 1Q ) ) +Q ( *Q ` ( 1Q +Q 1Q ) ) ) .Q 1Q ) = ( ( *Q ` ( 1Q +Q 1Q ) ) +Q ( *Q ` ( 1Q +Q 1Q ) ) ) ) |
20 |
5 18 19
|
mp2b |
|- ( ( ( *Q ` ( 1Q +Q 1Q ) ) +Q ( *Q ` ( 1Q +Q 1Q ) ) ) .Q 1Q ) = ( ( *Q ` ( 1Q +Q 1Q ) ) +Q ( *Q ` ( 1Q +Q 1Q ) ) ) |
21 |
11 15 20
|
3eqtr3i |
|- ( ( ( 1Q +Q 1Q ) .Q ( ( *Q ` ( 1Q +Q 1Q ) ) +Q ( *Q ` ( 1Q +Q 1Q ) ) ) ) .Q ( *Q ` ( 1Q +Q 1Q ) ) ) = ( ( *Q ` ( 1Q +Q 1Q ) ) +Q ( *Q ` ( 1Q +Q 1Q ) ) ) |
22 |
10 21 7
|
3eqtr3i |
|- ( ( *Q ` ( 1Q +Q 1Q ) ) +Q ( *Q ` ( 1Q +Q 1Q ) ) ) = 1Q |
23 |
22
|
oveq2i |
|- ( A .Q ( ( *Q ` ( 1Q +Q 1Q ) ) +Q ( *Q ` ( 1Q +Q 1Q ) ) ) ) = ( A .Q 1Q ) |
24 |
1 23
|
eqtr3i |
|- ( ( A .Q ( *Q ` ( 1Q +Q 1Q ) ) ) +Q ( A .Q ( *Q ` ( 1Q +Q 1Q ) ) ) ) = ( A .Q 1Q ) |
25 |
|
mulidnq |
|- ( A e. Q. -> ( A .Q 1Q ) = A ) |
26 |
24 25
|
eqtrid |
|- ( A e. Q. -> ( ( A .Q ( *Q ` ( 1Q +Q 1Q ) ) ) +Q ( A .Q ( *Q ` ( 1Q +Q 1Q ) ) ) ) = A ) |
27 |
|
ovex |
|- ( A .Q ( *Q ` ( 1Q +Q 1Q ) ) ) e. _V |
28 |
|
oveq12 |
|- ( ( x = ( A .Q ( *Q ` ( 1Q +Q 1Q ) ) ) /\ x = ( A .Q ( *Q ` ( 1Q +Q 1Q ) ) ) ) -> ( x +Q x ) = ( ( A .Q ( *Q ` ( 1Q +Q 1Q ) ) ) +Q ( A .Q ( *Q ` ( 1Q +Q 1Q ) ) ) ) ) |
29 |
28
|
anidms |
|- ( x = ( A .Q ( *Q ` ( 1Q +Q 1Q ) ) ) -> ( x +Q x ) = ( ( A .Q ( *Q ` ( 1Q +Q 1Q ) ) ) +Q ( A .Q ( *Q ` ( 1Q +Q 1Q ) ) ) ) ) |
30 |
29
|
eqeq1d |
|- ( x = ( A .Q ( *Q ` ( 1Q +Q 1Q ) ) ) -> ( ( x +Q x ) = A <-> ( ( A .Q ( *Q ` ( 1Q +Q 1Q ) ) ) +Q ( A .Q ( *Q ` ( 1Q +Q 1Q ) ) ) ) = A ) ) |
31 |
27 30
|
spcev |
|- ( ( ( A .Q ( *Q ` ( 1Q +Q 1Q ) ) ) +Q ( A .Q ( *Q ` ( 1Q +Q 1Q ) ) ) ) = A -> E. x ( x +Q x ) = A ) |
32 |
26 31
|
syl |
|- ( A e. Q. -> E. x ( x +Q x ) = A ) |