This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem mulidnq

Description: Multiplication identity element for positive fractions. (Contributed by NM, 3-Mar-1996) (Revised by Mario Carneiro, 28-Apr-2013) (New usage is discouraged.)

Ref Expression
Assertion mulidnq 
|- ( A e. Q. -> ( A .Q 1Q ) = A )

Proof

Step Hyp Ref Expression
1 1nq 
 |-  1Q e. Q.
2 mulpqnq 
 |-  ( ( A e. Q. /\ 1Q e. Q. ) -> ( A .Q 1Q ) = ( /Q ` ( A .pQ 1Q ) ) )
3 1 2 mpan2 
 |-  ( A e. Q. -> ( A .Q 1Q ) = ( /Q ` ( A .pQ 1Q ) ) )
4 relxp 
 |-  Rel ( N. X. N. )
5 elpqn 
 |-  ( A e. Q. -> A e. ( N. X. N. ) )
6 1st2nd 
 |-  ( ( Rel ( N. X. N. ) /\ A e. ( N. X. N. ) ) -> A = <. ( 1st ` A ) , ( 2nd ` A ) >. )
7 4 5 6 sylancr 
 |-  ( A e. Q. -> A = <. ( 1st ` A ) , ( 2nd ` A ) >. )
8 df-1nq 
 |-  1Q = <. 1o , 1o >.
9 8 a1i 
 |-  ( A e. Q. -> 1Q = <. 1o , 1o >. )
10 7 9 oveq12d 
 |-  ( A e. Q. -> ( A .pQ 1Q ) = ( <. ( 1st ` A ) , ( 2nd ` A ) >. .pQ <. 1o , 1o >. ) )
11 xp1st 
 |-  ( A e. ( N. X. N. ) -> ( 1st ` A ) e. N. )
12 5 11 syl 
 |-  ( A e. Q. -> ( 1st ` A ) e. N. )
13 xp2nd 
 |-  ( A e. ( N. X. N. ) -> ( 2nd ` A ) e. N. )
14 5 13 syl 
 |-  ( A e. Q. -> ( 2nd ` A ) e. N. )
15 1pi 
 |-  1o e. N.
16 15 a1i 
 |-  ( A e. Q. -> 1o e. N. )
17 mulpipq 
 |-  ( ( ( ( 1st ` A ) e. N. /\ ( 2nd ` A ) e. N. ) /\ ( 1o e. N. /\ 1o e. N. ) ) -> ( <. ( 1st ` A ) , ( 2nd ` A ) >. .pQ <. 1o , 1o >. ) = <. ( ( 1st ` A ) .N 1o ) , ( ( 2nd ` A ) .N 1o ) >. )
18 12 14 16 16 17 syl22anc 
 |-  ( A e. Q. -> ( <. ( 1st ` A ) , ( 2nd ` A ) >. .pQ <. 1o , 1o >. ) = <. ( ( 1st ` A ) .N 1o ) , ( ( 2nd ` A ) .N 1o ) >. )
19 mulidpi 
 |-  ( ( 1st ` A ) e. N. -> ( ( 1st ` A ) .N 1o ) = ( 1st ` A ) )
20 11 19 syl 
 |-  ( A e. ( N. X. N. ) -> ( ( 1st ` A ) .N 1o ) = ( 1st ` A ) )
21 mulidpi 
 |-  ( ( 2nd ` A ) e. N. -> ( ( 2nd ` A ) .N 1o ) = ( 2nd ` A ) )
22 13 21 syl 
 |-  ( A e. ( N. X. N. ) -> ( ( 2nd ` A ) .N 1o ) = ( 2nd ` A ) )
23 20 22 opeq12d 
 |-  ( A e. ( N. X. N. ) -> <. ( ( 1st ` A ) .N 1o ) , ( ( 2nd ` A ) .N 1o ) >. = <. ( 1st ` A ) , ( 2nd ` A ) >. )
24 5 23 syl 
 |-  ( A e. Q. -> <. ( ( 1st ` A ) .N 1o ) , ( ( 2nd ` A ) .N 1o ) >. = <. ( 1st ` A ) , ( 2nd ` A ) >. )
25 10 18 24 3eqtrd 
 |-  ( A e. Q. -> ( A .pQ 1Q ) = <. ( 1st ` A ) , ( 2nd ` A ) >. )
26 25 7 eqtr4d 
 |-  ( A e. Q. -> ( A .pQ 1Q ) = A )
27 26 fveq2d 
 |-  ( A e. Q. -> ( /Q ` ( A .pQ 1Q ) ) = ( /Q ` A ) )
28 nqerid 
 |-  ( A e. Q. -> ( /Q ` A ) = A )
29 3 27 28 3eqtrd 
 |-  ( A e. Q. -> ( A .Q 1Q ) = A )