Step | Hyp | Ref
| Expression |
1 | | ltmnqg 6385 |
. . . . . . 7
⊢
((y ∈ Q ∧ z ∈ Q ∧ w ∈ Q) → (y <Q z ↔ (w
·Q y)
<Q (w
·Q z))) |
2 | 1 | adantl 262 |
. . . . . 6
⊢
(((((A ∈ P ∧ 𝐺 ∈
(2nd ‘A)) ∧ (B ∈ P ∧ 𝐻 ∈
(2nd ‘B))) ∧ 𝑋 ∈
Q) ∧ (y ∈
Q ∧ z ∈
Q ∧ w ∈
Q)) → (y
<Q z ↔
(w ·Q
y) <Q (w ·Q z))) |
3 | | prop 6458 |
. . . . . . . . 9
⊢ (A ∈
P → 〈(1st ‘A), (2nd ‘A)〉 ∈
P) |
4 | | elprnqu 6465 |
. . . . . . . . 9
⊢
((〈(1st ‘A),
(2nd ‘A)〉 ∈ P ∧ 𝐺 ∈
(2nd ‘A)) → 𝐺 ∈ Q) |
5 | 3, 4 | sylan 267 |
. . . . . . . 8
⊢
((A ∈ P ∧ 𝐺 ∈
(2nd ‘A)) → 𝐺 ∈ Q) |
6 | 5 | ad2antrr 457 |
. . . . . . 7
⊢
((((A ∈ P ∧ 𝐺 ∈
(2nd ‘A)) ∧ (B ∈ P ∧ 𝐻 ∈
(2nd ‘B))) ∧ 𝑋 ∈
Q) → 𝐺
∈ Q) |
7 | | prop 6458 |
. . . . . . . . 9
⊢ (B ∈
P → 〈(1st ‘B), (2nd ‘B)〉 ∈
P) |
8 | | elprnqu 6465 |
. . . . . . . . 9
⊢
((〈(1st ‘B),
(2nd ‘B)〉 ∈ P ∧ 𝐻 ∈
(2nd ‘B)) → 𝐻 ∈ Q) |
9 | 7, 8 | sylan 267 |
. . . . . . . 8
⊢
((B ∈ P ∧ 𝐻 ∈
(2nd ‘B)) → 𝐻 ∈ Q) |
10 | 9 | ad2antlr 458 |
. . . . . . 7
⊢
((((A ∈ P ∧ 𝐺 ∈
(2nd ‘A)) ∧ (B ∈ P ∧ 𝐻 ∈
(2nd ‘B))) ∧ 𝑋 ∈
Q) → 𝐻
∈ Q) |
11 | | mulclnq 6360 |
. . . . . . 7
⊢ ((𝐺 ∈ Q ∧ 𝐻 ∈
Q) → (𝐺
·Q 𝐻) ∈
Q) |
12 | 6, 10, 11 | syl2anc 391 |
. . . . . 6
⊢
((((A ∈ P ∧ 𝐺 ∈
(2nd ‘A)) ∧ (B ∈ P ∧ 𝐻 ∈
(2nd ‘B))) ∧ 𝑋 ∈
Q) → (𝐺
·Q 𝐻) ∈
Q) |
13 | | simpr 103 |
. . . . . 6
⊢
((((A ∈ P ∧ 𝐺 ∈
(2nd ‘A)) ∧ (B ∈ P ∧ 𝐻 ∈
(2nd ‘B))) ∧ 𝑋 ∈
Q) → 𝑋
∈ Q) |
14 | | recclnq 6376 |
. . . . . . 7
⊢ (𝐻 ∈ Q →
(*Q‘𝐻) ∈
Q) |
15 | 10, 14 | syl 14 |
. . . . . 6
⊢
((((A ∈ P ∧ 𝐺 ∈
(2nd ‘A)) ∧ (B ∈ P ∧ 𝐻 ∈
(2nd ‘B))) ∧ 𝑋 ∈
Q) → (*Q‘𝐻) ∈
Q) |
16 | | mulcomnqg 6367 |
. . . . . . 7
⊢
((y ∈ Q ∧ z ∈ Q) → (y ·Q z) = (z
·Q y)) |
17 | 16 | adantl 262 |
. . . . . 6
⊢
(((((A ∈ P ∧ 𝐺 ∈
(2nd ‘A)) ∧ (B ∈ P ∧ 𝐻 ∈
(2nd ‘B))) ∧ 𝑋 ∈
Q) ∧ (y ∈
Q ∧ z ∈
Q)) → (y
·Q z) =
(z ·Q
y)) |
18 | 2, 12, 13, 15, 17 | caovord2d 5612 |
. . . . 5
⊢
((((A ∈ P ∧ 𝐺 ∈
(2nd ‘A)) ∧ (B ∈ P ∧ 𝐻 ∈
(2nd ‘B))) ∧ 𝑋 ∈
Q) → ((𝐺
·Q 𝐻) <Q 𝑋 ↔ ((𝐺 ·Q 𝐻)
·Q (*Q‘𝐻))
<Q (𝑋 ·Q
(*Q‘𝐻)))) |
19 | | mulassnqg 6368 |
. . . . . . . 8
⊢ ((𝐺 ∈ Q ∧ 𝐻 ∈
Q ∧
(*Q‘𝐻) ∈
Q) → ((𝐺
·Q 𝐻) ·Q
(*Q‘𝐻)) = (𝐺 ·Q (𝐻
·Q (*Q‘𝐻)))) |
20 | 6, 10, 15, 19 | syl3anc 1134 |
. . . . . . 7
⊢
((((A ∈ P ∧ 𝐺 ∈
(2nd ‘A)) ∧ (B ∈ P ∧ 𝐻 ∈
(2nd ‘B))) ∧ 𝑋 ∈
Q) → ((𝐺
·Q 𝐻) ·Q
(*Q‘𝐻)) = (𝐺 ·Q (𝐻
·Q (*Q‘𝐻)))) |
21 | | recidnq 6377 |
. . . . . . . . 9
⊢ (𝐻 ∈ Q → (𝐻 ·Q
(*Q‘𝐻)) =
1Q) |
22 | 21 | oveq2d 5471 |
. . . . . . . 8
⊢ (𝐻 ∈ Q → (𝐺 ·Q (𝐻
·Q (*Q‘𝐻))) = (𝐺 ·Q
1Q)) |
23 | 10, 22 | syl 14 |
. . . . . . 7
⊢
((((A ∈ P ∧ 𝐺 ∈
(2nd ‘A)) ∧ (B ∈ P ∧ 𝐻 ∈
(2nd ‘B))) ∧ 𝑋 ∈
Q) → (𝐺
·Q (𝐻 ·Q
(*Q‘𝐻))) = (𝐺 ·Q
1Q)) |
24 | | mulidnq 6373 |
. . . . . . . 8
⊢ (𝐺 ∈ Q → (𝐺 ·Q
1Q) = 𝐺) |
25 | 6, 24 | syl 14 |
. . . . . . 7
⊢
((((A ∈ P ∧ 𝐺 ∈
(2nd ‘A)) ∧ (B ∈ P ∧ 𝐻 ∈
(2nd ‘B))) ∧ 𝑋 ∈
Q) → (𝐺
·Q 1Q) = 𝐺) |
26 | 20, 23, 25 | 3eqtrd 2073 |
. . . . . 6
⊢
((((A ∈ P ∧ 𝐺 ∈
(2nd ‘A)) ∧ (B ∈ P ∧ 𝐻 ∈
(2nd ‘B))) ∧ 𝑋 ∈
Q) → ((𝐺
·Q 𝐻) ·Q
(*Q‘𝐻)) = 𝐺) |
27 | 26 | breq1d 3765 |
. . . . 5
⊢
((((A ∈ P ∧ 𝐺 ∈
(2nd ‘A)) ∧ (B ∈ P ∧ 𝐻 ∈
(2nd ‘B))) ∧ 𝑋 ∈
Q) → (((𝐺 ·Q 𝐻)
·Q (*Q‘𝐻))
<Q (𝑋 ·Q
(*Q‘𝐻)) ↔ 𝐺 <Q (𝑋
·Q (*Q‘𝐻)))) |
28 | 18, 27 | bitrd 177 |
. . . 4
⊢
((((A ∈ P ∧ 𝐺 ∈
(2nd ‘A)) ∧ (B ∈ P ∧ 𝐻 ∈
(2nd ‘B))) ∧ 𝑋 ∈
Q) → ((𝐺
·Q 𝐻) <Q 𝑋 ↔ 𝐺 <Q (𝑋
·Q (*Q‘𝐻)))) |
29 | | prcunqu 6468 |
. . . . . 6
⊢
((〈(1st ‘A),
(2nd ‘A)〉 ∈ P ∧ 𝐺 ∈
(2nd ‘A)) → (𝐺 <Q
(𝑋
·Q (*Q‘𝐻)) → (𝑋 ·Q
(*Q‘𝐻)) ∈
(2nd ‘A))) |
30 | 3, 29 | sylan 267 |
. . . . 5
⊢
((A ∈ P ∧ 𝐺 ∈
(2nd ‘A)) → (𝐺 <Q
(𝑋
·Q (*Q‘𝐻)) → (𝑋 ·Q
(*Q‘𝐻)) ∈
(2nd ‘A))) |
31 | 30 | ad2antrr 457 |
. . . 4
⊢
((((A ∈ P ∧ 𝐺 ∈
(2nd ‘A)) ∧ (B ∈ P ∧ 𝐻 ∈
(2nd ‘B))) ∧ 𝑋 ∈
Q) → (𝐺
<Q (𝑋 ·Q
(*Q‘𝐻)) → (𝑋 ·Q
(*Q‘𝐻)) ∈
(2nd ‘A))) |
32 | 28, 31 | sylbid 139 |
. . 3
⊢
((((A ∈ P ∧ 𝐺 ∈
(2nd ‘A)) ∧ (B ∈ P ∧ 𝐻 ∈
(2nd ‘B))) ∧ 𝑋 ∈
Q) → ((𝐺
·Q 𝐻) <Q 𝑋 → (𝑋 ·Q
(*Q‘𝐻)) ∈
(2nd ‘A))) |
33 | | df-imp 6452 |
. . . . . . . . 9
⊢
·P = (w
∈ P, v ∈
P ↦ 〈{x ∈ Q ∣ ∃y ∈ Q ∃z ∈ Q (y ∈
(1st ‘w) ∧ z ∈ (1st ‘v) ∧ x = (y
·Q z))},
{x ∈
Q ∣ ∃y ∈
Q ∃z ∈
Q (y ∈ (2nd ‘w) ∧ z ∈
(2nd ‘v) ∧ x = (y ·Q z))}〉) |
34 | | mulclnq 6360 |
. . . . . . . . 9
⊢
((y ∈ Q ∧ z ∈ Q) → (y ·Q z) ∈
Q) |
35 | 33, 34 | genppreclu 6498 |
. . . . . . . 8
⊢
((A ∈ P ∧ B ∈ P) → (((𝑋 ·Q
(*Q‘𝐻)) ∈
(2nd ‘A) ∧ 𝐻 ∈
(2nd ‘B)) → ((𝑋
·Q (*Q‘𝐻))
·Q 𝐻) ∈
(2nd ‘(A
·P B)))) |
36 | 35 | exp4b 349 |
. . . . . . 7
⊢ (A ∈
P → (B ∈ P → ((𝑋 ·Q
(*Q‘𝐻)) ∈
(2nd ‘A) → (𝐻 ∈ (2nd ‘B) → ((𝑋 ·Q
(*Q‘𝐻)) ·Q 𝐻) ∈ (2nd ‘(A ·P B)))))) |
37 | 36 | com34 77 |
. . . . . 6
⊢ (A ∈
P → (B ∈ P → (𝐻 ∈
(2nd ‘B) → ((𝑋
·Q (*Q‘𝐻)) ∈ (2nd ‘A) → ((𝑋 ·Q
(*Q‘𝐻)) ·Q 𝐻) ∈ (2nd ‘(A ·P B)))))) |
38 | 37 | imp32 244 |
. . . . 5
⊢
((A ∈ P ∧ (B ∈ P ∧ 𝐻 ∈
(2nd ‘B))) → ((𝑋
·Q (*Q‘𝐻)) ∈ (2nd ‘A) → ((𝑋 ·Q
(*Q‘𝐻)) ·Q 𝐻) ∈ (2nd ‘(A ·P B)))) |
39 | 38 | adantlr 446 |
. . . 4
⊢
(((A ∈ P ∧ 𝐺 ∈
(2nd ‘A)) ∧ (B ∈ P ∧ 𝐻 ∈
(2nd ‘B))) → ((𝑋
·Q (*Q‘𝐻)) ∈ (2nd ‘A) → ((𝑋 ·Q
(*Q‘𝐻)) ·Q 𝐻) ∈ (2nd ‘(A ·P B)))) |
40 | 39 | adantr 261 |
. . 3
⊢
((((A ∈ P ∧ 𝐺 ∈
(2nd ‘A)) ∧ (B ∈ P ∧ 𝐻 ∈
(2nd ‘B))) ∧ 𝑋 ∈
Q) → ((𝑋
·Q (*Q‘𝐻)) ∈ (2nd ‘A) → ((𝑋 ·Q
(*Q‘𝐻)) ·Q 𝐻) ∈ (2nd ‘(A ·P B)))) |
41 | 32, 40 | syld 40 |
. 2
⊢
((((A ∈ P ∧ 𝐺 ∈
(2nd ‘A)) ∧ (B ∈ P ∧ 𝐻 ∈
(2nd ‘B))) ∧ 𝑋 ∈
Q) → ((𝐺
·Q 𝐻) <Q 𝑋 → ((𝑋 ·Q
(*Q‘𝐻)) ·Q 𝐻) ∈ (2nd ‘(A ·P B)))) |
42 | | mulassnqg 6368 |
. . . . 5
⊢ ((𝑋 ∈ Q ∧ (*Q‘𝐻) ∈ Q ∧ 𝐻 ∈
Q) → ((𝑋
·Q (*Q‘𝐻))
·Q 𝐻) = (𝑋 ·Q
((*Q‘𝐻) ·Q 𝐻))) |
43 | 13, 15, 10, 42 | syl3anc 1134 |
. . . 4
⊢
((((A ∈ P ∧ 𝐺 ∈
(2nd ‘A)) ∧ (B ∈ P ∧ 𝐻 ∈
(2nd ‘B))) ∧ 𝑋 ∈
Q) → ((𝑋
·Q (*Q‘𝐻))
·Q 𝐻) = (𝑋 ·Q
((*Q‘𝐻) ·Q 𝐻))) |
44 | | mulcomnqg 6367 |
. . . . . . 7
⊢
(((*Q‘𝐻) ∈
Q ∧ 𝐻 ∈
Q) → ((*Q‘𝐻) ·Q 𝐻) = (𝐻 ·Q
(*Q‘𝐻))) |
45 | 15, 10, 44 | syl2anc 391 |
. . . . . 6
⊢
((((A ∈ P ∧ 𝐺 ∈
(2nd ‘A)) ∧ (B ∈ P ∧ 𝐻 ∈
(2nd ‘B))) ∧ 𝑋 ∈
Q) → ((*Q‘𝐻) ·Q 𝐻) = (𝐻 ·Q
(*Q‘𝐻))) |
46 | 10, 21 | syl 14 |
. . . . . 6
⊢
((((A ∈ P ∧ 𝐺 ∈
(2nd ‘A)) ∧ (B ∈ P ∧ 𝐻 ∈
(2nd ‘B))) ∧ 𝑋 ∈
Q) → (𝐻
·Q (*Q‘𝐻)) =
1Q) |
47 | 45, 46 | eqtrd 2069 |
. . . . 5
⊢
((((A ∈ P ∧ 𝐺 ∈
(2nd ‘A)) ∧ (B ∈ P ∧ 𝐻 ∈
(2nd ‘B))) ∧ 𝑋 ∈
Q) → ((*Q‘𝐻) ·Q 𝐻) =
1Q) |
48 | 47 | oveq2d 5471 |
. . . 4
⊢
((((A ∈ P ∧ 𝐺 ∈
(2nd ‘A)) ∧ (B ∈ P ∧ 𝐻 ∈
(2nd ‘B))) ∧ 𝑋 ∈
Q) → (𝑋
·Q ((*Q‘𝐻)
·Q 𝐻)) = (𝑋 ·Q
1Q)) |
49 | | mulidnq 6373 |
. . . . 5
⊢ (𝑋 ∈ Q → (𝑋 ·Q
1Q) = 𝑋) |
50 | 49 | adantl 262 |
. . . 4
⊢
((((A ∈ P ∧ 𝐺 ∈
(2nd ‘A)) ∧ (B ∈ P ∧ 𝐻 ∈
(2nd ‘B))) ∧ 𝑋 ∈
Q) → (𝑋
·Q 1Q) = 𝑋) |
51 | 43, 48, 50 | 3eqtrd 2073 |
. . 3
⊢
((((A ∈ P ∧ 𝐺 ∈
(2nd ‘A)) ∧ (B ∈ P ∧ 𝐻 ∈
(2nd ‘B))) ∧ 𝑋 ∈
Q) → ((𝑋
·Q (*Q‘𝐻))
·Q 𝐻) = 𝑋) |
52 | 51 | eleq1d 2103 |
. 2
⊢
((((A ∈ P ∧ 𝐺 ∈
(2nd ‘A)) ∧ (B ∈ P ∧ 𝐻 ∈
(2nd ‘B))) ∧ 𝑋 ∈
Q) → (((𝑋 ·Q
(*Q‘𝐻)) ·Q 𝐻) ∈ (2nd ‘(A ·P B)) ↔ 𝑋 ∈
(2nd ‘(A
·P B)))) |
53 | 41, 52 | sylibd 138 |
1
⊢
((((A ∈ P ∧ 𝐺 ∈
(2nd ‘A)) ∧ (B ∈ P ∧ 𝐻 ∈
(2nd ‘B))) ∧ 𝑋 ∈
Q) → ((𝐺
·Q 𝐻) <Q 𝑋 → 𝑋 ∈
(2nd ‘(A
·P B)))) |