Intuitionistic Logic Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  ILE Home  >  Th. List  >  recexprlem1ssu GIF version

Theorem recexprlem1ssu 6732
 Description: The upper cut of one is a subset of the upper cut of 𝐴 ·P 𝐵. Lemma for recexpr 6736. (Contributed by Jim Kingdon, 27-Dec-2019.)
Hypothesis
Ref Expression
recexpr.1 𝐵 = ⟨{𝑥 ∣ ∃𝑦(𝑥 <Q 𝑦 ∧ (*Q𝑦) ∈ (2nd𝐴))}, {𝑥 ∣ ∃𝑦(𝑦 <Q 𝑥 ∧ (*Q𝑦) ∈ (1st𝐴))}⟩
Assertion
Ref Expression
recexprlem1ssu (𝐴P → (2nd ‘1P) ⊆ (2nd ‘(𝐴 ·P 𝐵)))
Distinct variable groups:   𝑥,𝑦,𝐴   𝑥,𝐵,𝑦

Proof of Theorem recexprlem1ssu
Dummy variables 𝑧 𝑤 𝑣 𝑢 𝑓 𝑔 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 1pru 6654 . . . 4 (2nd ‘1P) = {𝑤 ∣ 1Q <Q 𝑤}
21abeq2i 2148 . . 3 (𝑤 ∈ (2nd ‘1P) ↔ 1Q <Q 𝑤)
3 prop 6573 . . . . . 6 (𝐴P → ⟨(1st𝐴), (2nd𝐴)⟩ ∈ P)
4 prmuloc2 6665 . . . . . 6 ((⟨(1st𝐴), (2nd𝐴)⟩ ∈ P ∧ 1Q <Q 𝑤) → ∃𝑣 ∈ (1st𝐴)(𝑣 ·Q 𝑤) ∈ (2nd𝐴))
53, 4sylan 267 . . . . 5 ((𝐴P ∧ 1Q <Q 𝑤) → ∃𝑣 ∈ (1st𝐴)(𝑣 ·Q 𝑤) ∈ (2nd𝐴))
6 prnminu 6587 . . . . . . . 8 ((⟨(1st𝐴), (2nd𝐴)⟩ ∈ P ∧ (𝑣 ·Q 𝑤) ∈ (2nd𝐴)) → ∃𝑧 ∈ (2nd𝐴)𝑧 <Q (𝑣 ·Q 𝑤))
73, 6sylan 267 . . . . . . 7 ((𝐴P ∧ (𝑣 ·Q 𝑤) ∈ (2nd𝐴)) → ∃𝑧 ∈ (2nd𝐴)𝑧 <Q (𝑣 ·Q 𝑤))
87ad2ant2rl 480 . . . . . 6 (((𝐴P ∧ 1Q <Q 𝑤) ∧ (𝑣 ∈ (1st𝐴) ∧ (𝑣 ·Q 𝑤) ∈ (2nd𝐴))) → ∃𝑧 ∈ (2nd𝐴)𝑧 <Q (𝑣 ·Q 𝑤))
9 simp3 906 . . . . . . . . . . 11 (((𝐴P ∧ 1Q <Q 𝑤) ∧ (𝑣 ∈ (1st𝐴) ∧ (𝑣 ·Q 𝑤) ∈ (2nd𝐴)) ∧ 𝑧 <Q (𝑣 ·Q 𝑤)) → 𝑧 <Q (𝑣 ·Q 𝑤))
10 simp2l 930 . . . . . . . . . . . 12 (((𝐴P ∧ 1Q <Q 𝑤) ∧ (𝑣 ∈ (1st𝐴) ∧ (𝑣 ·Q 𝑤) ∈ (2nd𝐴)) ∧ 𝑧 <Q (𝑣 ·Q 𝑤)) → 𝑣 ∈ (1st𝐴))
11 elprnql 6579 . . . . . . . . . . . . . . . . . 18 ((⟨(1st𝐴), (2nd𝐴)⟩ ∈ P𝑣 ∈ (1st𝐴)) → 𝑣Q)
123, 11sylan 267 . . . . . . . . . . . . . . . . 17 ((𝐴P𝑣 ∈ (1st𝐴)) → 𝑣Q)
1312ad2ant2r 478 . . . . . . . . . . . . . . . 16 (((𝐴P ∧ 1Q <Q 𝑤) ∧ (𝑣 ∈ (1st𝐴) ∧ (𝑣 ·Q 𝑤) ∈ (2nd𝐴))) → 𝑣Q)
14133adant3 924 . . . . . . . . . . . . . . 15 (((𝐴P ∧ 1Q <Q 𝑤) ∧ (𝑣 ∈ (1st𝐴) ∧ (𝑣 ·Q 𝑤) ∈ (2nd𝐴)) ∧ 𝑧 <Q (𝑣 ·Q 𝑤)) → 𝑣Q)
15 simp1r 929 . . . . . . . . . . . . . . . 16 (((𝐴P ∧ 1Q <Q 𝑤) ∧ (𝑣 ∈ (1st𝐴) ∧ (𝑣 ·Q 𝑤) ∈ (2nd𝐴)) ∧ 𝑧 <Q (𝑣 ·Q 𝑤)) → 1Q <Q 𝑤)
16 ltrelnq 6463 . . . . . . . . . . . . . . . . . 18 <Q ⊆ (Q × Q)
1716brel 4392 . . . . . . . . . . . . . . . . 17 (1Q <Q 𝑤 → (1QQ𝑤Q))
1817simprd 107 . . . . . . . . . . . . . . . 16 (1Q <Q 𝑤𝑤Q)
1915, 18syl 14 . . . . . . . . . . . . . . 15 (((𝐴P ∧ 1Q <Q 𝑤) ∧ (𝑣 ∈ (1st𝐴) ∧ (𝑣 ·Q 𝑤) ∈ (2nd𝐴)) ∧ 𝑧 <Q (𝑣 ·Q 𝑤)) → 𝑤Q)
20 recclnq 6490 . . . . . . . . . . . . . . . 16 (𝑤Q → (*Q𝑤) ∈ Q)
2119, 20syl 14 . . . . . . . . . . . . . . 15 (((𝐴P ∧ 1Q <Q 𝑤) ∧ (𝑣 ∈ (1st𝐴) ∧ (𝑣 ·Q 𝑤) ∈ (2nd𝐴)) ∧ 𝑧 <Q (𝑣 ·Q 𝑤)) → (*Q𝑤) ∈ Q)
22 mulassnqg 6482 . . . . . . . . . . . . . . 15 ((𝑣Q𝑤Q ∧ (*Q𝑤) ∈ Q) → ((𝑣 ·Q 𝑤) ·Q (*Q𝑤)) = (𝑣 ·Q (𝑤 ·Q (*Q𝑤))))
2314, 19, 21, 22syl3anc 1135 . . . . . . . . . . . . . 14 (((𝐴P ∧ 1Q <Q 𝑤) ∧ (𝑣 ∈ (1st𝐴) ∧ (𝑣 ·Q 𝑤) ∈ (2nd𝐴)) ∧ 𝑧 <Q (𝑣 ·Q 𝑤)) → ((𝑣 ·Q 𝑤) ·Q (*Q𝑤)) = (𝑣 ·Q (𝑤 ·Q (*Q𝑤))))
24 recidnq 6491 . . . . . . . . . . . . . . . 16 (𝑤Q → (𝑤 ·Q (*Q𝑤)) = 1Q)
2519, 24syl 14 . . . . . . . . . . . . . . 15 (((𝐴P ∧ 1Q <Q 𝑤) ∧ (𝑣 ∈ (1st𝐴) ∧ (𝑣 ·Q 𝑤) ∈ (2nd𝐴)) ∧ 𝑧 <Q (𝑣 ·Q 𝑤)) → (𝑤 ·Q (*Q𝑤)) = 1Q)
2625oveq2d 5528 . . . . . . . . . . . . . 14 (((𝐴P ∧ 1Q <Q 𝑤) ∧ (𝑣 ∈ (1st𝐴) ∧ (𝑣 ·Q 𝑤) ∈ (2nd𝐴)) ∧ 𝑧 <Q (𝑣 ·Q 𝑤)) → (𝑣 ·Q (𝑤 ·Q (*Q𝑤))) = (𝑣 ·Q 1Q))
27 mulidnq 6487 . . . . . . . . . . . . . . 15 (𝑣Q → (𝑣 ·Q 1Q) = 𝑣)
2814, 27syl 14 . . . . . . . . . . . . . 14 (((𝐴P ∧ 1Q <Q 𝑤) ∧ (𝑣 ∈ (1st𝐴) ∧ (𝑣 ·Q 𝑤) ∈ (2nd𝐴)) ∧ 𝑧 <Q (𝑣 ·Q 𝑤)) → (𝑣 ·Q 1Q) = 𝑣)
2923, 26, 283eqtrd 2076 . . . . . . . . . . . . 13 (((𝐴P ∧ 1Q <Q 𝑤) ∧ (𝑣 ∈ (1st𝐴) ∧ (𝑣 ·Q 𝑤) ∈ (2nd𝐴)) ∧ 𝑧 <Q (𝑣 ·Q 𝑤)) → ((𝑣 ·Q 𝑤) ·Q (*Q𝑤)) = 𝑣)
3029eleq1d 2106 . . . . . . . . . . . 12 (((𝐴P ∧ 1Q <Q 𝑤) ∧ (𝑣 ∈ (1st𝐴) ∧ (𝑣 ·Q 𝑤) ∈ (2nd𝐴)) ∧ 𝑧 <Q (𝑣 ·Q 𝑤)) → (((𝑣 ·Q 𝑤) ·Q (*Q𝑤)) ∈ (1st𝐴) ↔ 𝑣 ∈ (1st𝐴)))
3110, 30mpbird 156 . . . . . . . . . . 11 (((𝐴P ∧ 1Q <Q 𝑤) ∧ (𝑣 ∈ (1st𝐴) ∧ (𝑣 ·Q 𝑤) ∈ (2nd𝐴)) ∧ 𝑧 <Q (𝑣 ·Q 𝑤)) → ((𝑣 ·Q 𝑤) ·Q (*Q𝑤)) ∈ (1st𝐴))
32 ltrnqi 6519 . . . . . . . . . . . . 13 (𝑧 <Q (𝑣 ·Q 𝑤) → (*Q‘(𝑣 ·Q 𝑤)) <Q (*Q𝑧))
33 ltmnqg 6499 . . . . . . . . . . . . . . 15 ((𝑓Q𝑔QQ) → (𝑓 <Q 𝑔 ↔ ( ·Q 𝑓) <Q ( ·Q 𝑔)))
3433adantl 262 . . . . . . . . . . . . . 14 ((((𝐴P ∧ 1Q <Q 𝑤) ∧ (𝑣 ∈ (1st𝐴) ∧ (𝑣 ·Q 𝑤) ∈ (2nd𝐴)) ∧ 𝑧 <Q (𝑣 ·Q 𝑤)) ∧ (𝑓Q𝑔QQ)) → (𝑓 <Q 𝑔 ↔ ( ·Q 𝑓) <Q ( ·Q 𝑔)))
35 mulclnq 6474 . . . . . . . . . . . . . . . 16 ((𝑣Q𝑤Q) → (𝑣 ·Q 𝑤) ∈ Q)
3614, 19, 35syl2anc 391 . . . . . . . . . . . . . . 15 (((𝐴P ∧ 1Q <Q 𝑤) ∧ (𝑣 ∈ (1st𝐴) ∧ (𝑣 ·Q 𝑤) ∈ (2nd𝐴)) ∧ 𝑧 <Q (𝑣 ·Q 𝑤)) → (𝑣 ·Q 𝑤) ∈ Q)
37 recclnq 6490 . . . . . . . . . . . . . . 15 ((𝑣 ·Q 𝑤) ∈ Q → (*Q‘(𝑣 ·Q 𝑤)) ∈ Q)
3836, 37syl 14 . . . . . . . . . . . . . 14 (((𝐴P ∧ 1Q <Q 𝑤) ∧ (𝑣 ∈ (1st𝐴) ∧ (𝑣 ·Q 𝑤) ∈ (2nd𝐴)) ∧ 𝑧 <Q (𝑣 ·Q 𝑤)) → (*Q‘(𝑣 ·Q 𝑤)) ∈ Q)
3916brel 4392 . . . . . . . . . . . . . . . . 17 (𝑧 <Q (𝑣 ·Q 𝑤) → (𝑧Q ∧ (𝑣 ·Q 𝑤) ∈ Q))
4039simpld 105 . . . . . . . . . . . . . . . 16 (𝑧 <Q (𝑣 ·Q 𝑤) → 𝑧Q)
419, 40syl 14 . . . . . . . . . . . . . . 15 (((𝐴P ∧ 1Q <Q 𝑤) ∧ (𝑣 ∈ (1st𝐴) ∧ (𝑣 ·Q 𝑤) ∈ (2nd𝐴)) ∧ 𝑧 <Q (𝑣 ·Q 𝑤)) → 𝑧Q)
42 recclnq 6490 . . . . . . . . . . . . . . 15 (𝑧Q → (*Q𝑧) ∈ Q)
4341, 42syl 14 . . . . . . . . . . . . . 14 (((𝐴P ∧ 1Q <Q 𝑤) ∧ (𝑣 ∈ (1st𝐴) ∧ (𝑣 ·Q 𝑤) ∈ (2nd𝐴)) ∧ 𝑧 <Q (𝑣 ·Q 𝑤)) → (*Q𝑧) ∈ Q)
44 mulcomnqg 6481 . . . . . . . . . . . . . . 15 ((𝑓Q𝑔Q) → (𝑓 ·Q 𝑔) = (𝑔 ·Q 𝑓))
4544adantl 262 . . . . . . . . . . . . . 14 ((((𝐴P ∧ 1Q <Q 𝑤) ∧ (𝑣 ∈ (1st𝐴) ∧ (𝑣 ·Q 𝑤) ∈ (2nd𝐴)) ∧ 𝑧 <Q (𝑣 ·Q 𝑤)) ∧ (𝑓Q𝑔Q)) → (𝑓 ·Q 𝑔) = (𝑔 ·Q 𝑓))
4634, 38, 43, 19, 45caovord2d 5670 . . . . . . . . . . . . 13 (((𝐴P ∧ 1Q <Q 𝑤) ∧ (𝑣 ∈ (1st𝐴) ∧ (𝑣 ·Q 𝑤) ∈ (2nd𝐴)) ∧ 𝑧 <Q (𝑣 ·Q 𝑤)) → ((*Q‘(𝑣 ·Q 𝑤)) <Q (*Q𝑧) ↔ ((*Q‘(𝑣 ·Q 𝑤)) ·Q 𝑤) <Q ((*Q𝑧) ·Q 𝑤)))
4732, 46syl5ib 143 . . . . . . . . . . . 12 (((𝐴P ∧ 1Q <Q 𝑤) ∧ (𝑣 ∈ (1st𝐴) ∧ (𝑣 ·Q 𝑤) ∈ (2nd𝐴)) ∧ 𝑧 <Q (𝑣 ·Q 𝑤)) → (𝑧 <Q (𝑣 ·Q 𝑤) → ((*Q‘(𝑣 ·Q 𝑤)) ·Q 𝑤) <Q ((*Q𝑧) ·Q 𝑤)))
48 1nq 6464 . . . . . . . . . . . . . . . . 17 1QQ
49 mulidnq 6487 . . . . . . . . . . . . . . . . 17 (1QQ → (1Q ·Q 1Q) = 1Q)
5048, 49ax-mp 7 . . . . . . . . . . . . . . . 16 (1Q ·Q 1Q) = 1Q
51 mulcomnqg 6481 . . . . . . . . . . . . . . . . . . . . 21 (((𝑣 ·Q 𝑤) ∈ Q ∧ (*Q‘(𝑣 ·Q 𝑤)) ∈ Q) → ((𝑣 ·Q 𝑤) ·Q (*Q‘(𝑣 ·Q 𝑤))) = ((*Q‘(𝑣 ·Q 𝑤)) ·Q (𝑣 ·Q 𝑤)))
5237, 51mpdan 398 . . . . . . . . . . . . . . . . . . . 20 ((𝑣 ·Q 𝑤) ∈ Q → ((𝑣 ·Q 𝑤) ·Q (*Q‘(𝑣 ·Q 𝑤))) = ((*Q‘(𝑣 ·Q 𝑤)) ·Q (𝑣 ·Q 𝑤)))
53 recidnq 6491 . . . . . . . . . . . . . . . . . . . 20 ((𝑣 ·Q 𝑤) ∈ Q → ((𝑣 ·Q 𝑤) ·Q (*Q‘(𝑣 ·Q 𝑤))) = 1Q)
5452, 53eqtr3d 2074 . . . . . . . . . . . . . . . . . . 19 ((𝑣 ·Q 𝑤) ∈ Q → ((*Q‘(𝑣 ·Q 𝑤)) ·Q (𝑣 ·Q 𝑤)) = 1Q)
5554, 24oveqan12d 5531 . . . . . . . . . . . . . . . . . 18 (((𝑣 ·Q 𝑤) ∈ Q𝑤Q) → (((*Q‘(𝑣 ·Q 𝑤)) ·Q (𝑣 ·Q 𝑤)) ·Q (𝑤 ·Q (*Q𝑤))) = (1Q ·Q 1Q))
5636, 19, 55syl2anc 391 . . . . . . . . . . . . . . . . 17 (((𝐴P ∧ 1Q <Q 𝑤) ∧ (𝑣 ∈ (1st𝐴) ∧ (𝑣 ·Q 𝑤) ∈ (2nd𝐴)) ∧ 𝑧 <Q (𝑣 ·Q 𝑤)) → (((*Q‘(𝑣 ·Q 𝑤)) ·Q (𝑣 ·Q 𝑤)) ·Q (𝑤 ·Q (*Q𝑤))) = (1Q ·Q 1Q))
57 mulassnqg 6482 . . . . . . . . . . . . . . . . . . 19 ((𝑓Q𝑔QQ) → ((𝑓 ·Q 𝑔) ·Q ) = (𝑓 ·Q (𝑔 ·Q )))
5857adantl 262 . . . . . . . . . . . . . . . . . 18 ((((𝐴P ∧ 1Q <Q 𝑤) ∧ (𝑣 ∈ (1st𝐴) ∧ (𝑣 ·Q 𝑤) ∈ (2nd𝐴)) ∧ 𝑧 <Q (𝑣 ·Q 𝑤)) ∧ (𝑓Q𝑔QQ)) → ((𝑓 ·Q 𝑔) ·Q ) = (𝑓 ·Q (𝑔 ·Q )))
59 mulclnq 6474 . . . . . . . . . . . . . . . . . . 19 ((𝑓Q𝑔Q) → (𝑓 ·Q 𝑔) ∈ Q)
6059adantl 262 . . . . . . . . . . . . . . . . . 18 ((((𝐴P ∧ 1Q <Q 𝑤) ∧ (𝑣 ∈ (1st𝐴) ∧ (𝑣 ·Q 𝑤) ∈ (2nd𝐴)) ∧ 𝑧 <Q (𝑣 ·Q 𝑤)) ∧ (𝑓Q𝑔Q)) → (𝑓 ·Q 𝑔) ∈ Q)
6138, 36, 19, 45, 58, 21, 60caov4d 5685 . . . . . . . . . . . . . . . . 17 (((𝐴P ∧ 1Q <Q 𝑤) ∧ (𝑣 ∈ (1st𝐴) ∧ (𝑣 ·Q 𝑤) ∈ (2nd𝐴)) ∧ 𝑧 <Q (𝑣 ·Q 𝑤)) → (((*Q‘(𝑣 ·Q 𝑤)) ·Q (𝑣 ·Q 𝑤)) ·Q (𝑤 ·Q (*Q𝑤))) = (((*Q‘(𝑣 ·Q 𝑤)) ·Q 𝑤) ·Q ((𝑣 ·Q 𝑤) ·Q (*Q𝑤))))
6256, 61eqtr3d 2074 . . . . . . . . . . . . . . . 16 (((𝐴P ∧ 1Q <Q 𝑤) ∧ (𝑣 ∈ (1st𝐴) ∧ (𝑣 ·Q 𝑤) ∈ (2nd𝐴)) ∧ 𝑧 <Q (𝑣 ·Q 𝑤)) → (1Q ·Q 1Q) = (((*Q‘(𝑣 ·Q 𝑤)) ·Q 𝑤) ·Q ((𝑣 ·Q 𝑤) ·Q (*Q𝑤))))
6350, 62syl5reqr 2087 . . . . . . . . . . . . . . 15 (((𝐴P ∧ 1Q <Q 𝑤) ∧ (𝑣 ∈ (1st𝐴) ∧ (𝑣 ·Q 𝑤) ∈ (2nd𝐴)) ∧ 𝑧 <Q (𝑣 ·Q 𝑤)) → (((*Q‘(𝑣 ·Q 𝑤)) ·Q 𝑤) ·Q ((𝑣 ·Q 𝑤) ·Q (*Q𝑤))) = 1Q)
6460, 38, 19caovcld 5654 . . . . . . . . . . . . . . . 16 (((𝐴P ∧ 1Q <Q 𝑤) ∧ (𝑣 ∈ (1st𝐴) ∧ (𝑣 ·Q 𝑤) ∈ (2nd𝐴)) ∧ 𝑧 <Q (𝑣 ·Q 𝑤)) → ((*Q‘(𝑣 ·Q 𝑤)) ·Q 𝑤) ∈ Q)
6560, 36, 21caovcld 5654 . . . . . . . . . . . . . . . 16 (((𝐴P ∧ 1Q <Q 𝑤) ∧ (𝑣 ∈ (1st𝐴) ∧ (𝑣 ·Q 𝑤) ∈ (2nd𝐴)) ∧ 𝑧 <Q (𝑣 ·Q 𝑤)) → ((𝑣 ·Q 𝑤) ·Q (*Q𝑤)) ∈ Q)
66 recmulnqg 6489 . . . . . . . . . . . . . . . 16 ((((*Q‘(𝑣 ·Q 𝑤)) ·Q 𝑤) ∈ Q ∧ ((𝑣 ·Q 𝑤) ·Q (*Q𝑤)) ∈ Q) → ((*Q‘((*Q‘(𝑣 ·Q 𝑤)) ·Q 𝑤)) = ((𝑣 ·Q 𝑤) ·Q (*Q𝑤)) ↔ (((*Q‘(𝑣 ·Q 𝑤)) ·Q 𝑤) ·Q ((𝑣 ·Q 𝑤) ·Q (*Q𝑤))) = 1Q))
6764, 65, 66syl2anc 391 . . . . . . . . . . . . . . 15 (((𝐴P ∧ 1Q <Q 𝑤) ∧ (𝑣 ∈ (1st𝐴) ∧ (𝑣 ·Q 𝑤) ∈ (2nd𝐴)) ∧ 𝑧 <Q (𝑣 ·Q 𝑤)) → ((*Q‘((*Q‘(𝑣 ·Q 𝑤)) ·Q 𝑤)) = ((𝑣 ·Q 𝑤) ·Q (*Q𝑤)) ↔ (((*Q‘(𝑣 ·Q 𝑤)) ·Q 𝑤) ·Q ((𝑣 ·Q 𝑤) ·Q (*Q𝑤))) = 1Q))
6863, 67mpbird 156 . . . . . . . . . . . . . 14 (((𝐴P ∧ 1Q <Q 𝑤) ∧ (𝑣 ∈ (1st𝐴) ∧ (𝑣 ·Q 𝑤) ∈ (2nd𝐴)) ∧ 𝑧 <Q (𝑣 ·Q 𝑤)) → (*Q‘((*Q‘(𝑣 ·Q 𝑤)) ·Q 𝑤)) = ((𝑣 ·Q 𝑤) ·Q (*Q𝑤)))
6968eleq1d 2106 . . . . . . . . . . . . 13 (((𝐴P ∧ 1Q <Q 𝑤) ∧ (𝑣 ∈ (1st𝐴) ∧ (𝑣 ·Q 𝑤) ∈ (2nd𝐴)) ∧ 𝑧 <Q (𝑣 ·Q 𝑤)) → ((*Q‘((*Q‘(𝑣 ·Q 𝑤)) ·Q 𝑤)) ∈ (1st𝐴) ↔ ((𝑣 ·Q 𝑤) ·Q (*Q𝑤)) ∈ (1st𝐴)))
7069biimprd 147 . . . . . . . . . . . 12 (((𝐴P ∧ 1Q <Q 𝑤) ∧ (𝑣 ∈ (1st𝐴) ∧ (𝑣 ·Q 𝑤) ∈ (2nd𝐴)) ∧ 𝑧 <Q (𝑣 ·Q 𝑤)) → (((𝑣 ·Q 𝑤) ·Q (*Q𝑤)) ∈ (1st𝐴) → (*Q‘((*Q‘(𝑣 ·Q 𝑤)) ·Q 𝑤)) ∈ (1st𝐴)))
71 breq1 3767 . . . . . . . . . . . . . . . 16 (𝑦 = ((*Q‘(𝑣 ·Q 𝑤)) ·Q 𝑤) → (𝑦 <Q ((*Q𝑧) ·Q 𝑤) ↔ ((*Q‘(𝑣 ·Q 𝑤)) ·Q 𝑤) <Q ((*Q𝑧) ·Q 𝑤)))
72 fveq2 5178 . . . . . . . . . . . . . . . . 17 (𝑦 = ((*Q‘(𝑣 ·Q 𝑤)) ·Q 𝑤) → (*Q𝑦) = (*Q‘((*Q‘(𝑣 ·Q 𝑤)) ·Q 𝑤)))
7372eleq1d 2106 . . . . . . . . . . . . . . . 16 (𝑦 = ((*Q‘(𝑣 ·Q 𝑤)) ·Q 𝑤) → ((*Q𝑦) ∈ (1st𝐴) ↔ (*Q‘((*Q‘(𝑣 ·Q 𝑤)) ·Q 𝑤)) ∈ (1st𝐴)))
7471, 73anbi12d 442 . . . . . . . . . . . . . . 15 (𝑦 = ((*Q‘(𝑣 ·Q 𝑤)) ·Q 𝑤) → ((𝑦 <Q ((*Q𝑧) ·Q 𝑤) ∧ (*Q𝑦) ∈ (1st𝐴)) ↔ (((*Q‘(𝑣 ·Q 𝑤)) ·Q 𝑤) <Q ((*Q𝑧) ·Q 𝑤) ∧ (*Q‘((*Q‘(𝑣 ·Q 𝑤)) ·Q 𝑤)) ∈ (1st𝐴))))
7574spcegv 2641 . . . . . . . . . . . . . 14 (((*Q‘(𝑣 ·Q 𝑤)) ·Q 𝑤) ∈ Q → ((((*Q‘(𝑣 ·Q 𝑤)) ·Q 𝑤) <Q ((*Q𝑧) ·Q 𝑤) ∧ (*Q‘((*Q‘(𝑣 ·Q 𝑤)) ·Q 𝑤)) ∈ (1st𝐴)) → ∃𝑦(𝑦 <Q ((*Q𝑧) ·Q 𝑤) ∧ (*Q𝑦) ∈ (1st𝐴))))
7664, 75syl 14 . . . . . . . . . . . . 13 (((𝐴P ∧ 1Q <Q 𝑤) ∧ (𝑣 ∈ (1st𝐴) ∧ (𝑣 ·Q 𝑤) ∈ (2nd𝐴)) ∧ 𝑧 <Q (𝑣 ·Q 𝑤)) → ((((*Q‘(𝑣 ·Q 𝑤)) ·Q 𝑤) <Q ((*Q𝑧) ·Q 𝑤) ∧ (*Q‘((*Q‘(𝑣 ·Q 𝑤)) ·Q 𝑤)) ∈ (1st𝐴)) → ∃𝑦(𝑦 <Q ((*Q𝑧) ·Q 𝑤) ∧ (*Q𝑦) ∈ (1st𝐴))))
77 recexpr.1 . . . . . . . . . . . . . 14 𝐵 = ⟨{𝑥 ∣ ∃𝑦(𝑥 <Q 𝑦 ∧ (*Q𝑦) ∈ (2nd𝐴))}, {𝑥 ∣ ∃𝑦(𝑦 <Q 𝑥 ∧ (*Q𝑦) ∈ (1st𝐴))}⟩
7877recexprlemelu 6721 . . . . . . . . . . . . 13 (((*Q𝑧) ·Q 𝑤) ∈ (2nd𝐵) ↔ ∃𝑦(𝑦 <Q ((*Q𝑧) ·Q 𝑤) ∧ (*Q𝑦) ∈ (1st𝐴)))
7976, 78syl6ibr 151 . . . . . . . . . . . 12 (((𝐴P ∧ 1Q <Q 𝑤) ∧ (𝑣 ∈ (1st𝐴) ∧ (𝑣 ·Q 𝑤) ∈ (2nd𝐴)) ∧ 𝑧 <Q (𝑣 ·Q 𝑤)) → ((((*Q‘(𝑣 ·Q 𝑤)) ·Q 𝑤) <Q ((*Q𝑧) ·Q 𝑤) ∧ (*Q‘((*Q‘(𝑣 ·Q 𝑤)) ·Q 𝑤)) ∈ (1st𝐴)) → ((*Q𝑧) ·Q 𝑤) ∈ (2nd𝐵)))
8047, 70, 79syl2and 279 . . . . . . . . . . 11 (((𝐴P ∧ 1Q <Q 𝑤) ∧ (𝑣 ∈ (1st𝐴) ∧ (𝑣 ·Q 𝑤) ∈ (2nd𝐴)) ∧ 𝑧 <Q (𝑣 ·Q 𝑤)) → ((𝑧 <Q (𝑣 ·Q 𝑤) ∧ ((𝑣 ·Q 𝑤) ·Q (*Q𝑤)) ∈ (1st𝐴)) → ((*Q𝑧) ·Q 𝑤) ∈ (2nd𝐵)))
819, 31, 80mp2and 409 . . . . . . . . . 10 (((𝐴P ∧ 1Q <Q 𝑤) ∧ (𝑣 ∈ (1st𝐴) ∧ (𝑣 ·Q 𝑤) ∈ (2nd𝐴)) ∧ 𝑧 <Q (𝑣 ·Q 𝑤)) → ((*Q𝑧) ·Q 𝑤) ∈ (2nd𝐵))
82 mulidnq 6487 . . . . . . . . . . . . . 14 (𝑤Q → (𝑤 ·Q 1Q) = 𝑤)
83 mulcomnqg 6481 . . . . . . . . . . . . . . 15 ((𝑤Q ∧ 1QQ) → (𝑤 ·Q 1Q) = (1Q ·Q 𝑤))
8448, 83mpan2 401 . . . . . . . . . . . . . 14 (𝑤Q → (𝑤 ·Q 1Q) = (1Q ·Q 𝑤))
8582, 84eqtr3d 2074 . . . . . . . . . . . . 13 (𝑤Q𝑤 = (1Q ·Q 𝑤))
8685adantl 262 . . . . . . . . . . . 12 ((𝑧Q𝑤Q) → 𝑤 = (1Q ·Q 𝑤))
87 recidnq 6491 . . . . . . . . . . . . . 14 (𝑧Q → (𝑧 ·Q (*Q𝑧)) = 1Q)
8887oveq1d 5527 . . . . . . . . . . . . 13 (𝑧Q → ((𝑧 ·Q (*Q𝑧)) ·Q 𝑤) = (1Q ·Q 𝑤))
8988adantr 261 . . . . . . . . . . . 12 ((𝑧Q𝑤Q) → ((𝑧 ·Q (*Q𝑧)) ·Q 𝑤) = (1Q ·Q 𝑤))
90 mulassnqg 6482 . . . . . . . . . . . . . 14 ((𝑧Q ∧ (*Q𝑧) ∈ Q𝑤Q) → ((𝑧 ·Q (*Q𝑧)) ·Q 𝑤) = (𝑧 ·Q ((*Q𝑧) ·Q 𝑤)))
9142, 90syl3an2 1169 . . . . . . . . . . . . 13 ((𝑧Q𝑧Q𝑤Q) → ((𝑧 ·Q (*Q𝑧)) ·Q 𝑤) = (𝑧 ·Q ((*Q𝑧) ·Q 𝑤)))
92913anidm12 1192 . . . . . . . . . . . 12 ((𝑧Q𝑤Q) → ((𝑧 ·Q (*Q𝑧)) ·Q 𝑤) = (𝑧 ·Q ((*Q𝑧) ·Q 𝑤)))
9386, 89, 923eqtr2d 2078 . . . . . . . . . . 11 ((𝑧Q𝑤Q) → 𝑤 = (𝑧 ·Q ((*Q𝑧) ·Q 𝑤)))
9441, 19, 93syl2anc 391 . . . . . . . . . 10 (((𝐴P ∧ 1Q <Q 𝑤) ∧ (𝑣 ∈ (1st𝐴) ∧ (𝑣 ·Q 𝑤) ∈ (2nd𝐴)) ∧ 𝑧 <Q (𝑣 ·Q 𝑤)) → 𝑤 = (𝑧 ·Q ((*Q𝑧) ·Q 𝑤)))
95 oveq2 5520 . . . . . . . . . . . 12 (𝑥 = ((*Q𝑧) ·Q 𝑤) → (𝑧 ·Q 𝑥) = (𝑧 ·Q ((*Q𝑧) ·Q 𝑤)))
9695eqeq2d 2051 . . . . . . . . . . 11 (𝑥 = ((*Q𝑧) ·Q 𝑤) → (𝑤 = (𝑧 ·Q 𝑥) ↔ 𝑤 = (𝑧 ·Q ((*Q𝑧) ·Q 𝑤))))
9796rspcev 2656 . . . . . . . . . 10 ((((*Q𝑧) ·Q 𝑤) ∈ (2nd𝐵) ∧ 𝑤 = (𝑧 ·Q ((*Q𝑧) ·Q 𝑤))) → ∃𝑥 ∈ (2nd𝐵)𝑤 = (𝑧 ·Q 𝑥))
9881, 94, 97syl2anc 391 . . . . . . . . 9 (((𝐴P ∧ 1Q <Q 𝑤) ∧ (𝑣 ∈ (1st𝐴) ∧ (𝑣 ·Q 𝑤) ∈ (2nd𝐴)) ∧ 𝑧 <Q (𝑣 ·Q 𝑤)) → ∃𝑥 ∈ (2nd𝐵)𝑤 = (𝑧 ·Q 𝑥))
99983expia 1106 . . . . . . . 8 (((𝐴P ∧ 1Q <Q 𝑤) ∧ (𝑣 ∈ (1st𝐴) ∧ (𝑣 ·Q 𝑤) ∈ (2nd𝐴))) → (𝑧 <Q (𝑣 ·Q 𝑤) → ∃𝑥 ∈ (2nd𝐵)𝑤 = (𝑧 ·Q 𝑥)))
10099reximdv 2420 . . . . . . 7 (((𝐴P ∧ 1Q <Q 𝑤) ∧ (𝑣 ∈ (1st𝐴) ∧ (𝑣 ·Q 𝑤) ∈ (2nd𝐴))) → (∃𝑧 ∈ (2nd𝐴)𝑧 <Q (𝑣 ·Q 𝑤) → ∃𝑧 ∈ (2nd𝐴)∃𝑥 ∈ (2nd𝐵)𝑤 = (𝑧 ·Q 𝑥)))
10177recexprlempr 6730 . . . . . . . . 9 (𝐴P𝐵P)
102 df-imp 6567 . . . . . . . . . 10 ·P = (𝑦P, 𝑤P ↦ ⟨{𝑢Q ∣ ∃𝑓Q𝑔Q (𝑓 ∈ (1st𝑦) ∧ 𝑔 ∈ (1st𝑤) ∧ 𝑢 = (𝑓 ·Q 𝑔))}, {𝑢Q ∣ ∃𝑓Q𝑔Q (𝑓 ∈ (2nd𝑦) ∧ 𝑔 ∈ (2nd𝑤) ∧ 𝑢 = (𝑓 ·Q 𝑔))}⟩)
103102, 59genpelvu 6611 . . . . . . . . 9 ((𝐴P𝐵P) → (𝑤 ∈ (2nd ‘(𝐴 ·P 𝐵)) ↔ ∃𝑧 ∈ (2nd𝐴)∃𝑥 ∈ (2nd𝐵)𝑤 = (𝑧 ·Q 𝑥)))
104101, 103mpdan 398 . . . . . . . 8 (𝐴P → (𝑤 ∈ (2nd ‘(𝐴 ·P 𝐵)) ↔ ∃𝑧 ∈ (2nd𝐴)∃𝑥 ∈ (2nd𝐵)𝑤 = (𝑧 ·Q 𝑥)))
105104ad2antrr 457 . . . . . . 7 (((𝐴P ∧ 1Q <Q 𝑤) ∧ (𝑣 ∈ (1st𝐴) ∧ (𝑣 ·Q 𝑤) ∈ (2nd𝐴))) → (𝑤 ∈ (2nd ‘(𝐴 ·P 𝐵)) ↔ ∃𝑧 ∈ (2nd𝐴)∃𝑥 ∈ (2nd𝐵)𝑤 = (𝑧 ·Q 𝑥)))
106100, 105sylibrd 158 . . . . . 6 (((𝐴P ∧ 1Q <Q 𝑤) ∧ (𝑣 ∈ (1st𝐴) ∧ (𝑣 ·Q 𝑤) ∈ (2nd𝐴))) → (∃𝑧 ∈ (2nd𝐴)𝑧 <Q (𝑣 ·Q 𝑤) → 𝑤 ∈ (2nd ‘(𝐴 ·P 𝐵))))
1078, 106mpd 13 . . . . 5 (((𝐴P ∧ 1Q <Q 𝑤) ∧ (𝑣 ∈ (1st𝐴) ∧ (𝑣 ·Q 𝑤) ∈ (2nd𝐴))) → 𝑤 ∈ (2nd ‘(𝐴 ·P 𝐵)))
1085, 107rexlimddv 2437 . . . 4 ((𝐴P ∧ 1Q <Q 𝑤) → 𝑤 ∈ (2nd ‘(𝐴 ·P 𝐵)))
109108ex 108 . . 3 (𝐴P → (1Q <Q 𝑤𝑤 ∈ (2nd ‘(𝐴 ·P 𝐵))))
1102, 109syl5bi 141 . 2 (𝐴P → (𝑤 ∈ (2nd ‘1P) → 𝑤 ∈ (2nd ‘(𝐴 ·P 𝐵))))
111110ssrdv 2951 1 (𝐴P → (2nd ‘1P) ⊆ (2nd ‘(𝐴 ·P 𝐵)))
 Colors of variables: wff set class Syntax hints:   → wi 4   ∧ wa 97   ↔ wb 98   ∧ w3a 885   = wceq 1243  ∃wex 1381   ∈ wcel 1393  {cab 2026  ∃wrex 2307   ⊆ wss 2917  ⟨cop 3378   class class class wbr 3764  ‘cfv 4902  (class class class)co 5512  1st c1st 5765  2nd c2nd 5766  Qcnq 6378  1Qc1q 6379   ·Q cmq 6381  *Qcrq 6382
 Copyright terms: Public domain W3C validator