Theorem unxpwdom3 43540

Description: Weaker version of unxpwdom 9494 where a function is required only to be cancellative, not an injection. 𝐷 and 𝐵 are to be thought of as "large" "horizonal" sets, the others as "small". Because the operator is row-wise injective, but the whole row cannot inject into 𝐴, each row must hit an element of 𝐵; by column injectivity, each row can be identified in at least one way by the 𝐵 element that it hits and the column in which it is hit. (Contributed by Stefan O'Rear, 8-Jul-2015.) MOVABLE

Hypotheses

Ref	Expression
unxpwdom3.av	⊢ (𝜑 → 𝐴 ∈ 𝑉)
unxpwdom3.bv	⊢ (𝜑 → 𝐵 ∈ 𝑊)
unxpwdom3.dv	⊢ (𝜑 → 𝐷 ∈ 𝑋)
unxpwdom3.ov	⊢ ((𝜑 ∧ 𝑎 ∈ 𝐶 ∧ 𝑏 ∈ 𝐷) → (𝑎 + 𝑏) ∈ (𝐴 ∪ 𝐵))
unxpwdom3.lc	⊢ (((𝜑 ∧ 𝑎 ∈ 𝐶) ∧ (𝑏 ∈ 𝐷 ∧ 𝑐 ∈ 𝐷)) → ((𝑎 + 𝑏) = (𝑎 + 𝑐) ↔ 𝑏 = 𝑐))
unxpwdom3.rc	⊢ (((𝜑 ∧ 𝑑 ∈ 𝐷) ∧ (𝑎 ∈ 𝐶 ∧ 𝑐 ∈ 𝐶)) → ((𝑐 + 𝑑) = (𝑎 + 𝑑) ↔ 𝑐 = 𝑎))
unxpwdom3.ni	⊢ (𝜑 → ¬ 𝐷 ≼ 𝐴)

Assertion

Ref	Expression
unxpwdom3	⊢ (𝜑 → 𝐶 ≼* (𝐷 × 𝐵))

Distinct variable groups:   𝑎,𝑏,𝑐,𝑑,𝐵   𝐶,𝑎,𝑏,𝑐,𝑑   𝐷,𝑎,𝑏,𝑐,𝑑   + ,𝑎,𝑏,𝑐,𝑑   𝜑,𝑎,𝑏,𝑐,𝑑   𝐴,𝑏,𝑐

Allowed substitution hints:   𝐴(𝑎,𝑑)   𝑉(𝑎,𝑏,𝑐,𝑑)   𝑊(𝑎,𝑏,𝑐,𝑑)   𝑋(𝑎,𝑏,𝑐,𝑑)

Proof of Theorem unxpwdom3

Dummy variables 𝑥 𝑦 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		unxpwdom3.dv	. . 3 ⊢ (𝜑 → 𝐷 ∈ 𝑋)
2		unxpwdom3.bv	. . 3 ⊢ (𝜑 → 𝐵 ∈ 𝑊)
3	1, 2	xpexd 7694	. 2 ⊢ (𝜑 → (𝐷 × 𝐵) ∈ V)
4		simprr 778	. . . . 5 ⊢ (((𝜑 ∧ 𝑎 ∈ 𝐶) ∧ (𝑑 ∈ 𝐷 ∧ (𝑎 + 𝑑) ∈ 𝐵)) → (𝑎 + 𝑑) ∈ 𝐵)
5		simplr 774	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑎 ∈ 𝐶) ∧ (𝑑 ∈ 𝐷 ∧ (𝑎 + 𝑑) ∈ 𝐵)) → 𝑎 ∈ 𝐶)
6		unxpwdom3.rc	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑑 ∈ 𝐷) ∧ (𝑎 ∈ 𝐶 ∧ 𝑐 ∈ 𝐶)) → ((𝑐 + 𝑑) = (𝑎 + 𝑑) ↔ 𝑐 = 𝑎))
7	6	an4s 666	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑎 ∈ 𝐶) ∧ (𝑑 ∈ 𝐷 ∧ 𝑐 ∈ 𝐶)) → ((𝑐 + 𝑑) = (𝑎 + 𝑑) ↔ 𝑐 = 𝑎))
8	7	anassrs 468	. . . . . . . 8 ⊢ ((((𝜑 ∧ 𝑎 ∈ 𝐶) ∧ 𝑑 ∈ 𝐷) ∧ 𝑐 ∈ 𝐶) → ((𝑐 + 𝑑) = (𝑎 + 𝑑) ↔ 𝑐 = 𝑎))
9	8	adantlrr 727	. . . . . . 7 ⊢ ((((𝜑 ∧ 𝑎 ∈ 𝐶) ∧ (𝑑 ∈ 𝐷 ∧ (𝑎 + 𝑑) ∈ 𝐵)) ∧ 𝑐 ∈ 𝐶) → ((𝑐 + 𝑑) = (𝑎 + 𝑑) ↔ 𝑐 = 𝑎))
10	5, 9	riota5 7342	. . . . . 6 ⊢ (((𝜑 ∧ 𝑎 ∈ 𝐶) ∧ (𝑑 ∈ 𝐷 ∧ (𝑎 + 𝑑) ∈ 𝐵)) → (℩𝑐 ∈ 𝐶 (𝑐 + 𝑑) = (𝑎 + 𝑑)) = 𝑎)
11	10	eqcomd 2745	. . . . 5 ⊢ (((𝜑 ∧ 𝑎 ∈ 𝐶) ∧ (𝑑 ∈ 𝐷 ∧ (𝑎 + 𝑑) ∈ 𝐵)) → 𝑎 = (℩𝑐 ∈ 𝐶 (𝑐 + 𝑑) = (𝑎 + 𝑑)))
12		eqeq2 2751	. . . . . . 7 ⊢ (𝑦 = (𝑎 + 𝑑) → ((𝑐 + 𝑑) = 𝑦 ↔ (𝑐 + 𝑑) = (𝑎 + 𝑑)))
13	12	riotabidv 7315	. . . . . 6 ⊢ (𝑦 = (𝑎 + 𝑑) → (℩𝑐 ∈ 𝐶 (𝑐 + 𝑑) = 𝑦) = (℩𝑐 ∈ 𝐶 (𝑐 + 𝑑) = (𝑎 + 𝑑)))
14	13	rspceeqv 3583	. . . . 5 ⊢ (((𝑎 + 𝑑) ∈ 𝐵 ∧ 𝑎 = (℩𝑐 ∈ 𝐶 (𝑐 + 𝑑) = (𝑎 + 𝑑))) → ∃𝑦 ∈ 𝐵 𝑎 = (℩𝑐 ∈ 𝐶 (𝑐 + 𝑑) = 𝑦))
15	4, 11, 14	syl2anc 590	. . . 4 ⊢ (((𝜑 ∧ 𝑎 ∈ 𝐶) ∧ (𝑑 ∈ 𝐷 ∧ (𝑎 + 𝑑) ∈ 𝐵)) → ∃𝑦 ∈ 𝐵 𝑎 = (℩𝑐 ∈ 𝐶 (𝑐 + 𝑑) = 𝑦))
16		unxpwdom3.ni	. . . . . . 7 ⊢ (𝜑 → ¬ 𝐷 ≼ 𝐴)
17	16	adantr 481	. . . . . 6 ⊢ ((𝜑 ∧ 𝑎 ∈ 𝐶) → ¬ 𝐷 ≼ 𝐴)
18		unxpwdom3.av	. . . . . . . 8 ⊢ (𝜑 → 𝐴 ∈ 𝑉)
19	18	ad2antrr 732	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑎 ∈ 𝐶) ∧ ∀𝑑 ∈ 𝐷 ¬ (𝑎 + 𝑑) ∈ 𝐵) → 𝐴 ∈ 𝑉)
20		oveq2 7364	. . . . . . . . . . . . . 14 ⊢ (𝑑 = 𝑏 → (𝑎 + 𝑑) = (𝑎 + 𝑏))
21	20	eleq1d 2824	. . . . . . . . . . . . 13 ⊢ (𝑑 = 𝑏 → ((𝑎 + 𝑑) ∈ 𝐵 ↔ (𝑎 + 𝑏) ∈ 𝐵))
22	21	notbid 319	. . . . . . . . . . . 12 ⊢ (𝑑 = 𝑏 → (¬ (𝑎 + 𝑑) ∈ 𝐵 ↔ ¬ (𝑎 + 𝑏) ∈ 𝐵))
23	22	rspcv 3556	. . . . . . . . . . 11 ⊢ (𝑏 ∈ 𝐷 → (∀𝑑 ∈ 𝐷 ¬ (𝑎 + 𝑑) ∈ 𝐵 → ¬ (𝑎 + 𝑏) ∈ 𝐵))
24	23	adantl 482	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑎 ∈ 𝐶) ∧ 𝑏 ∈ 𝐷) → (∀𝑑 ∈ 𝐷 ¬ (𝑎 + 𝑑) ∈ 𝐵 → ¬ (𝑎 + 𝑏) ∈ 𝐵))
25		unxpwdom3.ov	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑎 ∈ 𝐶 ∧ 𝑏 ∈ 𝐷) → (𝑎 + 𝑏) ∈ (𝐴 ∪ 𝐵))
26	25	3expa 1124	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑎 ∈ 𝐶) ∧ 𝑏 ∈ 𝐷) → (𝑎 + 𝑏) ∈ (𝐴 ∪ 𝐵))
27		elun 4083	. . . . . . . . . . . . 13 ⊢ ((𝑎 + 𝑏) ∈ (𝐴 ∪ 𝐵) ↔ ((𝑎 + 𝑏) ∈ 𝐴 ∨ (𝑎 + 𝑏) ∈ 𝐵))
28	26, 27	sylib 219	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑎 ∈ 𝐶) ∧ 𝑏 ∈ 𝐷) → ((𝑎 + 𝑏) ∈ 𝐴 ∨ (𝑎 + 𝑏) ∈ 𝐵))
29	28	orcomd 877	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑎 ∈ 𝐶) ∧ 𝑏 ∈ 𝐷) → ((𝑎 + 𝑏) ∈ 𝐵 ∨ (𝑎 + 𝑏) ∈ 𝐴))
30	29	ord 870	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑎 ∈ 𝐶) ∧ 𝑏 ∈ 𝐷) → (¬ (𝑎 + 𝑏) ∈ 𝐵 → (𝑎 + 𝑏) ∈ 𝐴))
31	24, 30	syld 47	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑎 ∈ 𝐶) ∧ 𝑏 ∈ 𝐷) → (∀𝑑 ∈ 𝐷 ¬ (𝑎 + 𝑑) ∈ 𝐵 → (𝑎 + 𝑏) ∈ 𝐴))
32	31	impancom 452	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑎 ∈ 𝐶) ∧ ∀𝑑 ∈ 𝐷 ¬ (𝑎 + 𝑑) ∈ 𝐵) → (𝑏 ∈ 𝐷 → (𝑎 + 𝑏) ∈ 𝐴))
33		unxpwdom3.lc	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑎 ∈ 𝐶) ∧ (𝑏 ∈ 𝐷 ∧ 𝑐 ∈ 𝐷)) → ((𝑎 + 𝑏) = (𝑎 + 𝑐) ↔ 𝑏 = 𝑐))
34	33	ex 413	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑎 ∈ 𝐶) → ((𝑏 ∈ 𝐷 ∧ 𝑐 ∈ 𝐷) → ((𝑎 + 𝑏) = (𝑎 + 𝑐) ↔ 𝑏 = 𝑐)))
35	34	adantr 481	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑎 ∈ 𝐶) ∧ ∀𝑑 ∈ 𝐷 ¬ (𝑎 + 𝑑) ∈ 𝐵) → ((𝑏 ∈ 𝐷 ∧ 𝑐 ∈ 𝐷) → ((𝑎 + 𝑏) = (𝑎 + 𝑐) ↔ 𝑏 = 𝑐)))
36	32, 35	dom2d 8930	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑎 ∈ 𝐶) ∧ ∀𝑑 ∈ 𝐷 ¬ (𝑎 + 𝑑) ∈ 𝐵) → (𝐴 ∈ 𝑉 → 𝐷 ≼ 𝐴))
37	19, 36	mpd 15	. . . . . 6 ⊢ (((𝜑 ∧ 𝑎 ∈ 𝐶) ∧ ∀𝑑 ∈ 𝐷 ¬ (𝑎 + 𝑑) ∈ 𝐵) → 𝐷 ≼ 𝐴)
38	17, 37	mtand 821	. . . . 5 ⊢ ((𝜑 ∧ 𝑎 ∈ 𝐶) → ¬ ∀𝑑 ∈ 𝐷 ¬ (𝑎 + 𝑑) ∈ 𝐵)
39		dfrex2 3066	. . . . 5 ⊢ (∃𝑑 ∈ 𝐷 (𝑎 + 𝑑) ∈ 𝐵 ↔ ¬ ∀𝑑 ∈ 𝐷 ¬ (𝑎 + 𝑑) ∈ 𝐵)
40	38, 39	sylibr 235	. . . 4 ⊢ ((𝜑 ∧ 𝑎 ∈ 𝐶) → ∃𝑑 ∈ 𝐷 (𝑎 + 𝑑) ∈ 𝐵)
41	15, 40	reximddv 3155	. . 3 ⊢ ((𝜑 ∧ 𝑎 ∈ 𝐶) → ∃𝑑 ∈ 𝐷 ∃𝑦 ∈ 𝐵 𝑎 = (℩𝑐 ∈ 𝐶 (𝑐 + 𝑑) = 𝑦))
42		vex 3435	. . . . . . . . 9 ⊢ 𝑑 ∈ V
43		vex 3435	. . . . . . . . 9 ⊢ 𝑦 ∈ V
44	42, 43	op1std 7941	. . . . . . . 8 ⊢ (𝑥 = ⟨𝑑, 𝑦⟩ → (1st ‘𝑥) = 𝑑)
45	44	oveq2d 7372	. . . . . . 7 ⊢ (𝑥 = ⟨𝑑, 𝑦⟩ → (𝑐 + (1st ‘𝑥)) = (𝑐 + 𝑑))
46	42, 43	op2ndd 7942	. . . . . . 7 ⊢ (𝑥 = ⟨𝑑, 𝑦⟩ → (2nd ‘𝑥) = 𝑦)
47	45, 46	eqeq12d 2755	. . . . . 6 ⊢ (𝑥 = ⟨𝑑, 𝑦⟩ → ((𝑐 + (1st ‘𝑥)) = (2nd ‘𝑥) ↔ (𝑐 + 𝑑) = 𝑦))
48	47	riotabidv 7315	. . . . 5 ⊢ (𝑥 = ⟨𝑑, 𝑦⟩ → (℩𝑐 ∈ 𝐶 (𝑐 + (1st ‘𝑥)) = (2nd ‘𝑥)) = (℩𝑐 ∈ 𝐶 (𝑐 + 𝑑) = 𝑦))
49	48	eqeq2d 2750	. . . 4 ⊢ (𝑥 = ⟨𝑑, 𝑦⟩ → (𝑎 = (℩𝑐 ∈ 𝐶 (𝑐 + (1st ‘𝑥)) = (2nd ‘𝑥)) ↔ 𝑎 = (℩𝑐 ∈ 𝐶 (𝑐 + 𝑑) = 𝑦)))
50	49	rexxp 5784	. . 3 ⊢ (∃𝑥 ∈ (𝐷 × 𝐵)𝑎 = (℩𝑐 ∈ 𝐶 (𝑐 + (1st ‘𝑥)) = (2nd ‘𝑥)) ↔ ∃𝑑 ∈ 𝐷 ∃𝑦 ∈ 𝐵 𝑎 = (℩𝑐 ∈ 𝐶 (𝑐 + 𝑑) = 𝑦))
51	41, 50	sylibr 235	. 2 ⊢ ((𝜑 ∧ 𝑎 ∈ 𝐶) → ∃𝑥 ∈ (𝐷 × 𝐵)𝑎 = (℩𝑐 ∈ 𝐶 (𝑐 + (1st ‘𝑥)) = (2nd ‘𝑥)))
52	3, 51	wdomd 9486	1 ⊢ (𝜑 → 𝐶 ≼* (𝐷 × 𝐵))

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 207   ∧ wa 396   ∨ wo 853   ∧ w3a 1092   = wceq 1547   ∈ wcel 2119  ∀wral 3053  ∃wrex 3063  Vcvv 3431   ∪ cun 3881  ⟨cop 4561   class class class wbr 5072   × cxp 5616  ‘cfv 6485  ℩crio 7312  (class class class)co 7356  1^st c1st 7929  2^nd c2nd 7930   ≼ cdom 8881   ≼^* cwdom 9469

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1974  ax-7 2015  ax-8 2121  ax-9 2129  ax-10 2152  ax-11 2168  ax-12 2189  ax-ext 2711  ax-rep 5199  ax-sep 5218  ax-nul 5228  ax-pow 5294  ax-pr 5362  ax-un 7678

This theorem depends on definitions:  df-bi 208  df-an 397  df-or 854  df-3an 1094  df-tru 1550  df-fal 1560  df-ex 1787  df-nf 1791  df-sb 2074  df-mo 2543  df-eu 2573  df-clab 2718  df-cleq 2731  df-clel 2814  df-nfc 2888  df-ne 2935  df-ral 3054  df-rex 3064  df-reu 3345  df-rab 3392  df-v 3433  df-sbc 3724  df-csb 3832  df-dif 3886  df-un 3888  df-in 3890  df-ss 3900  df-nul 4262  df-if 4455  df-pw 4531  df-sn 4556  df-pr 4558  df-op 4562  df-uni 4839  df-iun 4923  df-br 5073  df-opab 5135  df-mpt 5154  df-id 5513  df-xp 5624  df-rel 5625  df-cnv 5626  df-co 5627  df-dm 5628  df-rn 5629  df-res 5630  df-ima 5631  df-iota 6441  df-fun 6487  df-fn 6488  df-f 6489  df-f1 6490  df-fo 6491  df-f1o 6492  df-fv 6493  df-riota 7313  df-ov 7359  df-1st 7931  df-2nd 7932  df-en 8884  df-dom 8885  df-sdom 8886  df-wdom 9470

This theorem is referenced by:  isnumbasgrplem2  43549