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

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

Proof of Theorem recexprlem1ssl
Dummy variables 𝑧 𝑤 𝑣 𝑢 𝑓 𝑔 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 1prl 7572 . . . 4 (1st ‘1P) = {𝑤𝑤 <Q 1Q}
21abeq2i 2300 . . 3 (𝑤 ∈ (1st ‘1P) ↔ 𝑤 <Q 1Q)
3 rec1nq 7412 . . . . . . 7 (*Q‘1Q) = 1Q
4 ltrnqi 7438 . . . . . . 7 (𝑤 <Q 1Q → (*Q‘1Q) <Q (*Q𝑤))
53, 4eqbrtrrid 4054 . . . . . 6 (𝑤 <Q 1Q → 1Q <Q (*Q𝑤))
6 prop 7492 . . . . . . 7 (𝐴P → ⟨(1st𝐴), (2nd𝐴)⟩ ∈ P)
7 prmuloc2 7584 . . . . . . 7 ((⟨(1st𝐴), (2nd𝐴)⟩ ∈ P ∧ 1Q <Q (*Q𝑤)) → ∃𝑣 ∈ (1st𝐴)(𝑣 ·Q (*Q𝑤)) ∈ (2nd𝐴))
86, 7sylan 283 . . . . . 6 ((𝐴P ∧ 1Q <Q (*Q𝑤)) → ∃𝑣 ∈ (1st𝐴)(𝑣 ·Q (*Q𝑤)) ∈ (2nd𝐴))
95, 8sylan2 286 . . . . 5 ((𝐴P𝑤 <Q 1Q) → ∃𝑣 ∈ (1st𝐴)(𝑣 ·Q (*Q𝑤)) ∈ (2nd𝐴))
10 prnmaxl 7505 . . . . . . . 8 ((⟨(1st𝐴), (2nd𝐴)⟩ ∈ P𝑣 ∈ (1st𝐴)) → ∃𝑧 ∈ (1st𝐴)𝑣 <Q 𝑧)
116, 10sylan 283 . . . . . . 7 ((𝐴P𝑣 ∈ (1st𝐴)) → ∃𝑧 ∈ (1st𝐴)𝑣 <Q 𝑧)
1211ad2ant2r 509 . . . . . 6 (((𝐴P𝑤 <Q 1Q) ∧ (𝑣 ∈ (1st𝐴) ∧ (𝑣 ·Q (*Q𝑤)) ∈ (2nd𝐴))) → ∃𝑧 ∈ (1st𝐴)𝑣 <Q 𝑧)
13 elprnql 7498 . . . . . . . . . . . . . 14 ((⟨(1st𝐴), (2nd𝐴)⟩ ∈ P𝑣 ∈ (1st𝐴)) → 𝑣Q)
146, 13sylan 283 . . . . . . . . . . . . 13 ((𝐴P𝑣 ∈ (1st𝐴)) → 𝑣Q)
1514ad2ant2r 509 . . . . . . . . . . . 12 (((𝐴P𝑤 <Q 1Q) ∧ (𝑣 ∈ (1st𝐴) ∧ (𝑣 ·Q (*Q𝑤)) ∈ (2nd𝐴))) → 𝑣Q)
16153adant3 1019 . . . . . . . . . . 11 (((𝐴P𝑤 <Q 1Q) ∧ (𝑣 ∈ (1st𝐴) ∧ (𝑣 ·Q (*Q𝑤)) ∈ (2nd𝐴)) ∧ 𝑣 <Q 𝑧) → 𝑣Q)
17 simp1r 1024 . . . . . . . . . . . 12 (((𝐴P𝑤 <Q 1Q) ∧ (𝑣 ∈ (1st𝐴) ∧ (𝑣 ·Q (*Q𝑤)) ∈ (2nd𝐴)) ∧ 𝑣 <Q 𝑧) → 𝑤 <Q 1Q)
18 ltrelnq 7382 . . . . . . . . . . . . . 14 <Q ⊆ (Q × Q)
1918brel 4693 . . . . . . . . . . . . 13 (𝑤 <Q 1Q → (𝑤Q ∧ 1QQ))
2019simpld 112 . . . . . . . . . . . 12 (𝑤 <Q 1Q𝑤Q)
2117, 20syl 14 . . . . . . . . . . 11 (((𝐴P𝑤 <Q 1Q) ∧ (𝑣 ∈ (1st𝐴) ∧ (𝑣 ·Q (*Q𝑤)) ∈ (2nd𝐴)) ∧ 𝑣 <Q 𝑧) → 𝑤Q)
22 simp3 1001 . . . . . . . . . . 11 (((𝐴P𝑤 <Q 1Q) ∧ (𝑣 ∈ (1st𝐴) ∧ (𝑣 ·Q (*Q𝑤)) ∈ (2nd𝐴)) ∧ 𝑣 <Q 𝑧) → 𝑣 <Q 𝑧)
23 simp2r 1026 . . . . . . . . . . 11 (((𝐴P𝑤 <Q 1Q) ∧ (𝑣 ∈ (1st𝐴) ∧ (𝑣 ·Q (*Q𝑤)) ∈ (2nd𝐴)) ∧ 𝑣 <Q 𝑧) → (𝑣 ·Q (*Q𝑤)) ∈ (2nd𝐴))
24 simpr 110 . . . . . . . . . . . 12 (((𝑣Q𝑤Q) ∧ (𝑣 <Q 𝑧 ∧ (𝑣 ·Q (*Q𝑤)) ∈ (2nd𝐴))) → (𝑣 <Q 𝑧 ∧ (𝑣 ·Q (*Q𝑤)) ∈ (2nd𝐴)))
25 ltrnqi 7438 . . . . . . . . . . . . . 14 (𝑣 <Q 𝑧 → (*Q𝑧) <Q (*Q𝑣))
26 ltmnqg 7418 . . . . . . . . . . . . . . . 16 ((𝑓Q𝑔QQ) → (𝑓 <Q 𝑔 ↔ ( ·Q 𝑓) <Q ( ·Q 𝑔)))
2726adantl 277 . . . . . . . . . . . . . . 15 ((((𝑣Q𝑤Q) ∧ (𝑣 <Q 𝑧 ∧ (𝑣 ·Q (*Q𝑤)) ∈ (2nd𝐴))) ∧ (𝑓Q𝑔QQ)) → (𝑓 <Q 𝑔 ↔ ( ·Q 𝑓) <Q ( ·Q 𝑔)))
28 simprl 529 . . . . . . . . . . . . . . . 16 (((𝑣Q𝑤Q) ∧ (𝑣 <Q 𝑧 ∧ (𝑣 ·Q (*Q𝑤)) ∈ (2nd𝐴))) → 𝑣 <Q 𝑧)
2918brel 4693 . . . . . . . . . . . . . . . . 17 (𝑣 <Q 𝑧 → (𝑣Q𝑧Q))
3029simprd 114 . . . . . . . . . . . . . . . 16 (𝑣 <Q 𝑧𝑧Q)
31 recclnq 7409 . . . . . . . . . . . . . . . 16 (𝑧Q → (*Q𝑧) ∈ Q)
3228, 30, 313syl 17 . . . . . . . . . . . . . . 15 (((𝑣Q𝑤Q) ∧ (𝑣 <Q 𝑧 ∧ (𝑣 ·Q (*Q𝑤)) ∈ (2nd𝐴))) → (*Q𝑧) ∈ Q)
33 recclnq 7409 . . . . . . . . . . . . . . . 16 (𝑣Q → (*Q𝑣) ∈ Q)
3433ad2antrr 488 . . . . . . . . . . . . . . 15 (((𝑣Q𝑤Q) ∧ (𝑣 <Q 𝑧 ∧ (𝑣 ·Q (*Q𝑤)) ∈ (2nd𝐴))) → (*Q𝑣) ∈ Q)
35 simplr 528 . . . . . . . . . . . . . . 15 (((𝑣Q𝑤Q) ∧ (𝑣 <Q 𝑧 ∧ (𝑣 ·Q (*Q𝑤)) ∈ (2nd𝐴))) → 𝑤Q)
36 mulcomnqg 7400 . . . . . . . . . . . . . . . 16 ((𝑓Q𝑔Q) → (𝑓 ·Q 𝑔) = (𝑔 ·Q 𝑓))
3736adantl 277 . . . . . . . . . . . . . . 15 ((((𝑣Q𝑤Q) ∧ (𝑣 <Q 𝑧 ∧ (𝑣 ·Q (*Q𝑤)) ∈ (2nd𝐴))) ∧ (𝑓Q𝑔Q)) → (𝑓 ·Q 𝑔) = (𝑔 ·Q 𝑓))
3827, 32, 34, 35, 37caovord2d 6061 . . . . . . . . . . . . . 14 (((𝑣Q𝑤Q) ∧ (𝑣 <Q 𝑧 ∧ (𝑣 ·Q (*Q𝑤)) ∈ (2nd𝐴))) → ((*Q𝑧) <Q (*Q𝑣) ↔ ((*Q𝑧) ·Q 𝑤) <Q ((*Q𝑣) ·Q 𝑤)))
3925, 38imbitrid 154 . . . . . . . . . . . . 13 (((𝑣Q𝑤Q) ∧ (𝑣 <Q 𝑧 ∧ (𝑣 ·Q (*Q𝑤)) ∈ (2nd𝐴))) → (𝑣 <Q 𝑧 → ((*Q𝑧) ·Q 𝑤) <Q ((*Q𝑣) ·Q 𝑤)))
40 mulcomnqg 7400 . . . . . . . . . . . . . . . . . . . . . 22 ((𝑣Q ∧ (*Q𝑣) ∈ Q) → (𝑣 ·Q (*Q𝑣)) = ((*Q𝑣) ·Q 𝑣))
4133, 40mpdan 421 . . . . . . . . . . . . . . . . . . . . 21 (𝑣Q → (𝑣 ·Q (*Q𝑣)) = ((*Q𝑣) ·Q 𝑣))
42 recidnq 7410 . . . . . . . . . . . . . . . . . . . . 21 (𝑣Q → (𝑣 ·Q (*Q𝑣)) = 1Q)
4341, 42eqtr3d 2224 . . . . . . . . . . . . . . . . . . . 20 (𝑣Q → ((*Q𝑣) ·Q 𝑣) = 1Q)
44 recidnq 7410 . . . . . . . . . . . . . . . . . . . 20 (𝑤Q → (𝑤 ·Q (*Q𝑤)) = 1Q)
4543, 44oveqan12d 5910 . . . . . . . . . . . . . . . . . . 19 ((𝑣Q𝑤Q) → (((*Q𝑣) ·Q 𝑣) ·Q (𝑤 ·Q (*Q𝑤))) = (1Q ·Q 1Q))
4645adantr 276 . . . . . . . . . . . . . . . . . 18 (((𝑣Q𝑤Q) ∧ (𝑣 <Q 𝑧 ∧ (𝑣 ·Q (*Q𝑤)) ∈ (2nd𝐴))) → (((*Q𝑣) ·Q 𝑣) ·Q (𝑤 ·Q (*Q𝑤))) = (1Q ·Q 1Q))
47 simpll 527 . . . . . . . . . . . . . . . . . . 19 (((𝑣Q𝑤Q) ∧ (𝑣 <Q 𝑧 ∧ (𝑣 ·Q (*Q𝑤)) ∈ (2nd𝐴))) → 𝑣Q)
48 mulassnqg 7401 . . . . . . . . . . . . . . . . . . . 20 ((𝑓Q𝑔QQ) → ((𝑓 ·Q 𝑔) ·Q ) = (𝑓 ·Q (𝑔 ·Q )))
4948adantl 277 . . . . . . . . . . . . . . . . . . 19 ((((𝑣Q𝑤Q) ∧ (𝑣 <Q 𝑧 ∧ (𝑣 ·Q (*Q𝑤)) ∈ (2nd𝐴))) ∧ (𝑓Q𝑔QQ)) → ((𝑓 ·Q 𝑔) ·Q ) = (𝑓 ·Q (𝑔 ·Q )))
50 recclnq 7409 . . . . . . . . . . . . . . . . . . . 20 (𝑤Q → (*Q𝑤) ∈ Q)
5135, 50syl 14 . . . . . . . . . . . . . . . . . . 19 (((𝑣Q𝑤Q) ∧ (𝑣 <Q 𝑧 ∧ (𝑣 ·Q (*Q𝑤)) ∈ (2nd𝐴))) → (*Q𝑤) ∈ Q)
52 mulclnq 7393 . . . . . . . . . . . . . . . . . . . 20 ((𝑓Q𝑔Q) → (𝑓 ·Q 𝑔) ∈ Q)
5352adantl 277 . . . . . . . . . . . . . . . . . . 19 ((((𝑣Q𝑤Q) ∧ (𝑣 <Q 𝑧 ∧ (𝑣 ·Q (*Q𝑤)) ∈ (2nd𝐴))) ∧ (𝑓Q𝑔Q)) → (𝑓 ·Q 𝑔) ∈ Q)
5434, 47, 35, 37, 49, 51, 53caov4d 6076 . . . . . . . . . . . . . . . . . 18 (((𝑣Q𝑤Q) ∧ (𝑣 <Q 𝑧 ∧ (𝑣 ·Q (*Q𝑤)) ∈ (2nd𝐴))) → (((*Q𝑣) ·Q 𝑣) ·Q (𝑤 ·Q (*Q𝑤))) = (((*Q𝑣) ·Q 𝑤) ·Q (𝑣 ·Q (*Q𝑤))))
5546, 54eqtr3d 2224 . . . . . . . . . . . . . . . . 17 (((𝑣Q𝑤Q) ∧ (𝑣 <Q 𝑧 ∧ (𝑣 ·Q (*Q𝑤)) ∈ (2nd𝐴))) → (1Q ·Q 1Q) = (((*Q𝑣) ·Q 𝑤) ·Q (𝑣 ·Q (*Q𝑤))))
56 1nq 7383 . . . . . . . . . . . . . . . . . 18 1QQ
57 mulidnq 7406 . . . . . . . . . . . . . . . . . 18 (1QQ → (1Q ·Q 1Q) = 1Q)
5856, 57ax-mp 5 . . . . . . . . . . . . . . . . 17 (1Q ·Q 1Q) = 1Q
5955, 58eqtr3di 2237 . . . . . . . . . . . . . . . 16 (((𝑣Q𝑤Q) ∧ (𝑣 <Q 𝑧 ∧ (𝑣 ·Q (*Q𝑤)) ∈ (2nd𝐴))) → (((*Q𝑣) ·Q 𝑤) ·Q (𝑣 ·Q (*Q𝑤))) = 1Q)
60 mulclnq 7393 . . . . . . . . . . . . . . . . . . 19 (((*Q𝑣) ∈ Q𝑤Q) → ((*Q𝑣) ·Q 𝑤) ∈ Q)
6133, 60sylan 283 . . . . . . . . . . . . . . . . . 18 ((𝑣Q𝑤Q) → ((*Q𝑣) ·Q 𝑤) ∈ Q)
62 mulclnq 7393 . . . . . . . . . . . . . . . . . . 19 ((𝑣Q ∧ (*Q𝑤) ∈ Q) → (𝑣 ·Q (*Q𝑤)) ∈ Q)
6350, 62sylan2 286 . . . . . . . . . . . . . . . . . 18 ((𝑣Q𝑤Q) → (𝑣 ·Q (*Q𝑤)) ∈ Q)
64 recmulnqg 7408 . . . . . . . . . . . . . . . . . 18 ((((*Q𝑣) ·Q 𝑤) ∈ Q ∧ (𝑣 ·Q (*Q𝑤)) ∈ Q) → ((*Q‘((*Q𝑣) ·Q 𝑤)) = (𝑣 ·Q (*Q𝑤)) ↔ (((*Q𝑣) ·Q 𝑤) ·Q (𝑣 ·Q (*Q𝑤))) = 1Q))
6561, 63, 64syl2anc 411 . . . . . . . . . . . . . . . . 17 ((𝑣Q𝑤Q) → ((*Q‘((*Q𝑣) ·Q 𝑤)) = (𝑣 ·Q (*Q𝑤)) ↔ (((*Q𝑣) ·Q 𝑤) ·Q (𝑣 ·Q (*Q𝑤))) = 1Q))
6665adantr 276 . . . . . . . . . . . . . . . 16 (((𝑣Q𝑤Q) ∧ (𝑣 <Q 𝑧 ∧ (𝑣 ·Q (*Q𝑤)) ∈ (2nd𝐴))) → ((*Q‘((*Q𝑣) ·Q 𝑤)) = (𝑣 ·Q (*Q𝑤)) ↔ (((*Q𝑣) ·Q 𝑤) ·Q (𝑣 ·Q (*Q𝑤))) = 1Q))
6759, 66mpbird 167 . . . . . . . . . . . . . . 15 (((𝑣Q𝑤Q) ∧ (𝑣 <Q 𝑧 ∧ (𝑣 ·Q (*Q𝑤)) ∈ (2nd𝐴))) → (*Q‘((*Q𝑣) ·Q 𝑤)) = (𝑣 ·Q (*Q𝑤)))
6867eleq1d 2258 . . . . . . . . . . . . . 14 (((𝑣Q𝑤Q) ∧ (𝑣 <Q 𝑧 ∧ (𝑣 ·Q (*Q𝑤)) ∈ (2nd𝐴))) → ((*Q‘((*Q𝑣) ·Q 𝑤)) ∈ (2nd𝐴) ↔ (𝑣 ·Q (*Q𝑤)) ∈ (2nd𝐴)))
6968biimprd 158 . . . . . . . . . . . . 13 (((𝑣Q𝑤Q) ∧ (𝑣 <Q 𝑧 ∧ (𝑣 ·Q (*Q𝑤)) ∈ (2nd𝐴))) → ((𝑣 ·Q (*Q𝑤)) ∈ (2nd𝐴) → (*Q‘((*Q𝑣) ·Q 𝑤)) ∈ (2nd𝐴)))
70 breq2 4022 . . . . . . . . . . . . . . . . . 18 (𝑦 = ((*Q𝑣) ·Q 𝑤) → (((*Q𝑧) ·Q 𝑤) <Q 𝑦 ↔ ((*Q𝑧) ·Q 𝑤) <Q ((*Q𝑣) ·Q 𝑤)))
71 fveq2 5530 . . . . . . . . . . . . . . . . . . 19 (𝑦 = ((*Q𝑣) ·Q 𝑤) → (*Q𝑦) = (*Q‘((*Q𝑣) ·Q 𝑤)))
7271eleq1d 2258 . . . . . . . . . . . . . . . . . 18 (𝑦 = ((*Q𝑣) ·Q 𝑤) → ((*Q𝑦) ∈ (2nd𝐴) ↔ (*Q‘((*Q𝑣) ·Q 𝑤)) ∈ (2nd𝐴)))
7370, 72anbi12d 473 . . . . . . . . . . . . . . . . 17 (𝑦 = ((*Q𝑣) ·Q 𝑤) → ((((*Q𝑧) ·Q 𝑤) <Q 𝑦 ∧ (*Q𝑦) ∈ (2nd𝐴)) ↔ (((*Q𝑧) ·Q 𝑤) <Q ((*Q𝑣) ·Q 𝑤) ∧ (*Q‘((*Q𝑣) ·Q 𝑤)) ∈ (2nd𝐴))))
7473spcegv 2840 . . . . . . . . . . . . . . . 16 (((*Q𝑣) ·Q 𝑤) ∈ Q → ((((*Q𝑧) ·Q 𝑤) <Q ((*Q𝑣) ·Q 𝑤) ∧ (*Q‘((*Q𝑣) ·Q 𝑤)) ∈ (2nd𝐴)) → ∃𝑦(((*Q𝑧) ·Q 𝑤) <Q 𝑦 ∧ (*Q𝑦) ∈ (2nd𝐴))))
7561, 74syl 14 . . . . . . . . . . . . . . 15 ((𝑣Q𝑤Q) → ((((*Q𝑧) ·Q 𝑤) <Q ((*Q𝑣) ·Q 𝑤) ∧ (*Q‘((*Q𝑣) ·Q 𝑤)) ∈ (2nd𝐴)) → ∃𝑦(((*Q𝑧) ·Q 𝑤) <Q 𝑦 ∧ (*Q𝑦) ∈ (2nd𝐴))))
76 recexpr.1 . . . . . . . . . . . . . . . 16 𝐵 = ⟨{𝑥 ∣ ∃𝑦(𝑥 <Q 𝑦 ∧ (*Q𝑦) ∈ (2nd𝐴))}, {𝑥 ∣ ∃𝑦(𝑦 <Q 𝑥 ∧ (*Q𝑦) ∈ (1st𝐴))}⟩
7776recexprlemell 7639 . . . . . . . . . . . . . . 15 (((*Q𝑧) ·Q 𝑤) ∈ (1st𝐵) ↔ ∃𝑦(((*Q𝑧) ·Q 𝑤) <Q 𝑦 ∧ (*Q𝑦) ∈ (2nd𝐴)))
7875, 77imbitrrdi 162 . . . . . . . . . . . . . 14 ((𝑣Q𝑤Q) → ((((*Q𝑧) ·Q 𝑤) <Q ((*Q𝑣) ·Q 𝑤) ∧ (*Q‘((*Q𝑣) ·Q 𝑤)) ∈ (2nd𝐴)) → ((*Q𝑧) ·Q 𝑤) ∈ (1st𝐵)))
7978adantr 276 . . . . . . . . . . . . 13 (((𝑣Q𝑤Q) ∧ (𝑣 <Q 𝑧 ∧ (𝑣 ·Q (*Q𝑤)) ∈ (2nd𝐴))) → ((((*Q𝑧) ·Q 𝑤) <Q ((*Q𝑣) ·Q 𝑤) ∧ (*Q‘((*Q𝑣) ·Q 𝑤)) ∈ (2nd𝐴)) → ((*Q𝑧) ·Q 𝑤) ∈ (1st𝐵)))
8039, 69, 79syl2and 295 . . . . . . . . . . . 12 (((𝑣Q𝑤Q) ∧ (𝑣 <Q 𝑧 ∧ (𝑣 ·Q (*Q𝑤)) ∈ (2nd𝐴))) → ((𝑣 <Q 𝑧 ∧ (𝑣 ·Q (*Q𝑤)) ∈ (2nd𝐴)) → ((*Q𝑧) ·Q 𝑤) ∈ (1st𝐵)))
8124, 80mpd 13 . . . . . . . . . . 11 (((𝑣Q𝑤Q) ∧ (𝑣 <Q 𝑧 ∧ (𝑣 ·Q (*Q𝑤)) ∈ (2nd𝐴))) → ((*Q𝑧) ·Q 𝑤) ∈ (1st𝐵))
8216, 21, 22, 23, 81syl22anc 1250 . . . . . . . . . 10 (((𝐴P𝑤 <Q 1Q) ∧ (𝑣 ∈ (1st𝐴) ∧ (𝑣 ·Q (*Q𝑤)) ∈ (2nd𝐴)) ∧ 𝑣 <Q 𝑧) → ((*Q𝑧) ·Q 𝑤) ∈ (1st𝐵))
83303ad2ant3 1022 . . . . . . . . . . 11 (((𝐴P𝑤 <Q 1Q) ∧ (𝑣 ∈ (1st𝐴) ∧ (𝑣 ·Q (*Q𝑤)) ∈ (2nd𝐴)) ∧ 𝑣 <Q 𝑧) → 𝑧Q)
84 mulidnq 7406 . . . . . . . . . . . . . 14 (𝑤Q → (𝑤 ·Q 1Q) = 𝑤)
85 mulcomnqg 7400 . . . . . . . . . . . . . . 15 ((𝑤Q ∧ 1QQ) → (𝑤 ·Q 1Q) = (1Q ·Q 𝑤))
8656, 85mpan2 425 . . . . . . . . . . . . . 14 (𝑤Q → (𝑤 ·Q 1Q) = (1Q ·Q 𝑤))
8784, 86eqtr3d 2224 . . . . . . . . . . . . 13 (𝑤Q𝑤 = (1Q ·Q 𝑤))
8887adantl 277 . . . . . . . . . . . 12 ((𝑧Q𝑤Q) → 𝑤 = (1Q ·Q 𝑤))
89 recidnq 7410 . . . . . . . . . . . . . 14 (𝑧Q → (𝑧 ·Q (*Q𝑧)) = 1Q)
9089oveq1d 5906 . . . . . . . . . . . . 13 (𝑧Q → ((𝑧 ·Q (*Q𝑧)) ·Q 𝑤) = (1Q ·Q 𝑤))
9190adantr 276 . . . . . . . . . . . 12 ((𝑧Q𝑤Q) → ((𝑧 ·Q (*Q𝑧)) ·Q 𝑤) = (1Q ·Q 𝑤))
92 mulassnqg 7401 . . . . . . . . . . . . . 14 ((𝑧Q ∧ (*Q𝑧) ∈ Q𝑤Q) → ((𝑧 ·Q (*Q𝑧)) ·Q 𝑤) = (𝑧 ·Q ((*Q𝑧) ·Q 𝑤)))
9331, 92syl3an2 1283 . . . . . . . . . . . . 13 ((𝑧Q𝑧Q𝑤Q) → ((𝑧 ·Q (*Q𝑧)) ·Q 𝑤) = (𝑧 ·Q ((*Q𝑧) ·Q 𝑤)))
94933anidm12 1306 . . . . . . . . . . . 12 ((𝑧Q𝑤Q) → ((𝑧 ·Q (*Q𝑧)) ·Q 𝑤) = (𝑧 ·Q ((*Q𝑧) ·Q 𝑤)))
9588, 91, 943eqtr2d 2228 . . . . . . . . . . 11 ((𝑧Q𝑤Q) → 𝑤 = (𝑧 ·Q ((*Q𝑧) ·Q 𝑤)))
9683, 21, 95syl2anc 411 . . . . . . . . . 10 (((𝐴P𝑤 <Q 1Q) ∧ (𝑣 ∈ (1st𝐴) ∧ (𝑣 ·Q (*Q𝑤)) ∈ (2nd𝐴)) ∧ 𝑣 <Q 𝑧) → 𝑤 = (𝑧 ·Q ((*Q𝑧) ·Q 𝑤)))
97 oveq2 5899 . . . . . . . . . . . 12 (𝑥 = ((*Q𝑧) ·Q 𝑤) → (𝑧 ·Q 𝑥) = (𝑧 ·Q ((*Q𝑧) ·Q 𝑤)))
9897eqeq2d 2201 . . . . . . . . . . 11 (𝑥 = ((*Q𝑧) ·Q 𝑤) → (𝑤 = (𝑧 ·Q 𝑥) ↔ 𝑤 = (𝑧 ·Q ((*Q𝑧) ·Q 𝑤))))
9998rspcev 2856 . . . . . . . . . 10 ((((*Q𝑧) ·Q 𝑤) ∈ (1st𝐵) ∧ 𝑤 = (𝑧 ·Q ((*Q𝑧) ·Q 𝑤))) → ∃𝑥 ∈ (1st𝐵)𝑤 = (𝑧 ·Q 𝑥))
10082, 96, 99syl2anc 411 . . . . . . . . 9 (((𝐴P𝑤 <Q 1Q) ∧ (𝑣 ∈ (1st𝐴) ∧ (𝑣 ·Q (*Q𝑤)) ∈ (2nd𝐴)) ∧ 𝑣 <Q 𝑧) → ∃𝑥 ∈ (1st𝐵)𝑤 = (𝑧 ·Q 𝑥))
1011003expia 1207 . . . . . . . 8 (((𝐴P𝑤 <Q 1Q) ∧ (𝑣 ∈ (1st𝐴) ∧ (𝑣 ·Q (*Q𝑤)) ∈ (2nd𝐴))) → (𝑣 <Q 𝑧 → ∃𝑥 ∈ (1st𝐵)𝑤 = (𝑧 ·Q 𝑥)))
102101reximdv 2591 . . . . . . 7 (((𝐴P𝑤 <Q 1Q) ∧ (𝑣 ∈ (1st𝐴) ∧ (𝑣 ·Q (*Q𝑤)) ∈ (2nd𝐴))) → (∃𝑧 ∈ (1st𝐴)𝑣 <Q 𝑧 → ∃𝑧 ∈ (1st𝐴)∃𝑥 ∈ (1st𝐵)𝑤 = (𝑧 ·Q 𝑥)))
10376recexprlempr 7649 . . . . . . . . 9 (𝐴P𝐵P)
104 df-imp 7486 . . . . . . . . . 10 ·P = (𝑦P, 𝑤P ↦ ⟨{𝑢Q ∣ ∃𝑓Q𝑔Q (𝑓 ∈ (1st𝑦) ∧ 𝑔 ∈ (1st𝑤) ∧ 𝑢 = (𝑓 ·Q 𝑔))}, {𝑢Q ∣ ∃𝑓Q𝑔Q (𝑓 ∈ (2nd𝑦) ∧ 𝑔 ∈ (2nd𝑤) ∧ 𝑢 = (𝑓 ·Q 𝑔))}⟩)
105104, 52genpelvl 7529 . . . . . . . . 9 ((𝐴P𝐵P) → (𝑤 ∈ (1st ‘(𝐴 ·P 𝐵)) ↔ ∃𝑧 ∈ (1st𝐴)∃𝑥 ∈ (1st𝐵)𝑤 = (𝑧 ·Q 𝑥)))
106103, 105mpdan 421 . . . . . . . 8 (𝐴P → (𝑤 ∈ (1st ‘(𝐴 ·P 𝐵)) ↔ ∃𝑧 ∈ (1st𝐴)∃𝑥 ∈ (1st𝐵)𝑤 = (𝑧 ·Q 𝑥)))
107106ad2antrr 488 . . . . . . 7 (((𝐴P𝑤 <Q 1Q) ∧ (𝑣 ∈ (1st𝐴) ∧ (𝑣 ·Q (*Q𝑤)) ∈ (2nd𝐴))) → (𝑤 ∈ (1st ‘(𝐴 ·P 𝐵)) ↔ ∃𝑧 ∈ (1st𝐴)∃𝑥 ∈ (1st𝐵)𝑤 = (𝑧 ·Q 𝑥)))
108102, 107sylibrd 169 . . . . . 6 (((𝐴P𝑤 <Q 1Q) ∧ (𝑣 ∈ (1st𝐴) ∧ (𝑣 ·Q (*Q𝑤)) ∈ (2nd𝐴))) → (∃𝑧 ∈ (1st𝐴)𝑣 <Q 𝑧𝑤 ∈ (1st ‘(𝐴 ·P 𝐵))))
10912, 108mpd 13 . . . . 5 (((𝐴P𝑤 <Q 1Q) ∧ (𝑣 ∈ (1st𝐴) ∧ (𝑣 ·Q (*Q𝑤)) ∈ (2nd𝐴))) → 𝑤 ∈ (1st ‘(𝐴 ·P 𝐵)))
1109, 109rexlimddv 2612 . . . 4 ((𝐴P𝑤 <Q 1Q) → 𝑤 ∈ (1st ‘(𝐴 ·P 𝐵)))
111110ex 115 . . 3 (𝐴P → (𝑤 <Q 1Q𝑤 ∈ (1st ‘(𝐴 ·P 𝐵))))
1122, 111biimtrid 152 . 2 (𝐴P → (𝑤 ∈ (1st ‘1P) → 𝑤 ∈ (1st ‘(𝐴 ·P 𝐵))))
113112ssrdv 3176 1 (𝐴P → (1st ‘1P) ⊆ (1st ‘(𝐴 ·P 𝐵)))
Colors of variables: wff set class
Syntax hints:  wi 4  wa 104  wb 105  w3a 980   = wceq 1364  wex 1503  wcel 2160  {cab 2175  wrex 2469  wss 3144  cop 3610   class class class wbr 4018  cfv 5231  (class class class)co 5891  1st c1st 6157  2nd c2nd 6158  Qcnq 7297  1Qc1q 7298   ·Q cmq 7300  *Qcrq 7301   <Q cltq 7302  Pcnp 7308  1Pc1p 7309   ·P cmp 7311
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 615  ax-in2 616  ax-io 710  ax-5 1458  ax-7 1459  ax-gen 1460  ax-ie1 1504  ax-ie2 1505  ax-8 1515  ax-10 1516  ax-11 1517  ax-i12 1518  ax-bndl 1520  ax-4 1521  ax-17 1537  ax-i9 1541  ax-ial 1545  ax-i5r 1546  ax-13 2162  ax-14 2163  ax-ext 2171  ax-coll 4133  ax-sep 4136  ax-nul 4144  ax-pow 4189  ax-pr 4224  ax-un 4448  ax-setind 4551  ax-iinf 4602
This theorem depends on definitions:  df-bi 117  df-dc 836  df-3or 981  df-3an 982  df-tru 1367  df-fal 1370  df-nf 1472  df-sb 1774  df-eu 2041  df-mo 2042  df-clab 2176  df-cleq 2182  df-clel 2185  df-nfc 2321  df-ne 2361  df-ral 2473  df-rex 2474  df-reu 2475  df-rab 2477  df-v 2754  df-sbc 2978  df-csb 3073  df-dif 3146  df-un 3148  df-in 3150  df-ss 3157  df-nul 3438  df-pw 3592  df-sn 3613  df-pr 3614  df-op 3616  df-uni 3825  df-int 3860  df-iun 3903  df-br 4019  df-opab 4080  df-mpt 4081  df-tr 4117  df-eprel 4304  df-id 4308  df-po 4311  df-iso 4312  df-iord 4381  df-on 4383  df-suc 4386  df-iom 4605  df-xp 4647  df-rel 4648  df-cnv 4649  df-co 4650  df-dm 4651  df-rn 4652  df-res 4653  df-ima 4654  df-iota 5193  df-fun 5233  df-fn 5234  df-f 5235  df-f1 5236  df-fo 5237  df-f1o 5238  df-fv 5239  df-ov 5894  df-oprab 5895  df-mpo 5896  df-1st 6159  df-2nd 6160  df-recs 6324  df-irdg 6389  df-1o 6435  df-2o 6436  df-oadd 6439  df-omul 6440  df-er 6553  df-ec 6555  df-qs 6559  df-ni 7321  df-pli 7322  df-mi 7323  df-lti 7324  df-plpq 7361  df-mpq 7362  df-enq 7364  df-nqqs 7365  df-plqqs 7366  df-mqqs 7367  df-1nqqs 7368  df-rq 7369  df-ltnqqs 7370  df-enq0 7441  df-nq0 7442  df-0nq0 7443  df-plq0 7444  df-mq0 7445  df-inp 7483  df-i1p 7484  df-imp 7486
This theorem is referenced by:  recexprlemex  7654
  Copyright terms: Public domain W3C validator