| Step | Hyp | Ref | Expression | 
|---|
| 1 |  | ltrelnq 10967 | . . 3
⊢ 
<Q ⊆ (Q ×
Q) | 
| 2 | 1 | brel 5749 | . 2
⊢ (𝐴 <Q
𝐵 → (𝐴 ∈ Q ∧ 𝐵 ∈
Q)) | 
| 3 | 1 | brel 5749 | . . 3
⊢
((*Q‘𝐵) <Q
(*Q‘𝐴) →
((*Q‘𝐵) ∈ Q ∧
(*Q‘𝐴) ∈ Q)) | 
| 4 |  | dmrecnq 11009 | . . . . 5
⊢ dom
*Q = Q | 
| 5 |  | 0nnq 10965 | . . . . 5
⊢  ¬
∅ ∈ Q | 
| 6 | 4, 5 | ndmfvrcl 6941 | . . . 4
⊢
((*Q‘𝐵) ∈ Q → 𝐵 ∈
Q) | 
| 7 | 4, 5 | ndmfvrcl 6941 | . . . 4
⊢
((*Q‘𝐴) ∈ Q → 𝐴 ∈
Q) | 
| 8 | 6, 7 | anim12ci 614 | . . 3
⊢
(((*Q‘𝐵) ∈ Q ∧
(*Q‘𝐴) ∈ Q) → (𝐴 ∈ Q ∧
𝐵 ∈
Q)) | 
| 9 | 3, 8 | syl 17 | . 2
⊢
((*Q‘𝐵) <Q
(*Q‘𝐴) → (𝐴 ∈ Q ∧ 𝐵 ∈
Q)) | 
| 10 |  | breq1 5145 | . . . 4
⊢ (𝑥 = 𝐴 → (𝑥 <Q 𝑦 ↔ 𝐴 <Q 𝑦)) | 
| 11 |  | fveq2 6905 | . . . . 5
⊢ (𝑥 = 𝐴 →
(*Q‘𝑥) = (*Q‘𝐴)) | 
| 12 | 11 | breq2d 5154 | . . . 4
⊢ (𝑥 = 𝐴 →
((*Q‘𝑦) <Q
(*Q‘𝑥) ↔
(*Q‘𝑦) <Q
(*Q‘𝐴))) | 
| 13 | 10, 12 | bibi12d 345 | . . 3
⊢ (𝑥 = 𝐴 → ((𝑥 <Q 𝑦 ↔
(*Q‘𝑦) <Q
(*Q‘𝑥)) ↔ (𝐴 <Q 𝑦 ↔
(*Q‘𝑦) <Q
(*Q‘𝐴)))) | 
| 14 |  | breq2 5146 | . . . 4
⊢ (𝑦 = 𝐵 → (𝐴 <Q 𝑦 ↔ 𝐴 <Q 𝐵)) | 
| 15 |  | fveq2 6905 | . . . . 5
⊢ (𝑦 = 𝐵 →
(*Q‘𝑦) = (*Q‘𝐵)) | 
| 16 | 15 | breq1d 5152 | . . . 4
⊢ (𝑦 = 𝐵 →
((*Q‘𝑦) <Q
(*Q‘𝐴) ↔
(*Q‘𝐵) <Q
(*Q‘𝐴))) | 
| 17 | 14, 16 | bibi12d 345 | . . 3
⊢ (𝑦 = 𝐵 → ((𝐴 <Q 𝑦 ↔
(*Q‘𝑦) <Q
(*Q‘𝐴)) ↔ (𝐴 <Q 𝐵 ↔
(*Q‘𝐵) <Q
(*Q‘𝐴)))) | 
| 18 |  | recclnq 11007 | . . . . . 6
⊢ (𝑥 ∈ Q →
(*Q‘𝑥) ∈ Q) | 
| 19 |  | recclnq 11007 | . . . . . 6
⊢ (𝑦 ∈ Q →
(*Q‘𝑦) ∈ Q) | 
| 20 |  | mulclnq 10988 | . . . . . 6
⊢
(((*Q‘𝑥) ∈ Q ∧
(*Q‘𝑦) ∈ Q) →
((*Q‘𝑥) ·Q
(*Q‘𝑦)) ∈ Q) | 
| 21 | 18, 19, 20 | syl2an 596 | . . . . 5
⊢ ((𝑥 ∈ Q ∧
𝑦 ∈ Q)
→ ((*Q‘𝑥) ·Q
(*Q‘𝑦)) ∈ Q) | 
| 22 |  | ltmnq 11013 | . . . . 5
⊢
(((*Q‘𝑥) ·Q
(*Q‘𝑦)) ∈ Q → (𝑥 <Q
𝑦 ↔
(((*Q‘𝑥) ·Q
(*Q‘𝑦)) ·Q 𝑥) <Q
(((*Q‘𝑥) ·Q
(*Q‘𝑦)) ·Q 𝑦))) | 
| 23 | 21, 22 | syl 17 | . . . 4
⊢ ((𝑥 ∈ Q ∧
𝑦 ∈ Q)
→ (𝑥
<Q 𝑦 ↔
(((*Q‘𝑥) ·Q
(*Q‘𝑦)) ·Q 𝑥) <Q
(((*Q‘𝑥) ·Q
(*Q‘𝑦)) ·Q 𝑦))) | 
| 24 |  | mulcomnq 10994 | . . . . . . 7
⊢
(((*Q‘𝑥) ·Q
(*Q‘𝑦)) ·Q 𝑥) = (𝑥 ·Q
((*Q‘𝑥) ·Q
(*Q‘𝑦))) | 
| 25 |  | mulassnq 11000 | . . . . . . 7
⊢ ((𝑥
·Q (*Q‘𝑥))
·Q (*Q‘𝑦)) = (𝑥 ·Q
((*Q‘𝑥) ·Q
(*Q‘𝑦))) | 
| 26 |  | mulcomnq 10994 | . . . . . . 7
⊢ ((𝑥
·Q (*Q‘𝑥))
·Q (*Q‘𝑦)) =
((*Q‘𝑦) ·Q (𝑥
·Q (*Q‘𝑥))) | 
| 27 | 24, 25, 26 | 3eqtr2i 2770 | . . . . . 6
⊢
(((*Q‘𝑥) ·Q
(*Q‘𝑦)) ·Q 𝑥) =
((*Q‘𝑦) ·Q (𝑥
·Q (*Q‘𝑥))) | 
| 28 |  | recidnq 11006 | . . . . . . . 8
⊢ (𝑥 ∈ Q →
(𝑥
·Q (*Q‘𝑥)) =
1Q) | 
| 29 | 28 | oveq2d 7448 | . . . . . . 7
⊢ (𝑥 ∈ Q →
((*Q‘𝑦) ·Q (𝑥
·Q (*Q‘𝑥))) =
((*Q‘𝑦) ·Q
1Q)) | 
| 30 |  | mulidnq 11004 | . . . . . . . 8
⊢
((*Q‘𝑦) ∈ Q →
((*Q‘𝑦) ·Q
1Q) = (*Q‘𝑦)) | 
| 31 | 19, 30 | syl 17 | . . . . . . 7
⊢ (𝑦 ∈ Q →
((*Q‘𝑦) ·Q
1Q) = (*Q‘𝑦)) | 
| 32 | 29, 31 | sylan9eq 2796 | . . . . . 6
⊢ ((𝑥 ∈ Q ∧
𝑦 ∈ Q)
→ ((*Q‘𝑦) ·Q (𝑥
·Q (*Q‘𝑥))) =
(*Q‘𝑦)) | 
| 33 | 27, 32 | eqtrid 2788 | . . . . 5
⊢ ((𝑥 ∈ Q ∧
𝑦 ∈ Q)
→ (((*Q‘𝑥) ·Q
(*Q‘𝑦)) ·Q 𝑥) =
(*Q‘𝑦)) | 
| 34 |  | mulassnq 11000 | . . . . . . 7
⊢
(((*Q‘𝑥) ·Q
(*Q‘𝑦)) ·Q 𝑦) =
((*Q‘𝑥) ·Q
((*Q‘𝑦) ·Q 𝑦)) | 
| 35 |  | mulcomnq 10994 | . . . . . . . 8
⊢
((*Q‘𝑦) ·Q 𝑦) = (𝑦 ·Q
(*Q‘𝑦)) | 
| 36 | 35 | oveq2i 7443 | . . . . . . 7
⊢
((*Q‘𝑥) ·Q
((*Q‘𝑦) ·Q 𝑦)) =
((*Q‘𝑥) ·Q (𝑦
·Q (*Q‘𝑦))) | 
| 37 | 34, 36 | eqtri 2764 | . . . . . 6
⊢
(((*Q‘𝑥) ·Q
(*Q‘𝑦)) ·Q 𝑦) =
((*Q‘𝑥) ·Q (𝑦
·Q (*Q‘𝑦))) | 
| 38 |  | recidnq 11006 | . . . . . . . 8
⊢ (𝑦 ∈ Q →
(𝑦
·Q (*Q‘𝑦)) =
1Q) | 
| 39 | 38 | oveq2d 7448 | . . . . . . 7
⊢ (𝑦 ∈ Q →
((*Q‘𝑥) ·Q (𝑦
·Q (*Q‘𝑦))) =
((*Q‘𝑥) ·Q
1Q)) | 
| 40 |  | mulidnq 11004 | . . . . . . . 8
⊢
((*Q‘𝑥) ∈ Q →
((*Q‘𝑥) ·Q
1Q) = (*Q‘𝑥)) | 
| 41 | 18, 40 | syl 17 | . . . . . . 7
⊢ (𝑥 ∈ Q →
((*Q‘𝑥) ·Q
1Q) = (*Q‘𝑥)) | 
| 42 | 39, 41 | sylan9eqr 2798 | . . . . . 6
⊢ ((𝑥 ∈ Q ∧
𝑦 ∈ Q)
→ ((*Q‘𝑥) ·Q (𝑦
·Q (*Q‘𝑦))) =
(*Q‘𝑥)) | 
| 43 | 37, 42 | eqtrid 2788 | . . . . 5
⊢ ((𝑥 ∈ Q ∧
𝑦 ∈ Q)
→ (((*Q‘𝑥) ·Q
(*Q‘𝑦)) ·Q 𝑦) =
(*Q‘𝑥)) | 
| 44 | 33, 43 | breq12d 5155 | . . . 4
⊢ ((𝑥 ∈ Q ∧
𝑦 ∈ Q)
→ ((((*Q‘𝑥) ·Q
(*Q‘𝑦)) ·Q 𝑥) <Q
(((*Q‘𝑥) ·Q
(*Q‘𝑦)) ·Q 𝑦) ↔
(*Q‘𝑦) <Q
(*Q‘𝑥))) | 
| 45 | 23, 44 | bitrd 279 | . . 3
⊢ ((𝑥 ∈ Q ∧
𝑦 ∈ Q)
→ (𝑥
<Q 𝑦 ↔
(*Q‘𝑦) <Q
(*Q‘𝑥))) | 
| 46 | 13, 17, 45 | vtocl2ga 3577 | . 2
⊢ ((𝐴 ∈ Q ∧
𝐵 ∈ Q)
→ (𝐴
<Q 𝐵 ↔
(*Q‘𝐵) <Q
(*Q‘𝐴))) | 
| 47 | 2, 9, 46 | pm5.21nii 378 | 1
⊢ (𝐴 <Q
𝐵 ↔
(*Q‘𝐵) <Q
(*Q‘𝐴)) |