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

Theorem recexprlem1ssl 7448
 Description: The lower cut of one is a subset of the lower cut of 𝐴 ·P 𝐵. Lemma for recexpr 7453. (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 7370 . . . 4 (1st ‘1P) = {𝑤𝑤 <Q 1Q}
21abeq2i 2250 . . 3 (𝑤 ∈ (1st ‘1P) ↔ 𝑤 <Q 1Q)
3 rec1nq 7210 . . . . . . 7 (*Q‘1Q) = 1Q
4 ltrnqi 7236 . . . . . . 7 (𝑤 <Q 1Q → (*Q‘1Q) <Q (*Q𝑤))
53, 4eqbrtrrid 3964 . . . . . 6 (𝑤 <Q 1Q → 1Q <Q (*Q𝑤))
6 prop 7290 . . . . . . 7 (𝐴P → ⟨(1st𝐴), (2nd𝐴)⟩ ∈ P)
7 prmuloc2 7382 . . . . . . 7 ((⟨(1st𝐴), (2nd𝐴)⟩ ∈ P ∧ 1Q <Q (*Q𝑤)) → ∃𝑣 ∈ (1st𝐴)(𝑣 ·Q (*Q𝑤)) ∈ (2nd𝐴))
86, 7sylan 281 . . . . . 6 ((𝐴P ∧ 1Q <Q (*Q𝑤)) → ∃𝑣 ∈ (1st𝐴)(𝑣 ·Q (*Q𝑤)) ∈ (2nd𝐴))
95, 8sylan2 284 . . . . 5 ((𝐴P𝑤 <Q 1Q) → ∃𝑣 ∈ (1st𝐴)(𝑣 ·Q (*Q𝑤)) ∈ (2nd𝐴))
10 prnmaxl 7303 . . . . . . . 8 ((⟨(1st𝐴), (2nd𝐴)⟩ ∈ P𝑣 ∈ (1st𝐴)) → ∃𝑧 ∈ (1st𝐴)𝑣 <Q 𝑧)
116, 10sylan 281 . . . . . . 7 ((𝐴P𝑣 ∈ (1st𝐴)) → ∃𝑧 ∈ (1st𝐴)𝑣 <Q 𝑧)
1211ad2ant2r 500 . . . . . 6 (((𝐴P𝑤 <Q 1Q) ∧ (𝑣 ∈ (1st𝐴) ∧ (𝑣 ·Q (*Q𝑤)) ∈ (2nd𝐴))) → ∃𝑧 ∈ (1st𝐴)𝑣 <Q 𝑧)
13 elprnql 7296 . . . . . . . . . . . . . 14 ((⟨(1st𝐴), (2nd𝐴)⟩ ∈ P𝑣 ∈ (1st𝐴)) → 𝑣Q)
146, 13sylan 281 . . . . . . . . . . . . 13 ((𝐴P𝑣 ∈ (1st𝐴)) → 𝑣Q)
1514ad2ant2r 500 . . . . . . . . . . . 12 (((𝐴P𝑤 <Q 1Q) ∧ (𝑣 ∈ (1st𝐴) ∧ (𝑣 ·Q (*Q𝑤)) ∈ (2nd𝐴))) → 𝑣Q)
16153adant3 1001 . . . . . . . . . . 11 (((𝐴P𝑤 <Q 1Q) ∧ (𝑣 ∈ (1st𝐴) ∧ (𝑣 ·Q (*Q𝑤)) ∈ (2nd𝐴)) ∧ 𝑣 <Q 𝑧) → 𝑣Q)
17 simp1r 1006 . . . . . . . . . . . 12 (((𝐴P𝑤 <Q 1Q) ∧ (𝑣 ∈ (1st𝐴) ∧ (𝑣 ·Q (*Q𝑤)) ∈ (2nd𝐴)) ∧ 𝑣 <Q 𝑧) → 𝑤 <Q 1Q)
18 ltrelnq 7180 . . . . . . . . . . . . . 14 <Q ⊆ (Q × Q)
1918brel 4591 . . . . . . . . . . . . 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 983 . . . . . . . . . . 11 (((𝐴P𝑤 <Q 1Q) ∧ (𝑣 ∈ (1st𝐴) ∧ (𝑣 ·Q (*Q𝑤)) ∈ (2nd𝐴)) ∧ 𝑣 <Q 𝑧) → 𝑣 <Q 𝑧)
23 simp2r 1008 . . . . . . . . . . 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 7236 . . . . . . . . . . . . . 14 (𝑣 <Q 𝑧 → (*Q𝑧) <Q (*Q𝑣))
26 ltmnqg 7216 . . . . . . . . . . . . . . . 16 ((𝑓Q𝑔QQ) → (𝑓 <Q 𝑔 ↔ ( ·Q 𝑓) <Q ( ·Q 𝑔)))
2726adantl 275 . . . . . . . . . . . . . . 15 ((((𝑣Q𝑤Q) ∧ (𝑣 <Q 𝑧 ∧ (𝑣 ·Q (*Q𝑤)) ∈ (2nd𝐴))) ∧ (𝑓Q𝑔QQ)) → (𝑓 <Q 𝑔 ↔ ( ·Q 𝑓) <Q ( ·Q 𝑔)))
28 simprl 520 . . . . . . . . . . . . . . . 16 (((𝑣Q𝑤Q) ∧ (𝑣 <Q 𝑧 ∧ (𝑣 ·Q (*Q𝑤)) ∈ (2nd𝐴))) → 𝑣 <Q 𝑧)
2918brel 4591 . . . . . . . . . . . . . . . . 17 (𝑣 <Q 𝑧 → (𝑣Q𝑧Q))
3029simprd 113 . . . . . . . . . . . . . . . 16 (𝑣 <Q 𝑧𝑧Q)
31 recclnq 7207 . . . . . . . . . . . . . . . 16 (𝑧Q → (*Q𝑧) ∈ Q)
3228, 30, 313syl 17 . . . . . . . . . . . . . . 15 (((𝑣Q𝑤Q) ∧ (𝑣 <Q 𝑧 ∧ (𝑣 ·Q (*Q𝑤)) ∈ (2nd𝐴))) → (*Q𝑧) ∈ Q)
33 recclnq 7207 . . . . . . . . . . . . . . . 16 (𝑣Q → (*Q𝑣) ∈ Q)
3433ad2antrr 479 . . . . . . . . . . . . . . 15 (((𝑣Q𝑤Q) ∧ (𝑣 <Q 𝑧 ∧ (𝑣 ·Q (*Q𝑤)) ∈ (2nd𝐴))) → (*Q𝑣) ∈ Q)
35 simplr 519 . . . . . . . . . . . . . . 15 (((𝑣Q𝑤Q) ∧ (𝑣 <Q 𝑧 ∧ (𝑣 ·Q (*Q𝑤)) ∈ (2nd𝐴))) → 𝑤Q)
36 mulcomnqg 7198 . . . . . . . . . . . . . . . 16 ((𝑓Q𝑔Q) → (𝑓 ·Q 𝑔) = (𝑔 ·Q 𝑓))
3736adantl 275 . . . . . . . . . . . . . . 15 ((((𝑣Q𝑤Q) ∧ (𝑣 <Q 𝑧 ∧ (𝑣 ·Q (*Q𝑤)) ∈ (2nd𝐴))) ∧ (𝑓Q𝑔Q)) → (𝑓 ·Q 𝑔) = (𝑔 ·Q 𝑓))
3827, 32, 34, 35, 37caovord2d 5940 . . . . . . . . . . . . . 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 7181 . . . . . . . . . . . . . . . . . 18 1QQ
41 mulidnq 7204 . . . . . . . . . . . . . . . . . 18 (1QQ → (1Q ·Q 1Q) = 1Q)
4240, 41ax-mp 5 . . . . . . . . . . . . . . . . 17 (1Q ·Q 1Q) = 1Q
43 mulcomnqg 7198 . . . . . . . . . . . . . . . . . . . . . 22 ((𝑣Q ∧ (*Q𝑣) ∈ Q) → (𝑣 ·Q (*Q𝑣)) = ((*Q𝑣) ·Q 𝑣))
4433, 43mpdan 417 . . . . . . . . . . . . . . . . . . . . 21 (𝑣Q → (𝑣 ·Q (*Q𝑣)) = ((*Q𝑣) ·Q 𝑣))
45 recidnq 7208 . . . . . . . . . . . . . . . . . . . . 21 (𝑣Q → (𝑣 ·Q (*Q𝑣)) = 1Q)
4644, 45eqtr3d 2174 . . . . . . . . . . . . . . . . . . . 20 (𝑣Q → ((*Q𝑣) ·Q 𝑣) = 1Q)
47 recidnq 7208 . . . . . . . . . . . . . . . . . . . 20 (𝑤Q → (𝑤 ·Q (*Q𝑤)) = 1Q)
4846, 47oveqan12d 5793 . . . . . . . . . . . . . . . . . . 19 ((𝑣Q𝑤Q) → (((*Q𝑣) ·Q 𝑣) ·Q (𝑤 ·Q (*Q𝑤))) = (1Q ·Q 1Q))
4948adantr 274 . . . . . . . . . . . . . . . . . 18 (((𝑣Q𝑤Q) ∧ (𝑣 <Q 𝑧 ∧ (𝑣 ·Q (*Q𝑤)) ∈ (2nd𝐴))) → (((*Q𝑣) ·Q 𝑣) ·Q (𝑤 ·Q (*Q𝑤))) = (1Q ·Q 1Q))
50 simpll 518 . . . . . . . . . . . . . . . . . . 19 (((𝑣Q𝑤Q) ∧ (𝑣 <Q 𝑧 ∧ (𝑣 ·Q (*Q𝑤)) ∈ (2nd𝐴))) → 𝑣Q)
51 mulassnqg 7199 . . . . . . . . . . . . . . . . . . . 20 ((𝑓Q𝑔QQ) → ((𝑓 ·Q 𝑔) ·Q ) = (𝑓 ·Q (𝑔 ·Q )))
5251adantl 275 . . . . . . . . . . . . . . . . . . 19 ((((𝑣Q𝑤Q) ∧ (𝑣 <Q 𝑧 ∧ (𝑣 ·Q (*Q𝑤)) ∈ (2nd𝐴))) ∧ (𝑓Q𝑔QQ)) → ((𝑓 ·Q 𝑔) ·Q ) = (𝑓 ·Q (𝑔 ·Q )))
53 recclnq 7207 . . . . . . . . . . . . . . . . . . . 20 (𝑤Q → (*Q𝑤) ∈ Q)
5435, 53syl 14 . . . . . . . . . . . . . . . . . . 19 (((𝑣Q𝑤Q) ∧ (𝑣 <Q 𝑧 ∧ (𝑣 ·Q (*Q𝑤)) ∈ (2nd𝐴))) → (*Q𝑤) ∈ Q)
55 mulclnq 7191 . . . . . . . . . . . . . . . . . . . 20 ((𝑓Q𝑔Q) → (𝑓 ·Q 𝑔) ∈ Q)
5655adantl 275 . . . . . . . . . . . . . . . . . . 19 ((((𝑣Q𝑤Q) ∧ (𝑣 <Q 𝑧 ∧ (𝑣 ·Q (*Q𝑤)) ∈ (2nd𝐴))) ∧ (𝑓Q𝑔Q)) → (𝑓 ·Q 𝑔) ∈ Q)
5734, 50, 35, 37, 52, 54, 56caov4d 5955 . . . . . . . . . . . . . . . . . 18 (((𝑣Q𝑤Q) ∧ (𝑣 <Q 𝑧 ∧ (𝑣 ·Q (*Q𝑤)) ∈ (2nd𝐴))) → (((*Q𝑣) ·Q 𝑣) ·Q (𝑤 ·Q (*Q𝑤))) = (((*Q𝑣) ·Q 𝑤) ·Q (𝑣 ·Q (*Q𝑤))))
5849, 57eqtr3d 2174 . . . . . . . . . . . . . . . . 17 (((𝑣Q𝑤Q) ∧ (𝑣 <Q 𝑧 ∧ (𝑣 ·Q (*Q𝑤)) ∈ (2nd𝐴))) → (1Q ·Q 1Q) = (((*Q𝑣) ·Q 𝑤) ·Q (𝑣 ·Q (*Q𝑤))))
5942, 58syl5reqr 2187 . . . . . . . . . . . . . . . 16 (((𝑣Q𝑤Q) ∧ (𝑣 <Q 𝑧 ∧ (𝑣 ·Q (*Q𝑤)) ∈ (2nd𝐴))) → (((*Q𝑣) ·Q 𝑤) ·Q (𝑣 ·Q (*Q𝑤))) = 1Q)
60 mulclnq 7191 . . . . . . . . . . . . . . . . . . 19 (((*Q𝑣) ∈ Q𝑤Q) → ((*Q𝑣) ·Q 𝑤) ∈ Q)
6133, 60sylan 281 . . . . . . . . . . . . . . . . . 18 ((𝑣Q𝑤Q) → ((*Q𝑣) ·Q 𝑤) ∈ Q)
62 mulclnq 7191 . . . . . . . . . . . . . . . . . . 19 ((𝑣Q ∧ (*Q𝑤) ∈ Q) → (𝑣 ·Q (*Q𝑤)) ∈ Q)
6353, 62sylan2 284 . . . . . . . . . . . . . . . . . 18 ((𝑣Q𝑤Q) → (𝑣 ·Q (*Q𝑤)) ∈ Q)
64 recmulnqg 7206 . . . . . . . . . . . . . . . . . 18 ((((*Q𝑣) ·Q 𝑤) ∈ Q ∧ (𝑣 ·Q (*Q𝑤)) ∈ Q) → ((*Q‘((*Q𝑣) ·Q 𝑤)) = (𝑣 ·Q (*Q𝑤)) ↔ (((*Q𝑣) ·Q 𝑤) ·Q (𝑣 ·Q (*Q𝑤))) = 1Q))
6561, 63, 64syl2anc 408 . . . . . . . . . . . . . . . . 17 ((𝑣Q𝑤Q) → ((*Q‘((*Q𝑣) ·Q 𝑤)) = (𝑣 ·Q (*Q𝑤)) ↔ (((*Q𝑣) ·Q 𝑤) ·Q (𝑣 ·Q (*Q𝑤))) = 1Q))
6665adantr 274 . . . . . . . . . . . . . . . 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 2208 . . . . . . . . . . . . . 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 3933 . . . . . . . . . . . . . . . . . 18 (𝑦 = ((*Q𝑣) ·Q 𝑤) → (((*Q𝑧) ·Q 𝑤) <Q 𝑦 ↔ ((*Q𝑧) ·Q 𝑤) <Q ((*Q𝑣) ·Q 𝑤)))
71 fveq2 5421 . . . . . . . . . . . . . . . . . . 19 (𝑦 = ((*Q𝑣) ·Q 𝑤) → (*Q𝑦) = (*Q‘((*Q𝑣) ·Q 𝑤)))
7271eleq1d 2208 . . . . . . . . . . . . . . . . . 18 (𝑦 = ((*Q𝑣) ·Q 𝑤) → ((*Q𝑦) ∈ (2nd𝐴) ↔ (*Q‘((*Q𝑣) ·Q 𝑤)) ∈ (2nd𝐴)))
7370, 72anbi12d 464 . . . . . . . . . . . . . . . . 17 (𝑦 = ((*Q𝑣) ·Q 𝑤) → ((((*Q𝑧) ·Q 𝑤) <Q 𝑦 ∧ (*Q𝑦) ∈ (2nd𝐴)) ↔ (((*Q𝑧) ·Q 𝑤) <Q ((*Q𝑣) ·Q 𝑤) ∧ (*Q‘((*Q𝑣) ·Q 𝑤)) ∈ (2nd𝐴))))
7473spcegv 2774 . . . . . . . . . . . . . . . 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 7437 . . . . . . . . . . . . . . 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 274 . . . . . . . . . . . . 13 (((𝑣Q𝑤Q) ∧ (𝑣 <Q 𝑧 ∧ (𝑣 ·Q (*Q𝑤)) ∈ (2nd𝐴))) → ((((*Q𝑧) ·Q 𝑤) <Q ((*Q𝑣) ·Q 𝑤) ∧ (*Q‘((*Q𝑣) ·Q 𝑤)) ∈ (2nd𝐴)) → ((*Q𝑧) ·Q 𝑤) ∈ (1st𝐵)))
8039, 69, 79syl2and 293 . . . . . . . . . . . 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 1217 . . . . . . . . . 10 (((𝐴P𝑤 <Q 1Q) ∧ (𝑣 ∈ (1st𝐴) ∧ (𝑣 ·Q (*Q𝑤)) ∈ (2nd𝐴)) ∧ 𝑣 <Q 𝑧) → ((*Q𝑧) ·Q 𝑤) ∈ (1st𝐵))
83303ad2ant3 1004 . . . . . . . . . . 11 (((𝐴P𝑤 <Q 1Q) ∧ (𝑣 ∈ (1st𝐴) ∧ (𝑣 ·Q (*Q𝑤)) ∈ (2nd𝐴)) ∧ 𝑣 <Q 𝑧) → 𝑧Q)
84 mulidnq 7204 . . . . . . . . . . . . . 14 (𝑤Q → (𝑤 ·Q 1Q) = 𝑤)
85 mulcomnqg 7198 . . . . . . . . . . . . . . 15 ((𝑤Q ∧ 1QQ) → (𝑤 ·Q 1Q) = (1Q ·Q 𝑤))
8640, 85mpan2 421 . . . . . . . . . . . . . 14 (𝑤Q → (𝑤 ·Q 1Q) = (1Q ·Q 𝑤))
8784, 86eqtr3d 2174 . . . . . . . . . . . . 13 (𝑤Q𝑤 = (1Q ·Q 𝑤))
8887adantl 275 . . . . . . . . . . . 12 ((𝑧Q𝑤Q) → 𝑤 = (1Q ·Q 𝑤))
89 recidnq 7208 . . . . . . . . . . . . . 14 (𝑧Q → (𝑧 ·Q (*Q𝑧)) = 1Q)
9089oveq1d 5789 . . . . . . . . . . . . 13 (𝑧Q → ((𝑧 ·Q (*Q𝑧)) ·Q 𝑤) = (1Q ·Q 𝑤))
9190adantr 274 . . . . . . . . . . . 12 ((𝑧Q𝑤Q) → ((𝑧 ·Q (*Q𝑧)) ·Q 𝑤) = (1Q ·Q 𝑤))
92 mulassnqg 7199 . . . . . . . . . . . . . 14 ((𝑧Q ∧ (*Q𝑧) ∈ Q𝑤Q) → ((𝑧 ·Q (*Q𝑧)) ·Q 𝑤) = (𝑧 ·Q ((*Q𝑧) ·Q 𝑤)))
9331, 92syl3an2 1250 . . . . . . . . . . . . 13 ((𝑧Q𝑧Q𝑤Q) → ((𝑧 ·Q (*Q𝑧)) ·Q 𝑤) = (𝑧 ·Q ((*Q𝑧) ·Q 𝑤)))
94933anidm12 1273 . . . . . . . . . . . 12 ((𝑧Q𝑤Q) → ((𝑧 ·Q (*Q𝑧)) ·Q 𝑤) = (𝑧 ·Q ((*Q𝑧) ·Q 𝑤)))
9588, 91, 943eqtr2d 2178 . . . . . . . . . . 11 ((𝑧Q𝑤Q) → 𝑤 = (𝑧 ·Q ((*Q𝑧) ·Q 𝑤)))
9683, 21, 95syl2anc 408 . . . . . . . . . 10 (((𝐴P𝑤 <Q 1Q) ∧ (𝑣 ∈ (1st𝐴) ∧ (𝑣 ·Q (*Q𝑤)) ∈ (2nd𝐴)) ∧ 𝑣 <Q 𝑧) → 𝑤 = (𝑧 ·Q ((*Q𝑧) ·Q 𝑤)))
97 oveq2 5782 . . . . . . . . . . . 12 (𝑥 = ((*Q𝑧) ·Q 𝑤) → (𝑧 ·Q 𝑥) = (𝑧 ·Q ((*Q𝑧) ·Q 𝑤)))
9897eqeq2d 2151 . . . . . . . . . . 11 (𝑥 = ((*Q𝑧) ·Q 𝑤) → (𝑤 = (𝑧 ·Q 𝑥) ↔ 𝑤 = (𝑧 ·Q ((*Q𝑧) ·Q 𝑤))))
9998rspcev 2789 . . . . . . . . . 10 ((((*Q𝑧) ·Q 𝑤) ∈ (1st𝐵) ∧ 𝑤 = (𝑧 ·Q ((*Q𝑧) ·Q 𝑤))) → ∃𝑥 ∈ (1st𝐵)𝑤 = (𝑧 ·Q 𝑥))
10082, 96, 99syl2anc 408 . . . . . . . . 9 (((𝐴P𝑤 <Q 1Q) ∧ (𝑣 ∈ (1st𝐴) ∧ (𝑣 ·Q (*Q𝑤)) ∈ (2nd𝐴)) ∧ 𝑣 <Q 𝑧) → ∃𝑥 ∈ (1st𝐵)𝑤 = (𝑧 ·Q 𝑥))
1011003expia 1183 . . . . . . . 8 (((𝐴P𝑤 <Q 1Q) ∧ (𝑣 ∈ (1st𝐴) ∧ (𝑣 ·Q (*Q𝑤)) ∈ (2nd𝐴))) → (𝑣 <Q 𝑧 → ∃𝑥 ∈ (1st𝐵)𝑤 = (𝑧 ·Q 𝑥)))
102101reximdv 2533 . . . . . . 7 (((𝐴P𝑤 <Q 1Q) ∧ (𝑣 ∈ (1st𝐴) ∧ (𝑣 ·Q (*Q𝑤)) ∈ (2nd𝐴))) → (∃𝑧 ∈ (1st𝐴)𝑣 <Q 𝑧 → ∃𝑧 ∈ (1st𝐴)∃𝑥 ∈ (1st𝐵)𝑤 = (𝑧 ·Q 𝑥)))
10376recexprlempr 7447 . . . . . . . . 9 (𝐴P𝐵P)
104 df-imp 7284 . . . . . . . . . 10 ·P = (𝑦P, 𝑤P ↦ ⟨{𝑢Q ∣ ∃𝑓Q𝑔Q (𝑓 ∈ (1st𝑦) ∧ 𝑔 ∈ (1st𝑤) ∧ 𝑢 = (𝑓 ·Q 𝑔))}, {𝑢Q ∣ ∃𝑓Q𝑔Q (𝑓 ∈ (2nd𝑦) ∧ 𝑔 ∈ (2nd𝑤) ∧ 𝑢 = (𝑓 ·Q 𝑔))}⟩)
105104, 55genpelvl 7327 . . . . . . . . 9 ((𝐴P𝐵P) → (𝑤 ∈ (1st ‘(𝐴 ·P 𝐵)) ↔ ∃𝑧 ∈ (1st𝐴)∃𝑥 ∈ (1st𝐵)𝑤 = (𝑧 ·Q 𝑥)))
106103, 105mpdan 417 . . . . . . . 8 (𝐴P → (𝑤 ∈ (1st ‘(𝐴 ·P 𝐵)) ↔ ∃𝑧 ∈ (1st𝐴)∃𝑥 ∈ (1st𝐵)𝑤 = (𝑧 ·Q 𝑥)))
107106ad2antrr 479 . . . . . . 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 2554 . . . 4 ((𝐴P𝑤 <Q 1Q) → 𝑤 ∈ (1st ‘(𝐴 ·P 𝐵)))
111110ex 114 . . 3 (𝐴P → (𝑤 <Q 1Q𝑤 ∈ (1st ‘(𝐴 ·P 𝐵))))
1122, 111syl5bi 151 . 2 (𝐴P → (𝑤 ∈ (1st ‘1P) → 𝑤 ∈ (1st ‘(𝐴 ·P 𝐵))))
113112ssrdv 3103 1 (𝐴P → (1st ‘1P) ⊆ (1st ‘(𝐴 ·P 𝐵)))
 Colors of variables: wff set class Syntax hints:   → wi 4   ∧ wa 103   ↔ wb 104   ∧ w3a 962   = wceq 1331  ∃wex 1468   ∈ wcel 1480  {cab 2125  ∃wrex 2417   ⊆ wss 3071  ⟨cop 3530   class class class wbr 3929  ‘cfv 5123  (class class class)co 5774  1st c1st 6036  2nd c2nd 6037  Qcnq 7095  1Qc1q 7096   ·Q cmq 7098  *Qcrq 7099
 Copyright terms: Public domain W3C validator