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

Theorem recexprlem1ssu 7632
Description: The upper cut of one is a subset of the upper cut of 𝐴 ·P 𝐵. Lemma for recexpr 7636. (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 7554 . . . 4 (2nd ‘1P) = {𝑤 ∣ 1Q <Q 𝑤}
21abeq2i 2288 . . 3 (𝑤 ∈ (2nd ‘1P) ↔ 1Q <Q 𝑤)
3 prop 7473 . . . . . 6 (𝐴P → ⟨(1st𝐴), (2nd𝐴)⟩ ∈ P)
4 prmuloc2 7565 . . . . . 6 ((⟨(1st𝐴), (2nd𝐴)⟩ ∈ P ∧ 1Q <Q 𝑤) → ∃𝑣 ∈ (1st𝐴)(𝑣 ·Q 𝑤) ∈ (2nd𝐴))
53, 4sylan 283 . . . . 5 ((𝐴P ∧ 1Q <Q 𝑤) → ∃𝑣 ∈ (1st𝐴)(𝑣 ·Q 𝑤) ∈ (2nd𝐴))
6 prnminu 7487 . . . . . . . 8 ((⟨(1st𝐴), (2nd𝐴)⟩ ∈ P ∧ (𝑣 ·Q 𝑤) ∈ (2nd𝐴)) → ∃𝑧 ∈ (2nd𝐴)𝑧 <Q (𝑣 ·Q 𝑤))
73, 6sylan 283 . . . . . . 7 ((𝐴P ∧ (𝑣 ·Q 𝑤) ∈ (2nd𝐴)) → ∃𝑧 ∈ (2nd𝐴)𝑧 <Q (𝑣 ·Q 𝑤))
87ad2ant2rl 511 . . . . . 6 (((𝐴P ∧ 1Q <Q 𝑤) ∧ (𝑣 ∈ (1st𝐴) ∧ (𝑣 ·Q 𝑤) ∈ (2nd𝐴))) → ∃𝑧 ∈ (2nd𝐴)𝑧 <Q (𝑣 ·Q 𝑤))
9 simp3 999 . . . . . . . . . . 11 (((𝐴P ∧ 1Q <Q 𝑤) ∧ (𝑣 ∈ (1st𝐴) ∧ (𝑣 ·Q 𝑤) ∈ (2nd𝐴)) ∧ 𝑧 <Q (𝑣 ·Q 𝑤)) → 𝑧 <Q (𝑣 ·Q 𝑤))
10 simp2l 1023 . . . . . . . . . . . 12 (((𝐴P ∧ 1Q <Q 𝑤) ∧ (𝑣 ∈ (1st𝐴) ∧ (𝑣 ·Q 𝑤) ∈ (2nd𝐴)) ∧ 𝑧 <Q (𝑣 ·Q 𝑤)) → 𝑣 ∈ (1st𝐴))
11 elprnql 7479 . . . . . . . . . . . . . . . . . 18 ((⟨(1st𝐴), (2nd𝐴)⟩ ∈ P𝑣 ∈ (1st𝐴)) → 𝑣Q)
123, 11sylan 283 . . . . . . . . . . . . . . . . 17 ((𝐴P𝑣 ∈ (1st𝐴)) → 𝑣Q)
1312ad2ant2r 509 . . . . . . . . . . . . . . . 16 (((𝐴P ∧ 1Q <Q 𝑤) ∧ (𝑣 ∈ (1st𝐴) ∧ (𝑣 ·Q 𝑤) ∈ (2nd𝐴))) → 𝑣Q)
14133adant3 1017 . . . . . . . . . . . . . . 15 (((𝐴P ∧ 1Q <Q 𝑤) ∧ (𝑣 ∈ (1st𝐴) ∧ (𝑣 ·Q 𝑤) ∈ (2nd𝐴)) ∧ 𝑧 <Q (𝑣 ·Q 𝑤)) → 𝑣Q)
15 simp1r 1022 . . . . . . . . . . . . . . . 16 (((𝐴P ∧ 1Q <Q 𝑤) ∧ (𝑣 ∈ (1st𝐴) ∧ (𝑣 ·Q 𝑤) ∈ (2nd𝐴)) ∧ 𝑧 <Q (𝑣 ·Q 𝑤)) → 1Q <Q 𝑤)
16 ltrelnq 7363 . . . . . . . . . . . . . . . . . 18 <Q ⊆ (Q × Q)
1716brel 4678 . . . . . . . . . . . . . . . . 17 (1Q <Q 𝑤 → (1QQ𝑤Q))
1817simprd 114 . . . . . . . . . . . . . . . 16 (1Q <Q 𝑤𝑤Q)
1915, 18syl 14 . . . . . . . . . . . . . . 15 (((𝐴P ∧ 1Q <Q 𝑤) ∧ (𝑣 ∈ (1st𝐴) ∧ (𝑣 ·Q 𝑤) ∈ (2nd𝐴)) ∧ 𝑧 <Q (𝑣 ·Q 𝑤)) → 𝑤Q)
20 recclnq 7390 . . . . . . . . . . . . . . . 16 (𝑤Q → (*Q𝑤) ∈ Q)
2119, 20syl 14 . . . . . . . . . . . . . . 15 (((𝐴P ∧ 1Q <Q 𝑤) ∧ (𝑣 ∈ (1st𝐴) ∧ (𝑣 ·Q 𝑤) ∈ (2nd𝐴)) ∧ 𝑧 <Q (𝑣 ·Q 𝑤)) → (*Q𝑤) ∈ Q)
22 mulassnqg 7382 . . . . . . . . . . . . . . 15 ((𝑣Q𝑤Q ∧ (*Q𝑤) ∈ Q) → ((𝑣 ·Q 𝑤) ·Q (*Q𝑤)) = (𝑣 ·Q (𝑤 ·Q (*Q𝑤))))
2314, 19, 21, 22syl3anc 1238 . . . . . . . . . . . . . 14 (((𝐴P ∧ 1Q <Q 𝑤) ∧ (𝑣 ∈ (1st𝐴) ∧ (𝑣 ·Q 𝑤) ∈ (2nd𝐴)) ∧ 𝑧 <Q (𝑣 ·Q 𝑤)) → ((𝑣 ·Q 𝑤) ·Q (*Q𝑤)) = (𝑣 ·Q (𝑤 ·Q (*Q𝑤))))
24 recidnq 7391 . . . . . . . . . . . . . . . 16 (𝑤Q → (𝑤 ·Q (*Q𝑤)) = 1Q)
2519, 24syl 14 . . . . . . . . . . . . . . 15 (((𝐴P ∧ 1Q <Q 𝑤) ∧ (𝑣 ∈ (1st𝐴) ∧ (𝑣 ·Q 𝑤) ∈ (2nd𝐴)) ∧ 𝑧 <Q (𝑣 ·Q 𝑤)) → (𝑤 ·Q (*Q𝑤)) = 1Q)
2625oveq2d 5890 . . . . . . . . . . . . . 14 (((𝐴P ∧ 1Q <Q 𝑤) ∧ (𝑣 ∈ (1st𝐴) ∧ (𝑣 ·Q 𝑤) ∈ (2nd𝐴)) ∧ 𝑧 <Q (𝑣 ·Q 𝑤)) → (𝑣 ·Q (𝑤 ·Q (*Q𝑤))) = (𝑣 ·Q 1Q))
27 mulidnq 7387 . . . . . . . . . . . . . . 15 (𝑣Q → (𝑣 ·Q 1Q) = 𝑣)
2814, 27syl 14 . . . . . . . . . . . . . 14 (((𝐴P ∧ 1Q <Q 𝑤) ∧ (𝑣 ∈ (1st𝐴) ∧ (𝑣 ·Q 𝑤) ∈ (2nd𝐴)) ∧ 𝑧 <Q (𝑣 ·Q 𝑤)) → (𝑣 ·Q 1Q) = 𝑣)
2923, 26, 283eqtrd 2214 . . . . . . . . . . . . 13 (((𝐴P ∧ 1Q <Q 𝑤) ∧ (𝑣 ∈ (1st𝐴) ∧ (𝑣 ·Q 𝑤) ∈ (2nd𝐴)) ∧ 𝑧 <Q (𝑣 ·Q 𝑤)) → ((𝑣 ·Q 𝑤) ·Q (*Q𝑤)) = 𝑣)
3029eleq1d 2246 . . . . . . . . . . . 12 (((𝐴P ∧ 1Q <Q 𝑤) ∧ (𝑣 ∈ (1st𝐴) ∧ (𝑣 ·Q 𝑤) ∈ (2nd𝐴)) ∧ 𝑧 <Q (𝑣 ·Q 𝑤)) → (((𝑣 ·Q 𝑤) ·Q (*Q𝑤)) ∈ (1st𝐴) ↔ 𝑣 ∈ (1st𝐴)))
3110, 30mpbird 167 . . . . . . . . . . 11 (((𝐴P ∧ 1Q <Q 𝑤) ∧ (𝑣 ∈ (1st𝐴) ∧ (𝑣 ·Q 𝑤) ∈ (2nd𝐴)) ∧ 𝑧 <Q (𝑣 ·Q 𝑤)) → ((𝑣 ·Q 𝑤) ·Q (*Q𝑤)) ∈ (1st𝐴))
32 ltrnqi 7419 . . . . . . . . . . . . 13 (𝑧 <Q (𝑣 ·Q 𝑤) → (*Q‘(𝑣 ·Q 𝑤)) <Q (*Q𝑧))
33 ltmnqg 7399 . . . . . . . . . . . . . . 15 ((𝑓Q𝑔QQ) → (𝑓 <Q 𝑔 ↔ ( ·Q 𝑓) <Q ( ·Q 𝑔)))
3433adantl 277 . . . . . . . . . . . . . 14 ((((𝐴P ∧ 1Q <Q 𝑤) ∧ (𝑣 ∈ (1st𝐴) ∧ (𝑣 ·Q 𝑤) ∈ (2nd𝐴)) ∧ 𝑧 <Q (𝑣 ·Q 𝑤)) ∧ (𝑓Q𝑔QQ)) → (𝑓 <Q 𝑔 ↔ ( ·Q 𝑓) <Q ( ·Q 𝑔)))
35 mulclnq 7374 . . . . . . . . . . . . . . . 16 ((𝑣Q𝑤Q) → (𝑣 ·Q 𝑤) ∈ Q)
3614, 19, 35syl2anc 411 . . . . . . . . . . . . . . 15 (((𝐴P ∧ 1Q <Q 𝑤) ∧ (𝑣 ∈ (1st𝐴) ∧ (𝑣 ·Q 𝑤) ∈ (2nd𝐴)) ∧ 𝑧 <Q (𝑣 ·Q 𝑤)) → (𝑣 ·Q 𝑤) ∈ Q)
37 recclnq 7390 . . . . . . . . . . . . . . 15 ((𝑣 ·Q 𝑤) ∈ Q → (*Q‘(𝑣 ·Q 𝑤)) ∈ Q)
3836, 37syl 14 . . . . . . . . . . . . . 14 (((𝐴P ∧ 1Q <Q 𝑤) ∧ (𝑣 ∈ (1st𝐴) ∧ (𝑣 ·Q 𝑤) ∈ (2nd𝐴)) ∧ 𝑧 <Q (𝑣 ·Q 𝑤)) → (*Q‘(𝑣 ·Q 𝑤)) ∈ Q)
3916brel 4678 . . . . . . . . . . . . . . . . 17 (𝑧 <Q (𝑣 ·Q 𝑤) → (𝑧Q ∧ (𝑣 ·Q 𝑤) ∈ Q))
4039simpld 112 . . . . . . . . . . . . . . . 16 (𝑧 <Q (𝑣 ·Q 𝑤) → 𝑧Q)
419, 40syl 14 . . . . . . . . . . . . . . 15 (((𝐴P ∧ 1Q <Q 𝑤) ∧ (𝑣 ∈ (1st𝐴) ∧ (𝑣 ·Q 𝑤) ∈ (2nd𝐴)) ∧ 𝑧 <Q (𝑣 ·Q 𝑤)) → 𝑧Q)
42 recclnq 7390 . . . . . . . . . . . . . . 15 (𝑧Q → (*Q𝑧) ∈ Q)
4341, 42syl 14 . . . . . . . . . . . . . 14 (((𝐴P ∧ 1Q <Q 𝑤) ∧ (𝑣 ∈ (1st𝐴) ∧ (𝑣 ·Q 𝑤) ∈ (2nd𝐴)) ∧ 𝑧 <Q (𝑣 ·Q 𝑤)) → (*Q𝑧) ∈ Q)
44 mulcomnqg 7381 . . . . . . . . . . . . . . 15 ((𝑓Q𝑔Q) → (𝑓 ·Q 𝑔) = (𝑔 ·Q 𝑓))
4544adantl 277 . . . . . . . . . . . . . 14 ((((𝐴P ∧ 1Q <Q 𝑤) ∧ (𝑣 ∈ (1st𝐴) ∧ (𝑣 ·Q 𝑤) ∈ (2nd𝐴)) ∧ 𝑧 <Q (𝑣 ·Q 𝑤)) ∧ (𝑓Q𝑔Q)) → (𝑓 ·Q 𝑔) = (𝑔 ·Q 𝑓))
4634, 38, 43, 19, 45caovord2d 6043 . . . . . . . . . . . . 13 (((𝐴P ∧ 1Q <Q 𝑤) ∧ (𝑣 ∈ (1st𝐴) ∧ (𝑣 ·Q 𝑤) ∈ (2nd𝐴)) ∧ 𝑧 <Q (𝑣 ·Q 𝑤)) → ((*Q‘(𝑣 ·Q 𝑤)) <Q (*Q𝑧) ↔ ((*Q‘(𝑣 ·Q 𝑤)) ·Q 𝑤) <Q ((*Q𝑧) ·Q 𝑤)))
4732, 46imbitrid 154 . . . . . . . . . . . 12 (((𝐴P ∧ 1Q <Q 𝑤) ∧ (𝑣 ∈ (1st𝐴) ∧ (𝑣 ·Q 𝑤) ∈ (2nd𝐴)) ∧ 𝑧 <Q (𝑣 ·Q 𝑤)) → (𝑧 <Q (𝑣 ·Q 𝑤) → ((*Q‘(𝑣 ·Q 𝑤)) ·Q 𝑤) <Q ((*Q𝑧) ·Q 𝑤)))
48 mulcomnqg 7381 . . . . . . . . . . . . . . . . . . . . 21 (((𝑣 ·Q 𝑤) ∈ Q ∧ (*Q‘(𝑣 ·Q 𝑤)) ∈ Q) → ((𝑣 ·Q 𝑤) ·Q (*Q‘(𝑣 ·Q 𝑤))) = ((*Q‘(𝑣 ·Q 𝑤)) ·Q (𝑣 ·Q 𝑤)))
4937, 48mpdan 421 . . . . . . . . . . . . . . . . . . . 20 ((𝑣 ·Q 𝑤) ∈ Q → ((𝑣 ·Q 𝑤) ·Q (*Q‘(𝑣 ·Q 𝑤))) = ((*Q‘(𝑣 ·Q 𝑤)) ·Q (𝑣 ·Q 𝑤)))
50 recidnq 7391 . . . . . . . . . . . . . . . . . . . 20 ((𝑣 ·Q 𝑤) ∈ Q → ((𝑣 ·Q 𝑤) ·Q (*Q‘(𝑣 ·Q 𝑤))) = 1Q)
5149, 50eqtr3d 2212 . . . . . . . . . . . . . . . . . . 19 ((𝑣 ·Q 𝑤) ∈ Q → ((*Q‘(𝑣 ·Q 𝑤)) ·Q (𝑣 ·Q 𝑤)) = 1Q)
5251, 24oveqan12d 5893 . . . . . . . . . . . . . . . . . 18 (((𝑣 ·Q 𝑤) ∈ Q𝑤Q) → (((*Q‘(𝑣 ·Q 𝑤)) ·Q (𝑣 ·Q 𝑤)) ·Q (𝑤 ·Q (*Q𝑤))) = (1Q ·Q 1Q))
5336, 19, 52syl2anc 411 . . . . . . . . . . . . . . . . 17 (((𝐴P ∧ 1Q <Q 𝑤) ∧ (𝑣 ∈ (1st𝐴) ∧ (𝑣 ·Q 𝑤) ∈ (2nd𝐴)) ∧ 𝑧 <Q (𝑣 ·Q 𝑤)) → (((*Q‘(𝑣 ·Q 𝑤)) ·Q (𝑣 ·Q 𝑤)) ·Q (𝑤 ·Q (*Q𝑤))) = (1Q ·Q 1Q))
54 mulassnqg 7382 . . . . . . . . . . . . . . . . . . 19 ((𝑓Q𝑔QQ) → ((𝑓 ·Q 𝑔) ·Q ) = (𝑓 ·Q (𝑔 ·Q )))
5554adantl 277 . . . . . . . . . . . . . . . . . 18 ((((𝐴P ∧ 1Q <Q 𝑤) ∧ (𝑣 ∈ (1st𝐴) ∧ (𝑣 ·Q 𝑤) ∈ (2nd𝐴)) ∧ 𝑧 <Q (𝑣 ·Q 𝑤)) ∧ (𝑓Q𝑔QQ)) → ((𝑓 ·Q 𝑔) ·Q ) = (𝑓 ·Q (𝑔 ·Q )))
56 mulclnq 7374 . . . . . . . . . . . . . . . . . . 19 ((𝑓Q𝑔Q) → (𝑓 ·Q 𝑔) ∈ Q)
5756adantl 277 . . . . . . . . . . . . . . . . . 18 ((((𝐴P ∧ 1Q <Q 𝑤) ∧ (𝑣 ∈ (1st𝐴) ∧ (𝑣 ·Q 𝑤) ∈ (2nd𝐴)) ∧ 𝑧 <Q (𝑣 ·Q 𝑤)) ∧ (𝑓Q𝑔Q)) → (𝑓 ·Q 𝑔) ∈ Q)
5838, 36, 19, 45, 55, 21, 57caov4d 6058 . . . . . . . . . . . . . . . . 17 (((𝐴P ∧ 1Q <Q 𝑤) ∧ (𝑣 ∈ (1st𝐴) ∧ (𝑣 ·Q 𝑤) ∈ (2nd𝐴)) ∧ 𝑧 <Q (𝑣 ·Q 𝑤)) → (((*Q‘(𝑣 ·Q 𝑤)) ·Q (𝑣 ·Q 𝑤)) ·Q (𝑤 ·Q (*Q𝑤))) = (((*Q‘(𝑣 ·Q 𝑤)) ·Q 𝑤) ·Q ((𝑣 ·Q 𝑤) ·Q (*Q𝑤))))
5953, 58eqtr3d 2212 . . . . . . . . . . . . . . . 16 (((𝐴P ∧ 1Q <Q 𝑤) ∧ (𝑣 ∈ (1st𝐴) ∧ (𝑣 ·Q 𝑤) ∈ (2nd𝐴)) ∧ 𝑧 <Q (𝑣 ·Q 𝑤)) → (1Q ·Q 1Q) = (((*Q‘(𝑣 ·Q 𝑤)) ·Q 𝑤) ·Q ((𝑣 ·Q 𝑤) ·Q (*Q𝑤))))
60 1nq 7364 . . . . . . . . . . . . . . . . 17 1QQ
61 mulidnq 7387 . . . . . . . . . . . . . . . . 17 (1QQ → (1Q ·Q 1Q) = 1Q)
6260, 61ax-mp 5 . . . . . . . . . . . . . . . 16 (1Q ·Q 1Q) = 1Q
6359, 62eqtr3di 2225 . . . . . . . . . . . . . . 15 (((𝐴P ∧ 1Q <Q 𝑤) ∧ (𝑣 ∈ (1st𝐴) ∧ (𝑣 ·Q 𝑤) ∈ (2nd𝐴)) ∧ 𝑧 <Q (𝑣 ·Q 𝑤)) → (((*Q‘(𝑣 ·Q 𝑤)) ·Q 𝑤) ·Q ((𝑣 ·Q 𝑤) ·Q (*Q𝑤))) = 1Q)
6457, 38, 19caovcld 6027 . . . . . . . . . . . . . . . 16 (((𝐴P ∧ 1Q <Q 𝑤) ∧ (𝑣 ∈ (1st𝐴) ∧ (𝑣 ·Q 𝑤) ∈ (2nd𝐴)) ∧ 𝑧 <Q (𝑣 ·Q 𝑤)) → ((*Q‘(𝑣 ·Q 𝑤)) ·Q 𝑤) ∈ Q)
6557, 36, 21caovcld 6027 . . . . . . . . . . . . . . . 16 (((𝐴P ∧ 1Q <Q 𝑤) ∧ (𝑣 ∈ (1st𝐴) ∧ (𝑣 ·Q 𝑤) ∈ (2nd𝐴)) ∧ 𝑧 <Q (𝑣 ·Q 𝑤)) → ((𝑣 ·Q 𝑤) ·Q (*Q𝑤)) ∈ Q)
66 recmulnqg 7389 . . . . . . . . . . . . . . . 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 411 . . . . . . . . . . . . . . 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 167 . . . . . . . . . . . . . 14 (((𝐴P ∧ 1Q <Q 𝑤) ∧ (𝑣 ∈ (1st𝐴) ∧ (𝑣 ·Q 𝑤) ∈ (2nd𝐴)) ∧ 𝑧 <Q (𝑣 ·Q 𝑤)) → (*Q‘((*Q‘(𝑣 ·Q 𝑤)) ·Q 𝑤)) = ((𝑣 ·Q 𝑤) ·Q (*Q𝑤)))
6968eleq1d 2246 . . . . . . . . . . . . 13 (((𝐴P ∧ 1Q <Q 𝑤) ∧ (𝑣 ∈ (1st𝐴) ∧ (𝑣 ·Q 𝑤) ∈ (2nd𝐴)) ∧ 𝑧 <Q (𝑣 ·Q 𝑤)) → ((*Q‘((*Q‘(𝑣 ·Q 𝑤)) ·Q 𝑤)) ∈ (1st𝐴) ↔ ((𝑣 ·Q 𝑤) ·Q (*Q𝑤)) ∈ (1st𝐴)))
7069biimprd 158 . . . . . . . . . . . 12 (((𝐴P ∧ 1Q <Q 𝑤) ∧ (𝑣 ∈ (1st𝐴) ∧ (𝑣 ·Q 𝑤) ∈ (2nd𝐴)) ∧ 𝑧 <Q (𝑣 ·Q 𝑤)) → (((𝑣 ·Q 𝑤) ·Q (*Q𝑤)) ∈ (1st𝐴) → (*Q‘((*Q‘(𝑣 ·Q 𝑤)) ·Q 𝑤)) ∈ (1st𝐴)))
71 breq1 4006 . . . . . . . . . . . . . . . 16 (𝑦 = ((*Q‘(𝑣 ·Q 𝑤)) ·Q 𝑤) → (𝑦 <Q ((*Q𝑧) ·Q 𝑤) ↔ ((*Q‘(𝑣 ·Q 𝑤)) ·Q 𝑤) <Q ((*Q𝑧) ·Q 𝑤)))
72 fveq2 5515 . . . . . . . . . . . . . . . . 17 (𝑦 = ((*Q‘(𝑣 ·Q 𝑤)) ·Q 𝑤) → (*Q𝑦) = (*Q‘((*Q‘(𝑣 ·Q 𝑤)) ·Q 𝑤)))
7372eleq1d 2246 . . . . . . . . . . . . . . . 16 (𝑦 = ((*Q‘(𝑣 ·Q 𝑤)) ·Q 𝑤) → ((*Q𝑦) ∈ (1st𝐴) ↔ (*Q‘((*Q‘(𝑣 ·Q 𝑤)) ·Q 𝑤)) ∈ (1st𝐴)))
7471, 73anbi12d 473 . . . . . . . . . . . . . . 15 (𝑦 = ((*Q‘(𝑣 ·Q 𝑤)) ·Q 𝑤) → ((𝑦 <Q ((*Q𝑧) ·Q 𝑤) ∧ (*Q𝑦) ∈ (1st𝐴)) ↔ (((*Q‘(𝑣 ·Q 𝑤)) ·Q 𝑤) <Q ((*Q𝑧) ·Q 𝑤) ∧ (*Q‘((*Q‘(𝑣 ·Q 𝑤)) ·Q 𝑤)) ∈ (1st𝐴))))
7574spcegv 2825 . . . . . . . . . . . . . 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 7621 . . . . . . . . . . . . 13 (((*Q𝑧) ·Q 𝑤) ∈ (2nd𝐵) ↔ ∃𝑦(𝑦 <Q ((*Q𝑧) ·Q 𝑤) ∧ (*Q𝑦) ∈ (1st𝐴)))
7976, 78syl6ibr 162 . . . . . . . . . . . 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 295 . . . . . . . . . . 11 (((𝐴P ∧ 1Q <Q 𝑤) ∧ (𝑣 ∈ (1st𝐴) ∧ (𝑣 ·Q 𝑤) ∈ (2nd𝐴)) ∧ 𝑧 <Q (𝑣 ·Q 𝑤)) → ((𝑧 <Q (𝑣 ·Q 𝑤) ∧ ((𝑣 ·Q 𝑤) ·Q (*Q𝑤)) ∈ (1st𝐴)) → ((*Q𝑧) ·Q 𝑤) ∈ (2nd𝐵)))
819, 31, 80mp2and 433 . . . . . . . . . 10 (((𝐴P ∧ 1Q <Q 𝑤) ∧ (𝑣 ∈ (1st𝐴) ∧ (𝑣 ·Q 𝑤) ∈ (2nd𝐴)) ∧ 𝑧 <Q (𝑣 ·Q 𝑤)) → ((*Q𝑧) ·Q 𝑤) ∈ (2nd𝐵))
82 mulidnq 7387 . . . . . . . . . . . . . 14 (𝑤Q → (𝑤 ·Q 1Q) = 𝑤)
83 mulcomnqg 7381 . . . . . . . . . . . . . . 15 ((𝑤Q ∧ 1QQ) → (𝑤 ·Q 1Q) = (1Q ·Q 𝑤))
8460, 83mpan2 425 . . . . . . . . . . . . . 14 (𝑤Q → (𝑤 ·Q 1Q) = (1Q ·Q 𝑤))
8582, 84eqtr3d 2212 . . . . . . . . . . . . 13 (𝑤Q𝑤 = (1Q ·Q 𝑤))
8685adantl 277 . . . . . . . . . . . 12 ((𝑧Q𝑤Q) → 𝑤 = (1Q ·Q 𝑤))
87 recidnq 7391 . . . . . . . . . . . . . 14 (𝑧Q → (𝑧 ·Q (*Q𝑧)) = 1Q)
8887oveq1d 5889 . . . . . . . . . . . . 13 (𝑧Q → ((𝑧 ·Q (*Q𝑧)) ·Q 𝑤) = (1Q ·Q 𝑤))
8988adantr 276 . . . . . . . . . . . 12 ((𝑧Q𝑤Q) → ((𝑧 ·Q (*Q𝑧)) ·Q 𝑤) = (1Q ·Q 𝑤))
90 mulassnqg 7382 . . . . . . . . . . . . . 14 ((𝑧Q ∧ (*Q𝑧) ∈ Q𝑤Q) → ((𝑧 ·Q (*Q𝑧)) ·Q 𝑤) = (𝑧 ·Q ((*Q𝑧) ·Q 𝑤)))
9142, 90syl3an2 1272 . . . . . . . . . . . . 13 ((𝑧Q𝑧Q𝑤Q) → ((𝑧 ·Q (*Q𝑧)) ·Q 𝑤) = (𝑧 ·Q ((*Q𝑧) ·Q 𝑤)))
92913anidm12 1295 . . . . . . . . . . . 12 ((𝑧Q𝑤Q) → ((𝑧 ·Q (*Q𝑧)) ·Q 𝑤) = (𝑧 ·Q ((*Q𝑧) ·Q 𝑤)))
9386, 89, 923eqtr2d 2216 . . . . . . . . . . 11 ((𝑧Q𝑤Q) → 𝑤 = (𝑧 ·Q ((*Q𝑧) ·Q 𝑤)))
9441, 19, 93syl2anc 411 . . . . . . . . . 10 (((𝐴P ∧ 1Q <Q 𝑤) ∧ (𝑣 ∈ (1st𝐴) ∧ (𝑣 ·Q 𝑤) ∈ (2nd𝐴)) ∧ 𝑧 <Q (𝑣 ·Q 𝑤)) → 𝑤 = (𝑧 ·Q ((*Q𝑧) ·Q 𝑤)))
95 oveq2 5882 . . . . . . . . . . . 12 (𝑥 = ((*Q𝑧) ·Q 𝑤) → (𝑧 ·Q 𝑥) = (𝑧 ·Q ((*Q𝑧) ·Q 𝑤)))
9695eqeq2d 2189 . . . . . . . . . . 11 (𝑥 = ((*Q𝑧) ·Q 𝑤) → (𝑤 = (𝑧 ·Q 𝑥) ↔ 𝑤 = (𝑧 ·Q ((*Q𝑧) ·Q 𝑤))))
9796rspcev 2841 . . . . . . . . . 10 ((((*Q𝑧) ·Q 𝑤) ∈ (2nd𝐵) ∧ 𝑤 = (𝑧 ·Q ((*Q𝑧) ·Q 𝑤))) → ∃𝑥 ∈ (2nd𝐵)𝑤 = (𝑧 ·Q 𝑥))
9881, 94, 97syl2anc 411 . . . . . . . . 9 (((𝐴P ∧ 1Q <Q 𝑤) ∧ (𝑣 ∈ (1st𝐴) ∧ (𝑣 ·Q 𝑤) ∈ (2nd𝐴)) ∧ 𝑧 <Q (𝑣 ·Q 𝑤)) → ∃𝑥 ∈ (2nd𝐵)𝑤 = (𝑧 ·Q 𝑥))
99983expia 1205 . . . . . . . 8 (((𝐴P ∧ 1Q <Q 𝑤) ∧ (𝑣 ∈ (1st𝐴) ∧ (𝑣 ·Q 𝑤) ∈ (2nd𝐴))) → (𝑧 <Q (𝑣 ·Q 𝑤) → ∃𝑥 ∈ (2nd𝐵)𝑤 = (𝑧 ·Q 𝑥)))
10099reximdv 2578 . . . . . . 7 (((𝐴P ∧ 1Q <Q 𝑤) ∧ (𝑣 ∈ (1st𝐴) ∧ (𝑣 ·Q 𝑤) ∈ (2nd𝐴))) → (∃𝑧 ∈ (2nd𝐴)𝑧 <Q (𝑣 ·Q 𝑤) → ∃𝑧 ∈ (2nd𝐴)∃𝑥 ∈ (2nd𝐵)𝑤 = (𝑧 ·Q 𝑥)))
10177recexprlempr 7630 . . . . . . . . 9 (𝐴P𝐵P)
102 df-imp 7467 . . . . . . . . . 10 ·P = (𝑦P, 𝑤P ↦ ⟨{𝑢Q ∣ ∃𝑓Q𝑔Q (𝑓 ∈ (1st𝑦) ∧ 𝑔 ∈ (1st𝑤) ∧ 𝑢 = (𝑓 ·Q 𝑔))}, {𝑢Q ∣ ∃𝑓Q𝑔Q (𝑓 ∈ (2nd𝑦) ∧ 𝑔 ∈ (2nd𝑤) ∧ 𝑢 = (𝑓 ·Q 𝑔))}⟩)
103102, 56genpelvu 7511 . . . . . . . . 9 ((𝐴P𝐵P) → (𝑤 ∈ (2nd ‘(𝐴 ·P 𝐵)) ↔ ∃𝑧 ∈ (2nd𝐴)∃𝑥 ∈ (2nd𝐵)𝑤 = (𝑧 ·Q 𝑥)))
104101, 103mpdan 421 . . . . . . . 8 (𝐴P → (𝑤 ∈ (2nd ‘(𝐴 ·P 𝐵)) ↔ ∃𝑧 ∈ (2nd𝐴)∃𝑥 ∈ (2nd𝐵)𝑤 = (𝑧 ·Q 𝑥)))
105104ad2antrr 488 . . . . . . 7 (((𝐴P ∧ 1Q <Q 𝑤) ∧ (𝑣 ∈ (1st𝐴) ∧ (𝑣 ·Q 𝑤) ∈ (2nd𝐴))) → (𝑤 ∈ (2nd ‘(𝐴 ·P 𝐵)) ↔ ∃𝑧 ∈ (2nd𝐴)∃𝑥 ∈ (2nd𝐵)𝑤 = (𝑧 ·Q 𝑥)))
106100, 105sylibrd 169 . . . . . 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 2599 . . . 4 ((𝐴P ∧ 1Q <Q 𝑤) → 𝑤 ∈ (2nd ‘(𝐴 ·P 𝐵)))
109108ex 115 . . 3 (𝐴P → (1Q <Q 𝑤𝑤 ∈ (2nd ‘(𝐴 ·P 𝐵))))
1102, 109biimtrid 152 . 2 (𝐴P → (𝑤 ∈ (2nd ‘1P) → 𝑤 ∈ (2nd ‘(𝐴 ·P 𝐵))))
111110ssrdv 3161 1 (𝐴P → (2nd ‘1P) ⊆ (2nd ‘(𝐴 ·P 𝐵)))
Colors of variables: wff set class
Syntax hints:  wi 4  wa 104  wb 105  w3a 978   = wceq 1353  wex 1492  wcel 2148  {cab 2163  wrex 2456  wss 3129  cop 3595   class class class wbr 4003  cfv 5216  (class class class)co 5874  1st c1st 6138  2nd c2nd 6139  Qcnq 7278  1Qc1q 7279   ·Q cmq 7281  *Qcrq 7282   <Q cltq 7283  Pcnp 7289  1Pc1p 7290   ·P cmp 7292
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-in1 614  ax-in2 615  ax-io 709  ax-5 1447  ax-7 1448  ax-gen 1449  ax-ie1 1493  ax-ie2 1494  ax-8 1504  ax-10 1505  ax-11 1506  ax-i12 1507  ax-bndl 1509  ax-4 1510  ax-17 1526  ax-i9 1530  ax-ial 1534  ax-i5r 1535  ax-13 2150  ax-14 2151  ax-ext 2159  ax-coll 4118  ax-sep 4121  ax-nul 4129  ax-pow 4174  ax-pr 4209  ax-un 4433  ax-setind 4536  ax-iinf 4587
This theorem depends on definitions:  df-bi 117  df-dc 835  df-3or 979  df-3an 980  df-tru 1356  df-fal 1359  df-nf 1461  df-sb 1763  df-eu 2029  df-mo 2030  df-clab 2164  df-cleq 2170  df-clel 2173  df-nfc 2308  df-ne 2348  df-ral 2460  df-rex 2461  df-reu 2462  df-rab 2464  df-v 2739  df-sbc 2963  df-csb 3058  df-dif 3131  df-un 3133  df-in 3135  df-ss 3142  df-nul 3423  df-pw 3577  df-sn 3598  df-pr 3599  df-op 3601  df-uni 3810  df-int 3845  df-iun 3888  df-br 4004  df-opab 4065  df-mpt 4066  df-tr 4102  df-eprel 4289  df-id 4293  df-po 4296  df-iso 4297  df-iord 4366  df-on 4368  df-suc 4371  df-iom 4590  df-xp 4632  df-rel 4633  df-cnv 4634  df-co 4635  df-dm 4636  df-rn 4637  df-res 4638  df-ima 4639  df-iota 5178  df-fun 5218  df-fn 5219  df-f 5220  df-f1 5221  df-fo 5222  df-f1o 5223  df-fv 5224  df-ov 5877  df-oprab 5878  df-mpo 5879  df-1st 6140  df-2nd 6141  df-recs 6305  df-irdg 6370  df-1o 6416  df-2o 6417  df-oadd 6420  df-omul 6421  df-er 6534  df-ec 6536  df-qs 6540  df-ni 7302  df-pli 7303  df-mi 7304  df-lti 7305  df-plpq 7342  df-mpq 7343  df-enq 7345  df-nqqs 7346  df-plqqs 7347  df-mqqs 7348  df-1nqqs 7349  df-rq 7350  df-ltnqqs 7351  df-enq0 7422  df-nq0 7423  df-0nq0 7424  df-plq0 7425  df-mq0 7426  df-inp 7464  df-i1p 7465  df-imp 7467
This theorem is referenced by:  recexprlemex  7635
  Copyright terms: Public domain W3C validator