Step | Hyp | Ref
| Expression |
1 | | ltmnqg 7356 |
. . . . . . 7
⊢ ((𝑦 ∈ Q ∧
𝑧 ∈ Q
∧ 𝑤 ∈
Q) → (𝑦
<Q 𝑧 ↔ (𝑤 ·Q 𝑦) <Q
(𝑤
·Q 𝑧))) |
2 | 1 | adantl 275 |
. . . . . 6
⊢
(((((𝐴 ∈
P ∧ 𝐺
∈ (1st ‘𝐴)) ∧ (𝐵 ∈ P ∧ 𝐻 ∈ (1st
‘𝐵))) ∧ 𝑋 ∈ Q) ∧
(𝑦 ∈ Q
∧ 𝑧 ∈
Q ∧ 𝑤
∈ Q)) → (𝑦 <Q 𝑧 ↔ (𝑤 ·Q 𝑦) <Q
(𝑤
·Q 𝑧))) |
3 | | simpr 109 |
. . . . . 6
⊢ ((((𝐴 ∈ P ∧
𝐺 ∈ (1st
‘𝐴)) ∧ (𝐵 ∈ P ∧
𝐻 ∈ (1st
‘𝐵))) ∧ 𝑋 ∈ Q) →
𝑋 ∈
Q) |
4 | | prop 7430 |
. . . . . . . . 9
⊢ (𝐴 ∈ P →
〈(1st ‘𝐴), (2nd ‘𝐴)〉 ∈
P) |
5 | | elprnql 7436 |
. . . . . . . . 9
⊢
((〈(1st ‘𝐴), (2nd ‘𝐴)〉 ∈ P ∧ 𝐺 ∈ (1st
‘𝐴)) → 𝐺 ∈
Q) |
6 | 4, 5 | sylan 281 |
. . . . . . . 8
⊢ ((𝐴 ∈ P ∧
𝐺 ∈ (1st
‘𝐴)) → 𝐺 ∈
Q) |
7 | 6 | ad2antrr 485 |
. . . . . . 7
⊢ ((((𝐴 ∈ P ∧
𝐺 ∈ (1st
‘𝐴)) ∧ (𝐵 ∈ P ∧
𝐻 ∈ (1st
‘𝐵))) ∧ 𝑋 ∈ Q) →
𝐺 ∈
Q) |
8 | | prop 7430 |
. . . . . . . . 9
⊢ (𝐵 ∈ P →
〈(1st ‘𝐵), (2nd ‘𝐵)〉 ∈
P) |
9 | | elprnql 7436 |
. . . . . . . . 9
⊢
((〈(1st ‘𝐵), (2nd ‘𝐵)〉 ∈ P ∧ 𝐻 ∈ (1st
‘𝐵)) → 𝐻 ∈
Q) |
10 | 8, 9 | sylan 281 |
. . . . . . . 8
⊢ ((𝐵 ∈ P ∧
𝐻 ∈ (1st
‘𝐵)) → 𝐻 ∈
Q) |
11 | 10 | ad2antlr 486 |
. . . . . . 7
⊢ ((((𝐴 ∈ P ∧
𝐺 ∈ (1st
‘𝐴)) ∧ (𝐵 ∈ P ∧
𝐻 ∈ (1st
‘𝐵))) ∧ 𝑋 ∈ Q) →
𝐻 ∈
Q) |
12 | | mulclnq 7331 |
. . . . . . 7
⊢ ((𝐺 ∈ Q ∧
𝐻 ∈ Q)
→ (𝐺
·Q 𝐻) ∈ Q) |
13 | 7, 11, 12 | syl2anc 409 |
. . . . . 6
⊢ ((((𝐴 ∈ P ∧
𝐺 ∈ (1st
‘𝐴)) ∧ (𝐵 ∈ P ∧
𝐻 ∈ (1st
‘𝐵))) ∧ 𝑋 ∈ Q) →
(𝐺
·Q 𝐻) ∈ Q) |
14 | | recclnq 7347 |
. . . . . . 7
⊢ (𝐻 ∈ Q →
(*Q‘𝐻) ∈ Q) |
15 | 11, 14 | syl 14 |
. . . . . 6
⊢ ((((𝐴 ∈ P ∧
𝐺 ∈ (1st
‘𝐴)) ∧ (𝐵 ∈ P ∧
𝐻 ∈ (1st
‘𝐵))) ∧ 𝑋 ∈ Q) →
(*Q‘𝐻) ∈ Q) |
16 | | mulcomnqg 7338 |
. . . . . . 7
⊢ ((𝑦 ∈ Q ∧
𝑧 ∈ Q)
→ (𝑦
·Q 𝑧) = (𝑧 ·Q 𝑦)) |
17 | 16 | adantl 275 |
. . . . . 6
⊢
(((((𝐴 ∈
P ∧ 𝐺
∈ (1st ‘𝐴)) ∧ (𝐵 ∈ P ∧ 𝐻 ∈ (1st
‘𝐵))) ∧ 𝑋 ∈ Q) ∧
(𝑦 ∈ Q
∧ 𝑧 ∈
Q)) → (𝑦
·Q 𝑧) = (𝑧 ·Q 𝑦)) |
18 | 2, 3, 13, 15, 17 | caovord2d 6020 |
. . . . 5
⊢ ((((𝐴 ∈ P ∧
𝐺 ∈ (1st
‘𝐴)) ∧ (𝐵 ∈ P ∧
𝐻 ∈ (1st
‘𝐵))) ∧ 𝑋 ∈ Q) →
(𝑋
<Q (𝐺 ·Q 𝐻) ↔ (𝑋 ·Q
(*Q‘𝐻)) <Q ((𝐺
·Q 𝐻) ·Q
(*Q‘𝐻)))) |
19 | | mulassnqg 7339 |
. . . . . . . 8
⊢ ((𝐺 ∈ Q ∧
𝐻 ∈ Q
∧ (*Q‘𝐻) ∈ Q) → ((𝐺
·Q 𝐻) ·Q
(*Q‘𝐻)) = (𝐺 ·Q (𝐻
·Q (*Q‘𝐻)))) |
20 | 7, 11, 15, 19 | syl3anc 1233 |
. . . . . . 7
⊢ ((((𝐴 ∈ P ∧
𝐺 ∈ (1st
‘𝐴)) ∧ (𝐵 ∈ P ∧
𝐻 ∈ (1st
‘𝐵))) ∧ 𝑋 ∈ Q) →
((𝐺
·Q 𝐻) ·Q
(*Q‘𝐻)) = (𝐺 ·Q (𝐻
·Q (*Q‘𝐻)))) |
21 | | recidnq 7348 |
. . . . . . . . 9
⊢ (𝐻 ∈ Q →
(𝐻
·Q (*Q‘𝐻)) =
1Q) |
22 | 21 | oveq2d 5867 |
. . . . . . . 8
⊢ (𝐻 ∈ Q →
(𝐺
·Q (𝐻 ·Q
(*Q‘𝐻))) = (𝐺 ·Q
1Q)) |
23 | 11, 22 | syl 14 |
. . . . . . 7
⊢ ((((𝐴 ∈ P ∧
𝐺 ∈ (1st
‘𝐴)) ∧ (𝐵 ∈ P ∧
𝐻 ∈ (1st
‘𝐵))) ∧ 𝑋 ∈ Q) →
(𝐺
·Q (𝐻 ·Q
(*Q‘𝐻))) = (𝐺 ·Q
1Q)) |
24 | | mulidnq 7344 |
. . . . . . . 8
⊢ (𝐺 ∈ Q →
(𝐺
·Q 1Q) = 𝐺) |
25 | 7, 24 | syl 14 |
. . . . . . 7
⊢ ((((𝐴 ∈ P ∧
𝐺 ∈ (1st
‘𝐴)) ∧ (𝐵 ∈ P ∧
𝐻 ∈ (1st
‘𝐵))) ∧ 𝑋 ∈ Q) →
(𝐺
·Q 1Q) = 𝐺) |
26 | 20, 23, 25 | 3eqtrd 2207 |
. . . . . 6
⊢ ((((𝐴 ∈ P ∧
𝐺 ∈ (1st
‘𝐴)) ∧ (𝐵 ∈ P ∧
𝐻 ∈ (1st
‘𝐵))) ∧ 𝑋 ∈ Q) →
((𝐺
·Q 𝐻) ·Q
(*Q‘𝐻)) = 𝐺) |
27 | 26 | breq2d 3999 |
. . . . 5
⊢ ((((𝐴 ∈ P ∧
𝐺 ∈ (1st
‘𝐴)) ∧ (𝐵 ∈ P ∧
𝐻 ∈ (1st
‘𝐵))) ∧ 𝑋 ∈ Q) →
((𝑋
·Q (*Q‘𝐻))
<Q ((𝐺 ·Q 𝐻)
·Q (*Q‘𝐻)) ↔ (𝑋 ·Q
(*Q‘𝐻)) <Q 𝐺)) |
28 | 18, 27 | bitrd 187 |
. . . 4
⊢ ((((𝐴 ∈ P ∧
𝐺 ∈ (1st
‘𝐴)) ∧ (𝐵 ∈ P ∧
𝐻 ∈ (1st
‘𝐵))) ∧ 𝑋 ∈ Q) →
(𝑋
<Q (𝐺 ·Q 𝐻) ↔ (𝑋 ·Q
(*Q‘𝐻)) <Q 𝐺)) |
29 | | prcdnql 7439 |
. . . . . 6
⊢
((〈(1st ‘𝐴), (2nd ‘𝐴)〉 ∈ P ∧ 𝐺 ∈ (1st
‘𝐴)) → ((𝑋
·Q (*Q‘𝐻))
<Q 𝐺 → (𝑋 ·Q
(*Q‘𝐻)) ∈ (1st ‘𝐴))) |
30 | 4, 29 | sylan 281 |
. . . . 5
⊢ ((𝐴 ∈ P ∧
𝐺 ∈ (1st
‘𝐴)) → ((𝑋
·Q (*Q‘𝐻))
<Q 𝐺 → (𝑋 ·Q
(*Q‘𝐻)) ∈ (1st ‘𝐴))) |
31 | 30 | ad2antrr 485 |
. . . 4
⊢ ((((𝐴 ∈ P ∧
𝐺 ∈ (1st
‘𝐴)) ∧ (𝐵 ∈ P ∧
𝐻 ∈ (1st
‘𝐵))) ∧ 𝑋 ∈ Q) →
((𝑋
·Q (*Q‘𝐻))
<Q 𝐺 → (𝑋 ·Q
(*Q‘𝐻)) ∈ (1st ‘𝐴))) |
32 | 28, 31 | sylbid 149 |
. . 3
⊢ ((((𝐴 ∈ P ∧
𝐺 ∈ (1st
‘𝐴)) ∧ (𝐵 ∈ P ∧
𝐻 ∈ (1st
‘𝐵))) ∧ 𝑋 ∈ Q) →
(𝑋
<Q (𝐺 ·Q 𝐻) → (𝑋 ·Q
(*Q‘𝐻)) ∈ (1st ‘𝐴))) |
33 | | df-imp 7424 |
. . . . . . . . 9
⊢
·P = (𝑤 ∈ P, 𝑣 ∈ P ↦ 〈{𝑥 ∈ Q ∣
∃𝑦 ∈
Q ∃𝑧
∈ Q (𝑦
∈ (1st ‘𝑤) ∧ 𝑧 ∈ (1st ‘𝑣) ∧ 𝑥 = (𝑦 ·Q 𝑧))}, {𝑥 ∈ Q ∣ ∃𝑦 ∈ Q
∃𝑧 ∈
Q (𝑦 ∈
(2nd ‘𝑤)
∧ 𝑧 ∈
(2nd ‘𝑣)
∧ 𝑥 = (𝑦
·Q 𝑧))}〉) |
34 | | mulclnq 7331 |
. . . . . . . . 9
⊢ ((𝑦 ∈ Q ∧
𝑧 ∈ Q)
→ (𝑦
·Q 𝑧) ∈ Q) |
35 | 33, 34 | genpprecll 7469 |
. . . . . . . 8
⊢ ((𝐴 ∈ P ∧
𝐵 ∈ P)
→ (((𝑋
·Q (*Q‘𝐻)) ∈ (1st
‘𝐴) ∧ 𝐻 ∈ (1st
‘𝐵)) → ((𝑋
·Q (*Q‘𝐻))
·Q 𝐻) ∈ (1st ‘(𝐴
·P 𝐵)))) |
36 | 35 | exp4b 365 |
. . . . . . 7
⊢ (𝐴 ∈ P →
(𝐵 ∈ P
→ ((𝑋
·Q (*Q‘𝐻)) ∈ (1st
‘𝐴) → (𝐻 ∈ (1st
‘𝐵) → ((𝑋
·Q (*Q‘𝐻))
·Q 𝐻) ∈ (1st ‘(𝐴
·P 𝐵)))))) |
37 | 36 | com34 83 |
. . . . . 6
⊢ (𝐴 ∈ P →
(𝐵 ∈ P
→ (𝐻 ∈
(1st ‘𝐵)
→ ((𝑋
·Q (*Q‘𝐻)) ∈ (1st
‘𝐴) → ((𝑋
·Q (*Q‘𝐻))
·Q 𝐻) ∈ (1st ‘(𝐴
·P 𝐵)))))) |
38 | 37 | imp32 255 |
. . . . 5
⊢ ((𝐴 ∈ P ∧
(𝐵 ∈ P
∧ 𝐻 ∈
(1st ‘𝐵)))
→ ((𝑋
·Q (*Q‘𝐻)) ∈ (1st
‘𝐴) → ((𝑋
·Q (*Q‘𝐻))
·Q 𝐻) ∈ (1st ‘(𝐴
·P 𝐵)))) |
39 | 38 | adantlr 474 |
. . . 4
⊢ (((𝐴 ∈ P ∧
𝐺 ∈ (1st
‘𝐴)) ∧ (𝐵 ∈ P ∧
𝐻 ∈ (1st
‘𝐵))) → ((𝑋
·Q (*Q‘𝐻)) ∈ (1st
‘𝐴) → ((𝑋
·Q (*Q‘𝐻))
·Q 𝐻) ∈ (1st ‘(𝐴
·P 𝐵)))) |
40 | 39 | adantr 274 |
. . 3
⊢ ((((𝐴 ∈ P ∧
𝐺 ∈ (1st
‘𝐴)) ∧ (𝐵 ∈ P ∧
𝐻 ∈ (1st
‘𝐵))) ∧ 𝑋 ∈ Q) →
((𝑋
·Q (*Q‘𝐻)) ∈ (1st
‘𝐴) → ((𝑋
·Q (*Q‘𝐻))
·Q 𝐻) ∈ (1st ‘(𝐴
·P 𝐵)))) |
41 | 32, 40 | syld 45 |
. 2
⊢ ((((𝐴 ∈ P ∧
𝐺 ∈ (1st
‘𝐴)) ∧ (𝐵 ∈ P ∧
𝐻 ∈ (1st
‘𝐵))) ∧ 𝑋 ∈ Q) →
(𝑋
<Q (𝐺 ·Q 𝐻) → ((𝑋 ·Q
(*Q‘𝐻)) ·Q 𝐻) ∈ (1st
‘(𝐴
·P 𝐵)))) |
42 | | mulassnqg 7339 |
. . . . 5
⊢ ((𝑋 ∈ Q ∧
(*Q‘𝐻) ∈ Q ∧ 𝐻 ∈ Q) →
((𝑋
·Q (*Q‘𝐻))
·Q 𝐻) = (𝑋 ·Q
((*Q‘𝐻) ·Q 𝐻))) |
43 | 3, 15, 11, 42 | syl3anc 1233 |
. . . 4
⊢ ((((𝐴 ∈ P ∧
𝐺 ∈ (1st
‘𝐴)) ∧ (𝐵 ∈ P ∧
𝐻 ∈ (1st
‘𝐵))) ∧ 𝑋 ∈ Q) →
((𝑋
·Q (*Q‘𝐻))
·Q 𝐻) = (𝑋 ·Q
((*Q‘𝐻) ·Q 𝐻))) |
44 | | mulcomnqg 7338 |
. . . . . . 7
⊢
(((*Q‘𝐻) ∈ Q ∧ 𝐻 ∈ Q) →
((*Q‘𝐻) ·Q 𝐻) = (𝐻 ·Q
(*Q‘𝐻))) |
45 | 15, 11, 44 | syl2anc 409 |
. . . . . 6
⊢ ((((𝐴 ∈ P ∧
𝐺 ∈ (1st
‘𝐴)) ∧ (𝐵 ∈ P ∧
𝐻 ∈ (1st
‘𝐵))) ∧ 𝑋 ∈ Q) →
((*Q‘𝐻) ·Q 𝐻) = (𝐻 ·Q
(*Q‘𝐻))) |
46 | 11, 21 | syl 14 |
. . . . . 6
⊢ ((((𝐴 ∈ P ∧
𝐺 ∈ (1st
‘𝐴)) ∧ (𝐵 ∈ P ∧
𝐻 ∈ (1st
‘𝐵))) ∧ 𝑋 ∈ Q) →
(𝐻
·Q (*Q‘𝐻)) =
1Q) |
47 | 45, 46 | eqtrd 2203 |
. . . . 5
⊢ ((((𝐴 ∈ P ∧
𝐺 ∈ (1st
‘𝐴)) ∧ (𝐵 ∈ P ∧
𝐻 ∈ (1st
‘𝐵))) ∧ 𝑋 ∈ Q) →
((*Q‘𝐻) ·Q 𝐻) =
1Q) |
48 | 47 | oveq2d 5867 |
. . . 4
⊢ ((((𝐴 ∈ P ∧
𝐺 ∈ (1st
‘𝐴)) ∧ (𝐵 ∈ P ∧
𝐻 ∈ (1st
‘𝐵))) ∧ 𝑋 ∈ Q) →
(𝑋
·Q ((*Q‘𝐻)
·Q 𝐻)) = (𝑋 ·Q
1Q)) |
49 | | mulidnq 7344 |
. . . . 5
⊢ (𝑋 ∈ Q →
(𝑋
·Q 1Q) = 𝑋) |
50 | 49 | adantl 275 |
. . . 4
⊢ ((((𝐴 ∈ P ∧
𝐺 ∈ (1st
‘𝐴)) ∧ (𝐵 ∈ P ∧
𝐻 ∈ (1st
‘𝐵))) ∧ 𝑋 ∈ Q) →
(𝑋
·Q 1Q) = 𝑋) |
51 | 43, 48, 50 | 3eqtrd 2207 |
. . 3
⊢ ((((𝐴 ∈ P ∧
𝐺 ∈ (1st
‘𝐴)) ∧ (𝐵 ∈ P ∧
𝐻 ∈ (1st
‘𝐵))) ∧ 𝑋 ∈ Q) →
((𝑋
·Q (*Q‘𝐻))
·Q 𝐻) = 𝑋) |
52 | 51 | eleq1d 2239 |
. 2
⊢ ((((𝐴 ∈ P ∧
𝐺 ∈ (1st
‘𝐴)) ∧ (𝐵 ∈ P ∧
𝐻 ∈ (1st
‘𝐵))) ∧ 𝑋 ∈ Q) →
(((𝑋
·Q (*Q‘𝐻))
·Q 𝐻) ∈ (1st ‘(𝐴
·P 𝐵)) ↔ 𝑋 ∈ (1st ‘(𝐴
·P 𝐵)))) |
53 | 41, 52 | sylibd 148 |
1
⊢ ((((𝐴 ∈ P ∧
𝐺 ∈ (1st
‘𝐴)) ∧ (𝐵 ∈ P ∧
𝐻 ∈ (1st
‘𝐵))) ∧ 𝑋 ∈ Q) →
(𝑋
<Q (𝐺 ·Q 𝐻) → 𝑋 ∈ (1st ‘(𝐴
·P 𝐵)))) |