Metamath Proof Explorer

Theorem mulerpq

Description: Multiplication is compatible with the equivalence relation. (Contributed by Mario Carneiro, 8-May-2013) (New usage is discouraged.)

Ref Expression
Assertion mulerpq 
|- ( ( /Q ` A ) .Q ( /Q ` B ) ) = ( /Q ` ( A .pQ B ) )

Proof

Step Hyp Ref Expression
1 nqercl 
 |-  ( A e. ( N. X. N. ) -> ( /Q ` A ) e. Q. )
2 nqercl 
 |-  ( B e. ( N. X. N. ) -> ( /Q ` B ) e. Q. )
3 mulpqnq 
 |-  ( ( ( /Q ` A ) e. Q. /\ ( /Q ` B ) e. Q. ) -> ( ( /Q ` A ) .Q ( /Q ` B ) ) = ( /Q ` ( ( /Q ` A ) .pQ ( /Q ` B ) ) ) )
4 1 2 3 syl2an 
 |-  ( ( A e. ( N. X. N. ) /\ B e. ( N. X. N. ) ) -> ( ( /Q ` A ) .Q ( /Q ` B ) ) = ( /Q ` ( ( /Q ` A ) .pQ ( /Q ` B ) ) ) )
5 enqer 
 |-  ~Q Er ( N. X. N. )
6 5 a1i 
 |-  ( ( A e. ( N. X. N. ) /\ B e. ( N. X. N. ) ) -> ~Q Er ( N. X. N. ) )
7 nqerrel 
 |-  ( A e. ( N. X. N. ) -> A ~Q ( /Q ` A ) )
8 7 adantr 
 |-  ( ( A e. ( N. X. N. ) /\ B e. ( N. X. N. ) ) -> A ~Q ( /Q ` A ) )
9 elpqn 
 |-  ( ( /Q ` A ) e. Q. -> ( /Q ` A ) e. ( N. X. N. ) )
10 1 9 syl 
 |-  ( A e. ( N. X. N. ) -> ( /Q ` A ) e. ( N. X. N. ) )
11 mulerpqlem 
 |-  ( ( A e. ( N. X. N. ) /\ ( /Q ` A ) e. ( N. X. N. ) /\ B e. ( N. X. N. ) ) -> ( A ~Q ( /Q ` A ) <-> ( A .pQ B ) ~Q ( ( /Q ` A ) .pQ B ) ) )
12 11 3exp 
 |-  ( A e. ( N. X. N. ) -> ( ( /Q ` A ) e. ( N. X. N. ) -> ( B e. ( N. X. N. ) -> ( A ~Q ( /Q ` A ) <-> ( A .pQ B ) ~Q ( ( /Q ` A ) .pQ B ) ) ) ) )
13 10 12 mpd 
 |-  ( A e. ( N. X. N. ) -> ( B e. ( N. X. N. ) -> ( A ~Q ( /Q ` A ) <-> ( A .pQ B ) ~Q ( ( /Q ` A ) .pQ B ) ) ) )
14 13 imp 
 |-  ( ( A e. ( N. X. N. ) /\ B e. ( N. X. N. ) ) -> ( A ~Q ( /Q ` A ) <-> ( A .pQ B ) ~Q ( ( /Q ` A ) .pQ B ) ) )
15 8 14 mpbid 
 |-  ( ( A e. ( N. X. N. ) /\ B e. ( N. X. N. ) ) -> ( A .pQ B ) ~Q ( ( /Q ` A ) .pQ B ) )
16 nqerrel 
 |-  ( B e. ( N. X. N. ) -> B ~Q ( /Q ` B ) )
17 16 adantl 
 |-  ( ( A e. ( N. X. N. ) /\ B e. ( N. X. N. ) ) -> B ~Q ( /Q ` B ) )
18 elpqn 
 |-  ( ( /Q ` B ) e. Q. -> ( /Q ` B ) e. ( N. X. N. ) )
19 2 18 syl 
 |-  ( B e. ( N. X. N. ) -> ( /Q ` B ) e. ( N. X. N. ) )
20 mulerpqlem 
 |-  ( ( B e. ( N. X. N. ) /\ ( /Q ` B ) e. ( N. X. N. ) /\ ( /Q ` A ) e. ( N. X. N. ) ) -> ( B ~Q ( /Q ` B ) <-> ( B .pQ ( /Q ` A ) ) ~Q ( ( /Q ` B ) .pQ ( /Q ` A ) ) ) )
21 20 3exp 
 |-  ( B e. ( N. X. N. ) -> ( ( /Q ` B ) e. ( N. X. N. ) -> ( ( /Q ` A ) e. ( N. X. N. ) -> ( B ~Q ( /Q ` B ) <-> ( B .pQ ( /Q ` A ) ) ~Q ( ( /Q ` B ) .pQ ( /Q ` A ) ) ) ) ) )
22 19 21 mpd 
 |-  ( B e. ( N. X. N. ) -> ( ( /Q ` A ) e. ( N. X. N. ) -> ( B ~Q ( /Q ` B ) <-> ( B .pQ ( /Q ` A ) ) ~Q ( ( /Q ` B ) .pQ ( /Q ` A ) ) ) ) )
23 10 22 mpan9 
 |-  ( ( A e. ( N. X. N. ) /\ B e. ( N. X. N. ) ) -> ( B ~Q ( /Q ` B ) <-> ( B .pQ ( /Q ` A ) ) ~Q ( ( /Q ` B ) .pQ ( /Q ` A ) ) ) )
24 17 23 mpbid 
 |-  ( ( A e. ( N. X. N. ) /\ B e. ( N. X. N. ) ) -> ( B .pQ ( /Q ` A ) ) ~Q ( ( /Q ` B ) .pQ ( /Q ` A ) ) )
25 mulcompq 
 |-  ( B .pQ ( /Q ` A ) ) = ( ( /Q ` A ) .pQ B )
26 mulcompq 
 |-  ( ( /Q ` B ) .pQ ( /Q ` A ) ) = ( ( /Q ` A ) .pQ ( /Q ` B ) )
27 24 25 26 3brtr3g 
 |-  ( ( A e. ( N. X. N. ) /\ B e. ( N. X. N. ) ) -> ( ( /Q ` A ) .pQ B ) ~Q ( ( /Q ` A ) .pQ ( /Q ` B ) ) )
28 6 15 27 ertrd 
 |-  ( ( A e. ( N. X. N. ) /\ B e. ( N. X. N. ) ) -> ( A .pQ B ) ~Q ( ( /Q ` A ) .pQ ( /Q ` B ) ) )
29 mulpqf 
 |-  .pQ : ( ( N. X. N. ) X. ( N. X. N. ) ) --> ( N. X. N. )
30 29 fovcl 
 |-  ( ( A e. ( N. X. N. ) /\ B e. ( N. X. N. ) ) -> ( A .pQ B ) e. ( N. X. N. ) )
31 29 fovcl 
 |-  ( ( ( /Q ` A ) e. ( N. X. N. ) /\ ( /Q ` B ) e. ( N. X. N. ) ) -> ( ( /Q ` A ) .pQ ( /Q ` B ) ) e. ( N. X. N. ) )
32 10 19 31 syl2an 
 |-  ( ( A e. ( N. X. N. ) /\ B e. ( N. X. N. ) ) -> ( ( /Q ` A ) .pQ ( /Q ` B ) ) e. ( N. X. N. ) )
33 nqereq 
 |-  ( ( ( A .pQ B ) e. ( N. X. N. ) /\ ( ( /Q ` A ) .pQ ( /Q ` B ) ) e. ( N. X. N. ) ) -> ( ( A .pQ B ) ~Q ( ( /Q ` A ) .pQ ( /Q ` B ) ) <-> ( /Q ` ( A .pQ B ) ) = ( /Q ` ( ( /Q ` A ) .pQ ( /Q ` B ) ) ) ) )
34 30 32 33 syl2anc 
 |-  ( ( A e. ( N. X. N. ) /\ B e. ( N. X. N. ) ) -> ( ( A .pQ B ) ~Q ( ( /Q ` A ) .pQ ( /Q ` B ) ) <-> ( /Q ` ( A .pQ B ) ) = ( /Q ` ( ( /Q ` A ) .pQ ( /Q ` B ) ) ) ) )
35 28 34 mpbid 
 |-  ( ( A e. ( N. X. N. ) /\ B e. ( N. X. N. ) ) -> ( /Q ` ( A .pQ B ) ) = ( /Q ` ( ( /Q ` A ) .pQ ( /Q ` B ) ) ) )
36 4 35 eqtr4d 
 |-  ( ( A e. ( N. X. N. ) /\ B e. ( N. X. N. ) ) -> ( ( /Q ` A ) .Q ( /Q ` B ) ) = ( /Q ` ( A .pQ B ) ) )
37 0nnq 
 |-  -. (/) e. Q.
38 nqerf 
 |-  /Q : ( N. X. N. ) --> Q.
39 38 fdmi 
 |-  dom /Q = ( N. X. N. )
40 39 eleq2i 
 |-  ( A e. dom /Q <-> A e. ( N. X. N. ) )
41 ndmfv 
 |-  ( -. A e. dom /Q -> ( /Q ` A ) = (/) )
42 40 41 sylnbir 
 |-  ( -. A e. ( N. X. N. ) -> ( /Q ` A ) = (/) )
43 42 eleq1d 
 |-  ( -. A e. ( N. X. N. ) -> ( ( /Q ` A ) e. Q. <-> (/) e. Q. ) )
44 37 43 mtbiri 
 |-  ( -. A e. ( N. X. N. ) -> -. ( /Q ` A ) e. Q. )
45 44 con4i 
 |-  ( ( /Q ` A ) e. Q. -> A e. ( N. X. N. ) )
46 39 eleq2i 
 |-  ( B e. dom /Q <-> B e. ( N. X. N. ) )
47 ndmfv 
 |-  ( -. B e. dom /Q -> ( /Q ` B ) = (/) )
48 46 47 sylnbir 
 |-  ( -. B e. ( N. X. N. ) -> ( /Q ` B ) = (/) )
49 48 eleq1d 
 |-  ( -. B e. ( N. X. N. ) -> ( ( /Q ` B ) e. Q. <-> (/) e. Q. ) )
50 37 49 mtbiri 
 |-  ( -. B e. ( N. X. N. ) -> -. ( /Q ` B ) e. Q. )
51 50 con4i 
 |-  ( ( /Q ` B ) e. Q. -> B e. ( N. X. N. ) )
52 45 51 anim12i 
 |-  ( ( ( /Q ` A ) e. Q. /\ ( /Q ` B ) e. Q. ) -> ( A e. ( N. X. N. ) /\ B e. ( N. X. N. ) ) )
53 mulnqf 
 |-  .Q : ( Q. X. Q. ) --> Q.
54 53 fdmi 
 |-  dom .Q = ( Q. X. Q. )
55 54 ndmov 
 |-  ( -. ( ( /Q ` A ) e. Q. /\ ( /Q ` B ) e. Q. ) -> ( ( /Q ` A ) .Q ( /Q ` B ) ) = (/) )
56 52 55 nsyl5 
 |-  ( -. ( A e. ( N. X. N. ) /\ B e. ( N. X. N. ) ) -> ( ( /Q ` A ) .Q ( /Q ` B ) ) = (/) )
57 0nelxp 
 |-  -. (/) e. ( N. X. N. )
58 39 eleq2i 
 |-  ( (/) e. dom /Q <-> (/) e. ( N. X. N. ) )
59 57 58 mtbir 
 |-  -. (/) e. dom /Q
60 29 fdmi 
 |-  dom .pQ = ( ( N. X. N. ) X. ( N. X. N. ) )
61 60 ndmov 
 |-  ( -. ( A e. ( N. X. N. ) /\ B e. ( N. X. N. ) ) -> ( A .pQ B ) = (/) )
62 61 eleq1d 
 |-  ( -. ( A e. ( N. X. N. ) /\ B e. ( N. X. N. ) ) -> ( ( A .pQ B ) e. dom /Q <-> (/) e. dom /Q ) )
63 59 62 mtbiri 
 |-  ( -. ( A e. ( N. X. N. ) /\ B e. ( N. X. N. ) ) -> -. ( A .pQ B ) e. dom /Q )
64 ndmfv 
 |-  ( -. ( A .pQ B ) e. dom /Q -> ( /Q ` ( A .pQ B ) ) = (/) )
65 63 64 syl 
 |-  ( -. ( A e. ( N. X. N. ) /\ B e. ( N. X. N. ) ) -> ( /Q ` ( A .pQ B ) ) = (/) )
66 56 65 eqtr4d 
 |-  ( -. ( A e. ( N. X. N. ) /\ B e. ( N. X. N. ) ) -> ( ( /Q ` A ) .Q ( /Q ` B ) ) = ( /Q ` ( A .pQ B ) ) )
67 36 66 pm2.61i 
 |-  ( ( /Q ` A ) .Q ( /Q ` B ) ) = ( /Q ` ( A .pQ B ) )