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

Theorem recexprlem1ssl 7255
Description: The lower cut of one is a subset of the lower cut of 𝐴 ·P 𝐵. Lemma for recexpr 7260. (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 7177 . . . 4 (1st ‘1P) = {𝑤𝑤 <Q 1Q}
21abeq2i 2199 . . 3 (𝑤 ∈ (1st ‘1P) ↔ 𝑤 <Q 1Q)
3 rec1nq 7017 . . . . . . 7 (*Q‘1Q) = 1Q
4 ltrnqi 7043 . . . . . . 7 (𝑤 <Q 1Q → (*Q‘1Q) <Q (*Q𝑤))
53, 4syl5eqbrr 3887 . . . . . 6 (𝑤 <Q 1Q → 1Q <Q (*Q𝑤))
6 prop 7097 . . . . . . 7 (𝐴P → ⟨(1st𝐴), (2nd𝐴)⟩ ∈ P)
7 prmuloc2 7189 . . . . . . 7 ((⟨(1st𝐴), (2nd𝐴)⟩ ∈ P ∧ 1Q <Q (*Q𝑤)) → ∃𝑣 ∈ (1st𝐴)(𝑣 ·Q (*Q𝑤)) ∈ (2nd𝐴))
86, 7sylan 278 . . . . . 6 ((𝐴P ∧ 1Q <Q (*Q𝑤)) → ∃𝑣 ∈ (1st𝐴)(𝑣 ·Q (*Q𝑤)) ∈ (2nd𝐴))
95, 8sylan2 281 . . . . 5 ((𝐴P𝑤 <Q 1Q) → ∃𝑣 ∈ (1st𝐴)(𝑣 ·Q (*Q𝑤)) ∈ (2nd𝐴))
10 prnmaxl 7110 . . . . . . . 8 ((⟨(1st𝐴), (2nd𝐴)⟩ ∈ P𝑣 ∈ (1st𝐴)) → ∃𝑧 ∈ (1st𝐴)𝑣 <Q 𝑧)
116, 10sylan 278 . . . . . . 7 ((𝐴P𝑣 ∈ (1st𝐴)) → ∃𝑧 ∈ (1st𝐴)𝑣 <Q 𝑧)
1211ad2ant2r 494 . . . . . 6 (((𝐴P𝑤 <Q 1Q) ∧ (𝑣 ∈ (1st𝐴) ∧ (𝑣 ·Q (*Q𝑤)) ∈ (2nd𝐴))) → ∃𝑧 ∈ (1st𝐴)𝑣 <Q 𝑧)
13 elprnql 7103 . . . . . . . . . . . . . 14 ((⟨(1st𝐴), (2nd𝐴)⟩ ∈ P𝑣 ∈ (1st𝐴)) → 𝑣Q)
146, 13sylan 278 . . . . . . . . . . . . 13 ((𝐴P𝑣 ∈ (1st𝐴)) → 𝑣Q)
1514ad2ant2r 494 . . . . . . . . . . . 12 (((𝐴P𝑤 <Q 1Q) ∧ (𝑣 ∈ (1st𝐴) ∧ (𝑣 ·Q (*Q𝑤)) ∈ (2nd𝐴))) → 𝑣Q)
16153adant3 964 . . . . . . . . . . 11 (((𝐴P𝑤 <Q 1Q) ∧ (𝑣 ∈ (1st𝐴) ∧ (𝑣 ·Q (*Q𝑤)) ∈ (2nd𝐴)) ∧ 𝑣 <Q 𝑧) → 𝑣Q)
17 simp1r 969 . . . . . . . . . . . 12 (((𝐴P𝑤 <Q 1Q) ∧ (𝑣 ∈ (1st𝐴) ∧ (𝑣 ·Q (*Q𝑤)) ∈ (2nd𝐴)) ∧ 𝑣 <Q 𝑧) → 𝑤 <Q 1Q)
18 ltrelnq 6987 . . . . . . . . . . . . . 14 <Q ⊆ (Q × Q)
1918brel 4505 . . . . . . . . . . . . 13 (𝑤 <Q 1Q → (𝑤Q ∧ 1QQ))
2019simpld 111 . . . . . . . . . . . 12 (𝑤 <Q 1Q𝑤Q)
2117, 20syl 14 . . . . . . . . . . 11 (((𝐴P𝑤 <Q 1Q) ∧ (𝑣 ∈ (1st𝐴) ∧ (𝑣 ·Q (*Q𝑤)) ∈ (2nd𝐴)) ∧ 𝑣 <Q 𝑧) → 𝑤Q)
22 simp3 946 . . . . . . . . . . 11 (((𝐴P𝑤 <Q 1Q) ∧ (𝑣 ∈ (1st𝐴) ∧ (𝑣 ·Q (*Q𝑤)) ∈ (2nd𝐴)) ∧ 𝑣 <Q 𝑧) → 𝑣 <Q 𝑧)
23 simp2r 971 . . . . . . . . . . 11 (((𝐴P𝑤 <Q 1Q) ∧ (𝑣 ∈ (1st𝐴) ∧ (𝑣 ·Q (*Q𝑤)) ∈ (2nd𝐴)) ∧ 𝑣 <Q 𝑧) → (𝑣 ·Q (*Q𝑤)) ∈ (2nd𝐴))
24 simpr 109 . . . . . . . . . . . 12 (((𝑣Q𝑤Q) ∧ (𝑣 <Q 𝑧 ∧ (𝑣 ·Q (*Q𝑤)) ∈ (2nd𝐴))) → (𝑣 <Q 𝑧 ∧ (𝑣 ·Q (*Q𝑤)) ∈ (2nd𝐴)))
25 ltrnqi 7043 . . . . . . . . . . . . . 14 (𝑣 <Q 𝑧 → (*Q𝑧) <Q (*Q𝑣))
26 ltmnqg 7023 . . . . . . . . . . . . . . . 16 ((𝑓Q𝑔QQ) → (𝑓 <Q 𝑔 ↔ ( ·Q 𝑓) <Q ( ·Q 𝑔)))
2726adantl 272 . . . . . . . . . . . . . . 15 ((((𝑣Q𝑤Q) ∧ (𝑣 <Q 𝑧 ∧ (𝑣 ·Q (*Q𝑤)) ∈ (2nd𝐴))) ∧ (𝑓Q𝑔QQ)) → (𝑓 <Q 𝑔 ↔ ( ·Q 𝑓) <Q ( ·Q 𝑔)))
28 simprl 499 . . . . . . . . . . . . . . . 16 (((𝑣Q𝑤Q) ∧ (𝑣 <Q 𝑧 ∧ (𝑣 ·Q (*Q𝑤)) ∈ (2nd𝐴))) → 𝑣 <Q 𝑧)
2918brel 4505 . . . . . . . . . . . . . . . . 17 (𝑣 <Q 𝑧 → (𝑣Q𝑧Q))
3029simprd 113 . . . . . . . . . . . . . . . 16 (𝑣 <Q 𝑧𝑧Q)
31 recclnq 7014 . . . . . . . . . . . . . . . 16 (𝑧Q → (*Q𝑧) ∈ Q)
3228, 30, 313syl 17 . . . . . . . . . . . . . . 15 (((𝑣Q𝑤Q) ∧ (𝑣 <Q 𝑧 ∧ (𝑣 ·Q (*Q𝑤)) ∈ (2nd𝐴))) → (*Q𝑧) ∈ Q)
33 recclnq 7014 . . . . . . . . . . . . . . . 16 (𝑣Q → (*Q𝑣) ∈ Q)
3433ad2antrr 473 . . . . . . . . . . . . . . 15 (((𝑣Q𝑤Q) ∧ (𝑣 <Q 𝑧 ∧ (𝑣 ·Q (*Q𝑤)) ∈ (2nd𝐴))) → (*Q𝑣) ∈ Q)
35 simplr 498 . . . . . . . . . . . . . . 15 (((𝑣Q𝑤Q) ∧ (𝑣 <Q 𝑧 ∧ (𝑣 ·Q (*Q𝑤)) ∈ (2nd𝐴))) → 𝑤Q)
36 mulcomnqg 7005 . . . . . . . . . . . . . . . 16 ((𝑓Q𝑔Q) → (𝑓 ·Q 𝑔) = (𝑔 ·Q 𝑓))
3736adantl 272 . . . . . . . . . . . . . . 15 ((((𝑣Q𝑤Q) ∧ (𝑣 <Q 𝑧 ∧ (𝑣 ·Q (*Q𝑤)) ∈ (2nd𝐴))) ∧ (𝑓Q𝑔Q)) → (𝑓 ·Q 𝑔) = (𝑔 ·Q 𝑓))
3827, 32, 34, 35, 37caovord2d 5830 . . . . . . . . . . . . . 14 (((𝑣Q𝑤Q) ∧ (𝑣 <Q 𝑧 ∧ (𝑣 ·Q (*Q𝑤)) ∈ (2nd𝐴))) → ((*Q𝑧) <Q (*Q𝑣) ↔ ((*Q𝑧) ·Q 𝑤) <Q ((*Q𝑣) ·Q 𝑤)))
3925, 38syl5ib 153 . . . . . . . . . . . . 13 (((𝑣Q𝑤Q) ∧ (𝑣 <Q 𝑧 ∧ (𝑣 ·Q (*Q𝑤)) ∈ (2nd𝐴))) → (𝑣 <Q 𝑧 → ((*Q𝑧) ·Q 𝑤) <Q ((*Q𝑣) ·Q 𝑤)))
40 1nq 6988 . . . . . . . . . . . . . . . . . 18 1QQ
41 mulidnq 7011 . . . . . . . . . . . . . . . . . 18 (1QQ → (1Q ·Q 1Q) = 1Q)
4240, 41ax-mp 7 . . . . . . . . . . . . . . . . 17 (1Q ·Q 1Q) = 1Q
43 mulcomnqg 7005 . . . . . . . . . . . . . . . . . . . . . 22 ((𝑣Q ∧ (*Q𝑣) ∈ Q) → (𝑣 ·Q (*Q𝑣)) = ((*Q𝑣) ·Q 𝑣))
4433, 43mpdan 413 . . . . . . . . . . . . . . . . . . . . 21 (𝑣Q → (𝑣 ·Q (*Q𝑣)) = ((*Q𝑣) ·Q 𝑣))
45 recidnq 7015 . . . . . . . . . . . . . . . . . . . . 21 (𝑣Q → (𝑣 ·Q (*Q𝑣)) = 1Q)
4644, 45eqtr3d 2123 . . . . . . . . . . . . . . . . . . . 20 (𝑣Q → ((*Q𝑣) ·Q 𝑣) = 1Q)
47 recidnq 7015 . . . . . . . . . . . . . . . . . . . 20 (𝑤Q → (𝑤 ·Q (*Q𝑤)) = 1Q)
4846, 47oveqan12d 5687 . . . . . . . . . . . . . . . . . . 19 ((𝑣Q𝑤Q) → (((*Q𝑣) ·Q 𝑣) ·Q (𝑤 ·Q (*Q𝑤))) = (1Q ·Q 1Q))
4948adantr 271 . . . . . . . . . . . . . . . . . 18 (((𝑣Q𝑤Q) ∧ (𝑣 <Q 𝑧 ∧ (𝑣 ·Q (*Q𝑤)) ∈ (2nd𝐴))) → (((*Q𝑣) ·Q 𝑣) ·Q (𝑤 ·Q (*Q𝑤))) = (1Q ·Q 1Q))
50 simpll 497 . . . . . . . . . . . . . . . . . . 19 (((𝑣Q𝑤Q) ∧ (𝑣 <Q 𝑧 ∧ (𝑣 ·Q (*Q𝑤)) ∈ (2nd𝐴))) → 𝑣Q)
51 mulassnqg 7006 . . . . . . . . . . . . . . . . . . . 20 ((𝑓Q𝑔QQ) → ((𝑓 ·Q 𝑔) ·Q ) = (𝑓 ·Q (𝑔 ·Q )))
5251adantl 272 . . . . . . . . . . . . . . . . . . 19 ((((𝑣Q𝑤Q) ∧ (𝑣 <Q 𝑧 ∧ (𝑣 ·Q (*Q𝑤)) ∈ (2nd𝐴))) ∧ (𝑓Q𝑔QQ)) → ((𝑓 ·Q 𝑔) ·Q ) = (𝑓 ·Q (𝑔 ·Q )))
53 recclnq 7014 . . . . . . . . . . . . . . . . . . . 20 (𝑤Q → (*Q𝑤) ∈ Q)
5435, 53syl 14 . . . . . . . . . . . . . . . . . . 19 (((𝑣Q𝑤Q) ∧ (𝑣 <Q 𝑧 ∧ (𝑣 ·Q (*Q𝑤)) ∈ (2nd𝐴))) → (*Q𝑤) ∈ Q)
55 mulclnq 6998 . . . . . . . . . . . . . . . . . . . 20 ((𝑓Q𝑔Q) → (𝑓 ·Q 𝑔) ∈ Q)
5655adantl 272 . . . . . . . . . . . . . . . . . . 19 ((((𝑣Q𝑤Q) ∧ (𝑣 <Q 𝑧 ∧ (𝑣 ·Q (*Q𝑤)) ∈ (2nd𝐴))) ∧ (𝑓Q𝑔Q)) → (𝑓 ·Q 𝑔) ∈ Q)
5734, 50, 35, 37, 52, 54, 56caov4d 5845 . . . . . . . . . . . . . . . . . 18 (((𝑣Q𝑤Q) ∧ (𝑣 <Q 𝑧 ∧ (𝑣 ·Q (*Q𝑤)) ∈ (2nd𝐴))) → (((*Q𝑣) ·Q 𝑣) ·Q (𝑤 ·Q (*Q𝑤))) = (((*Q𝑣) ·Q 𝑤) ·Q (𝑣 ·Q (*Q𝑤))))
5849, 57eqtr3d 2123 . . . . . . . . . . . . . . . . 17 (((𝑣Q𝑤Q) ∧ (𝑣 <Q 𝑧 ∧ (𝑣 ·Q (*Q𝑤)) ∈ (2nd𝐴))) → (1Q ·Q 1Q) = (((*Q𝑣) ·Q 𝑤) ·Q (𝑣 ·Q (*Q𝑤))))
5942, 58syl5reqr 2136 . . . . . . . . . . . . . . . 16 (((𝑣Q𝑤Q) ∧ (𝑣 <Q 𝑧 ∧ (𝑣 ·Q (*Q𝑤)) ∈ (2nd𝐴))) → (((*Q𝑣) ·Q 𝑤) ·Q (𝑣 ·Q (*Q𝑤))) = 1Q)
60 mulclnq 6998 . . . . . . . . . . . . . . . . . . 19 (((*Q𝑣) ∈ Q𝑤Q) → ((*Q𝑣) ·Q 𝑤) ∈ Q)
6133, 60sylan 278 . . . . . . . . . . . . . . . . . 18 ((𝑣Q𝑤Q) → ((*Q𝑣) ·Q 𝑤) ∈ Q)
62 mulclnq 6998 . . . . . . . . . . . . . . . . . . 19 ((𝑣Q ∧ (*Q𝑤) ∈ Q) → (𝑣 ·Q (*Q𝑤)) ∈ Q)
6353, 62sylan2 281 . . . . . . . . . . . . . . . . . 18 ((𝑣Q𝑤Q) → (𝑣 ·Q (*Q𝑤)) ∈ Q)
64 recmulnqg 7013 . . . . . . . . . . . . . . . . . 18 ((((*Q𝑣) ·Q 𝑤) ∈ Q ∧ (𝑣 ·Q (*Q𝑤)) ∈ Q) → ((*Q‘((*Q𝑣) ·Q 𝑤)) = (𝑣 ·Q (*Q𝑤)) ↔ (((*Q𝑣) ·Q 𝑤) ·Q (𝑣 ·Q (*Q𝑤))) = 1Q))
6561, 63, 64syl2anc 404 . . . . . . . . . . . . . . . . 17 ((𝑣Q𝑤Q) → ((*Q‘((*Q𝑣) ·Q 𝑤)) = (𝑣 ·Q (*Q𝑤)) ↔ (((*Q𝑣) ·Q 𝑤) ·Q (𝑣 ·Q (*Q𝑤))) = 1Q))
6665adantr 271 . . . . . . . . . . . . . . . 16 (((𝑣Q𝑤Q) ∧ (𝑣 <Q 𝑧 ∧ (𝑣 ·Q (*Q𝑤)) ∈ (2nd𝐴))) → ((*Q‘((*Q𝑣) ·Q 𝑤)) = (𝑣 ·Q (*Q𝑤)) ↔ (((*Q𝑣) ·Q 𝑤) ·Q (𝑣 ·Q (*Q𝑤))) = 1Q))
6759, 66mpbird 166 . . . . . . . . . . . . . . 15 (((𝑣Q𝑤Q) ∧ (𝑣 <Q 𝑧 ∧ (𝑣 ·Q (*Q𝑤)) ∈ (2nd𝐴))) → (*Q‘((*Q𝑣) ·Q 𝑤)) = (𝑣 ·Q (*Q𝑤)))
6867eleq1d 2157 . . . . . . . . . . . . . 14 (((𝑣Q𝑤Q) ∧ (𝑣 <Q 𝑧 ∧ (𝑣 ·Q (*Q𝑤)) ∈ (2nd𝐴))) → ((*Q‘((*Q𝑣) ·Q 𝑤)) ∈ (2nd𝐴) ↔ (𝑣 ·Q (*Q𝑤)) ∈ (2nd𝐴)))
6968biimprd 157 . . . . . . . . . . . . 13 (((𝑣Q𝑤Q) ∧ (𝑣 <Q 𝑧 ∧ (𝑣 ·Q (*Q𝑤)) ∈ (2nd𝐴))) → ((𝑣 ·Q (*Q𝑤)) ∈ (2nd𝐴) → (*Q‘((*Q𝑣) ·Q 𝑤)) ∈ (2nd𝐴)))
70 breq2 3857 . . . . . . . . . . . . . . . . . 18 (𝑦 = ((*Q𝑣) ·Q 𝑤) → (((*Q𝑧) ·Q 𝑤) <Q 𝑦 ↔ ((*Q𝑧) ·Q 𝑤) <Q ((*Q𝑣) ·Q 𝑤)))
71 fveq2 5320 . . . . . . . . . . . . . . . . . . 19 (𝑦 = ((*Q𝑣) ·Q 𝑤) → (*Q𝑦) = (*Q‘((*Q𝑣) ·Q 𝑤)))
7271eleq1d 2157 . . . . . . . . . . . . . . . . . 18 (𝑦 = ((*Q𝑣) ·Q 𝑤) → ((*Q𝑦) ∈ (2nd𝐴) ↔ (*Q‘((*Q𝑣) ·Q 𝑤)) ∈ (2nd𝐴)))
7370, 72anbi12d 458 . . . . . . . . . . . . . . . . 17 (𝑦 = ((*Q𝑣) ·Q 𝑤) → ((((*Q𝑧) ·Q 𝑤) <Q 𝑦 ∧ (*Q𝑦) ∈ (2nd𝐴)) ↔ (((*Q𝑧) ·Q 𝑤) <Q ((*Q𝑣) ·Q 𝑤) ∧ (*Q‘((*Q𝑣) ·Q 𝑤)) ∈ (2nd𝐴))))
7473spcegv 2710 . . . . . . . . . . . . . . . 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 7244 . . . . . . . . . . . . . . 15 (((*Q𝑧) ·Q 𝑤) ∈ (1st𝐵) ↔ ∃𝑦(((*Q𝑧) ·Q 𝑤) <Q 𝑦 ∧ (*Q𝑦) ∈ (2nd𝐴)))
7875, 77syl6ibr 161 . . . . . . . . . . . . . 14 ((𝑣Q𝑤Q) → ((((*Q𝑧) ·Q 𝑤) <Q ((*Q𝑣) ·Q 𝑤) ∧ (*Q‘((*Q𝑣) ·Q 𝑤)) ∈ (2nd𝐴)) → ((*Q𝑧) ·Q 𝑤) ∈ (1st𝐵)))
7978adantr 271 . . . . . . . . . . . . 13 (((𝑣Q𝑤Q) ∧ (𝑣 <Q 𝑧 ∧ (𝑣 ·Q (*Q𝑤)) ∈ (2nd𝐴))) → ((((*Q𝑧) ·Q 𝑤) <Q ((*Q𝑣) ·Q 𝑤) ∧ (*Q‘((*Q𝑣) ·Q 𝑤)) ∈ (2nd𝐴)) → ((*Q𝑧) ·Q 𝑤) ∈ (1st𝐵)))
8039, 69, 79syl2and 290 . . . . . . . . . . . 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 1176 . . . . . . . . . 10 (((𝐴P𝑤 <Q 1Q) ∧ (𝑣 ∈ (1st𝐴) ∧ (𝑣 ·Q (*Q𝑤)) ∈ (2nd𝐴)) ∧ 𝑣 <Q 𝑧) → ((*Q𝑧) ·Q 𝑤) ∈ (1st𝐵))
83303ad2ant3 967 . . . . . . . . . . 11 (((𝐴P𝑤 <Q 1Q) ∧ (𝑣 ∈ (1st𝐴) ∧ (𝑣 ·Q (*Q𝑤)) ∈ (2nd𝐴)) ∧ 𝑣 <Q 𝑧) → 𝑧Q)
84 mulidnq 7011 . . . . . . . . . . . . . 14 (𝑤Q → (𝑤 ·Q 1Q) = 𝑤)
85 mulcomnqg 7005 . . . . . . . . . . . . . . 15 ((𝑤Q ∧ 1QQ) → (𝑤 ·Q 1Q) = (1Q ·Q 𝑤))
8640, 85mpan2 417 . . . . . . . . . . . . . 14 (𝑤Q → (𝑤 ·Q 1Q) = (1Q ·Q 𝑤))
8784, 86eqtr3d 2123 . . . . . . . . . . . . 13 (𝑤Q𝑤 = (1Q ·Q 𝑤))
8887adantl 272 . . . . . . . . . . . 12 ((𝑧Q𝑤Q) → 𝑤 = (1Q ·Q 𝑤))
89 recidnq 7015 . . . . . . . . . . . . . 14 (𝑧Q → (𝑧 ·Q (*Q𝑧)) = 1Q)
9089oveq1d 5683 . . . . . . . . . . . . 13 (𝑧Q → ((𝑧 ·Q (*Q𝑧)) ·Q 𝑤) = (1Q ·Q 𝑤))
9190adantr 271 . . . . . . . . . . . 12 ((𝑧Q𝑤Q) → ((𝑧 ·Q (*Q𝑧)) ·Q 𝑤) = (1Q ·Q 𝑤))
92 mulassnqg 7006 . . . . . . . . . . . . . 14 ((𝑧Q ∧ (*Q𝑧) ∈ Q𝑤Q) → ((𝑧 ·Q (*Q𝑧)) ·Q 𝑤) = (𝑧 ·Q ((*Q𝑧) ·Q 𝑤)))
9331, 92syl3an2 1209 . . . . . . . . . . . . 13 ((𝑧Q𝑧Q𝑤Q) → ((𝑧 ·Q (*Q𝑧)) ·Q 𝑤) = (𝑧 ·Q ((*Q𝑧) ·Q 𝑤)))
94933anidm12 1232 . . . . . . . . . . . 12 ((𝑧Q𝑤Q) → ((𝑧 ·Q (*Q𝑧)) ·Q 𝑤) = (𝑧 ·Q ((*Q𝑧) ·Q 𝑤)))
9588, 91, 943eqtr2d 2127 . . . . . . . . . . 11 ((𝑧Q𝑤Q) → 𝑤 = (𝑧 ·Q ((*Q𝑧) ·Q 𝑤)))
9683, 21, 95syl2anc 404 . . . . . . . . . 10 (((𝐴P𝑤 <Q 1Q) ∧ (𝑣 ∈ (1st𝐴) ∧ (𝑣 ·Q (*Q𝑤)) ∈ (2nd𝐴)) ∧ 𝑣 <Q 𝑧) → 𝑤 = (𝑧 ·Q ((*Q𝑧) ·Q 𝑤)))
97 oveq2 5676 . . . . . . . . . . . 12 (𝑥 = ((*Q𝑧) ·Q 𝑤) → (𝑧 ·Q 𝑥) = (𝑧 ·Q ((*Q𝑧) ·Q 𝑤)))
9897eqeq2d 2100 . . . . . . . . . . 11 (𝑥 = ((*Q𝑧) ·Q 𝑤) → (𝑤 = (𝑧 ·Q 𝑥) ↔ 𝑤 = (𝑧 ·Q ((*Q𝑧) ·Q 𝑤))))
9998rspcev 2725 . . . . . . . . . 10 ((((*Q𝑧) ·Q 𝑤) ∈ (1st𝐵) ∧ 𝑤 = (𝑧 ·Q ((*Q𝑧) ·Q 𝑤))) → ∃𝑥 ∈ (1st𝐵)𝑤 = (𝑧 ·Q 𝑥))
10082, 96, 99syl2anc 404 . . . . . . . . 9 (((𝐴P𝑤 <Q 1Q) ∧ (𝑣 ∈ (1st𝐴) ∧ (𝑣 ·Q (*Q𝑤)) ∈ (2nd𝐴)) ∧ 𝑣 <Q 𝑧) → ∃𝑥 ∈ (1st𝐵)𝑤 = (𝑧 ·Q 𝑥))
1011003expia 1146 . . . . . . . 8 (((𝐴P𝑤 <Q 1Q) ∧ (𝑣 ∈ (1st𝐴) ∧ (𝑣 ·Q (*Q𝑤)) ∈ (2nd𝐴))) → (𝑣 <Q 𝑧 → ∃𝑥 ∈ (1st𝐵)𝑤 = (𝑧 ·Q 𝑥)))
102101reximdv 2475 . . . . . . 7 (((𝐴P𝑤 <Q 1Q) ∧ (𝑣 ∈ (1st𝐴) ∧ (𝑣 ·Q (*Q𝑤)) ∈ (2nd𝐴))) → (∃𝑧 ∈ (1st𝐴)𝑣 <Q 𝑧 → ∃𝑧 ∈ (1st𝐴)∃𝑥 ∈ (1st𝐵)𝑤 = (𝑧 ·Q 𝑥)))
10376recexprlempr 7254 . . . . . . . . 9 (𝐴P𝐵P)
104 df-imp 7091 . . . . . . . . . 10 ·P = (𝑦P, 𝑤P ↦ ⟨{𝑢Q ∣ ∃𝑓Q𝑔Q (𝑓 ∈ (1st𝑦) ∧ 𝑔 ∈ (1st𝑤) ∧ 𝑢 = (𝑓 ·Q 𝑔))}, {𝑢Q ∣ ∃𝑓Q𝑔Q (𝑓 ∈ (2nd𝑦) ∧ 𝑔 ∈ (2nd𝑤) ∧ 𝑢 = (𝑓 ·Q 𝑔))}⟩)
105104, 55genpelvl 7134 . . . . . . . . 9 ((𝐴P𝐵P) → (𝑤 ∈ (1st ‘(𝐴 ·P 𝐵)) ↔ ∃𝑧 ∈ (1st𝐴)∃𝑥 ∈ (1st𝐵)𝑤 = (𝑧 ·Q 𝑥)))
106103, 105mpdan 413 . . . . . . . 8 (𝐴P → (𝑤 ∈ (1st ‘(𝐴 ·P 𝐵)) ↔ ∃𝑧 ∈ (1st𝐴)∃𝑥 ∈ (1st𝐵)𝑤 = (𝑧 ·Q 𝑥)))
107106ad2antrr 473 . . . . . . 7 (((𝐴P𝑤 <Q 1Q) ∧ (𝑣 ∈ (1st𝐴) ∧ (𝑣 ·Q (*Q𝑤)) ∈ (2nd𝐴))) → (𝑤 ∈ (1st ‘(𝐴 ·P 𝐵)) ↔ ∃𝑧 ∈ (1st𝐴)∃𝑥 ∈ (1st𝐵)𝑤 = (𝑧 ·Q 𝑥)))
108102, 107sylibrd 168 . . . . . 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 2496 . . . 4 ((𝐴P𝑤 <Q 1Q) → 𝑤 ∈ (1st ‘(𝐴 ·P 𝐵)))
111110ex 114 . . 3 (𝐴P → (𝑤 <Q 1Q𝑤 ∈ (1st ‘(𝐴 ·P 𝐵))))
1122, 111syl5bi 151 . 2 (𝐴P → (𝑤 ∈ (1st ‘1P) → 𝑤 ∈ (1st ‘(𝐴 ·P 𝐵))))
113112ssrdv 3034 1 (𝐴P → (1st ‘1P) ⊆ (1st ‘(𝐴 ·P 𝐵)))
Colors of variables: wff set class
Syntax hints:  wi 4  wa 103  wb 104  w3a 925   = wceq 1290  wex 1427  wcel 1439  {cab 2075  wrex 2361  wss 3002  cop 3455   class class class wbr 3853  cfv 5030  (class class class)co 5668  1st c1st 5925  2nd c2nd 5926  Qcnq 6902  1Qc1q 6903   ·Q cmq 6905  *Qcrq 6906   <Q cltq 6907  Pcnp 6913  1Pc1p 6914   ·P cmp 6916
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-in1 580  ax-in2 581  ax-io 666  ax-5 1382  ax-7 1383  ax-gen 1384  ax-ie1 1428  ax-ie2 1429  ax-8 1441  ax-10 1442  ax-11 1443  ax-i12 1444  ax-bndl 1445  ax-4 1446  ax-13 1450  ax-14 1451  ax-17 1465  ax-i9 1469  ax-ial 1473  ax-i5r 1474  ax-ext 2071  ax-coll 3962  ax-sep 3965  ax-nul 3973  ax-pow 4017  ax-pr 4047  ax-un 4271  ax-setind 4368  ax-iinf 4418
This theorem depends on definitions:  df-bi 116  df-dc 782  df-3or 926  df-3an 927  df-tru 1293  df-fal 1296  df-nf 1396  df-sb 1694  df-eu 1952  df-mo 1953  df-clab 2076  df-cleq 2082  df-clel 2085  df-nfc 2218  df-ne 2257  df-ral 2365  df-rex 2366  df-reu 2367  df-rab 2369  df-v 2624  df-sbc 2844  df-csb 2937  df-dif 3004  df-un 3006  df-in 3008  df-ss 3015  df-nul 3290  df-pw 3437  df-sn 3458  df-pr 3459  df-op 3461  df-uni 3662  df-int 3697  df-iun 3740  df-br 3854  df-opab 3908  df-mpt 3909  df-tr 3945  df-eprel 4127  df-id 4131  df-po 4134  df-iso 4135  df-iord 4204  df-on 4206  df-suc 4209  df-iom 4421  df-xp 4460  df-rel 4461  df-cnv 4462  df-co 4463  df-dm 4464  df-rn 4465  df-res 4466  df-ima 4467  df-iota 4995  df-fun 5032  df-fn 5033  df-f 5034  df-f1 5035  df-fo 5036  df-f1o 5037  df-fv 5038  df-ov 5671  df-oprab 5672  df-mpt2 5673  df-1st 5927  df-2nd 5928  df-recs 6086  df-irdg 6151  df-1o 6197  df-2o 6198  df-oadd 6201  df-omul 6202  df-er 6308  df-ec 6310  df-qs 6314  df-ni 6926  df-pli 6927  df-mi 6928  df-lti 6929  df-plpq 6966  df-mpq 6967  df-enq 6969  df-nqqs 6970  df-plqqs 6971  df-mqqs 6972  df-1nqqs 6973  df-rq 6974  df-ltnqqs 6975  df-enq0 7046  df-nq0 7047  df-0nq0 7048  df-plq0 7049  df-mq0 7050  df-inp 7088  df-i1p 7089  df-imp 7091
This theorem is referenced by:  recexprlemex  7259
  Copyright terms: Public domain W3C validator