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] ‘ 𝐴 ) ·Q ( [Q] ‘ 𝐵 ) ) = ( [Q] ‘ ( 𝐴 ·pQ 𝐵 ) )

Proof

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