HSE Home Hilbert Space Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  HSE Home  >  Th. List  >  mdslmd1lem2 Structured version   Visualization version   GIF version

Theorem mdslmd1lem2 29757
Description: Lemma for mdslmd1i 29760. (Contributed by NM, 29-Apr-2006.) (New usage is discouraged.)
Hypotheses
Ref Expression
mdslmd.1 𝐴C
mdslmd.2 𝐵C
mdslmd.3 𝐶C
mdslmd.4 𝐷C
mdslmd1lem.5 𝑅C
Assertion
Ref Expression
mdslmd1lem2 (((𝐴 𝑀 𝐵𝐵 𝑀* 𝐴) ∧ ((𝐴𝐶𝐴𝐷) ∧ (𝐶 ⊆ (𝐴 𝐵) ∧ 𝐷 ⊆ (𝐴 𝐵)))) → (((𝑅𝐵) ⊆ (𝐷𝐵) → (((𝑅𝐵) ∨ (𝐶𝐵)) ∩ (𝐷𝐵)) ⊆ ((𝑅𝐵) ∨ ((𝐶𝐵) ∩ (𝐷𝐵)))) → (((𝐶𝐷) ⊆ 𝑅𝑅𝐷) → ((𝑅 𝐶) ∩ 𝐷) ⊆ (𝑅 (𝐶𝐷)))))

Proof of Theorem mdslmd1lem2
StepHypRef Expression
1 ssrin 4058 . . . 4 (𝑅𝐷 → (𝑅𝐵) ⊆ (𝐷𝐵))
21adantl 475 . . 3 (((𝐶𝐷) ⊆ 𝑅𝑅𝐷) → (𝑅𝐵) ⊆ (𝐷𝐵))
32imim1i 63 . 2 (((𝑅𝐵) ⊆ (𝐷𝐵) → (((𝑅𝐵) ∨ (𝐶𝐵)) ∩ (𝐷𝐵)) ⊆ ((𝑅𝐵) ∨ ((𝐶𝐵) ∩ (𝐷𝐵)))) → (((𝐶𝐷) ⊆ 𝑅𝑅𝐷) → (((𝑅𝐵) ∨ (𝐶𝐵)) ∩ (𝐷𝐵)) ⊆ ((𝑅𝐵) ∨ ((𝐶𝐵) ∩ (𝐷𝐵)))))
4 simpllr 766 . . . . . 6 ((((𝐴 𝑀 𝐵𝐵 𝑀* 𝐴) ∧ ((𝐴𝐶𝐴𝐷) ∧ (𝐶 ⊆ (𝐴 𝐵) ∧ 𝐷 ⊆ (𝐴 𝐵)))) ∧ ((𝐶𝐷) ⊆ 𝑅𝑅𝐷)) → 𝐵 𝑀* 𝐴)
5 mdslmd.3 . . . . . . . . . . . 12 𝐶C
6 mdslmd1lem.5 . . . . . . . . . . . 12 𝑅C
75, 6chub2i 28901 . . . . . . . . . . 11 𝐶 ⊆ (𝑅 𝐶)
8 sstr 3829 . . . . . . . . . . 11 ((𝐴𝐶𝐶 ⊆ (𝑅 𝐶)) → 𝐴 ⊆ (𝑅 𝐶))
97, 8mpan2 681 . . . . . . . . . 10 (𝐴𝐶𝐴 ⊆ (𝑅 𝐶))
109ad2antrr 716 . . . . . . . . 9 (((𝐴𝐶𝐴𝐷) ∧ (𝐶 ⊆ (𝐴 𝐵) ∧ 𝐷 ⊆ (𝐴 𝐵))) → 𝐴 ⊆ (𝑅 𝐶))
1110ad2antlr 717 . . . . . . . 8 ((((𝐴 𝑀 𝐵𝐵 𝑀* 𝐴) ∧ ((𝐴𝐶𝐴𝐷) ∧ (𝐶 ⊆ (𝐴 𝐵) ∧ 𝐷 ⊆ (𝐴 𝐵)))) ∧ ((𝐶𝐷) ⊆ 𝑅𝑅𝐷)) → 𝐴 ⊆ (𝑅 𝐶))
12 simplr 759 . . . . . . . . 9 (((𝐴𝐶𝐴𝐷) ∧ (𝐶 ⊆ (𝐴 𝐵) ∧ 𝐷 ⊆ (𝐴 𝐵))) → 𝐴𝐷)
1312ad2antlr 717 . . . . . . . 8 ((((𝐴 𝑀 𝐵𝐵 𝑀* 𝐴) ∧ ((𝐴𝐶𝐴𝐷) ∧ (𝐶 ⊆ (𝐴 𝐵) ∧ 𝐷 ⊆ (𝐴 𝐵)))) ∧ ((𝐶𝐷) ⊆ 𝑅𝑅𝐷)) → 𝐴𝐷)
1411, 13ssind 4057 . . . . . . 7 ((((𝐴 𝑀 𝐵𝐵 𝑀* 𝐴) ∧ ((𝐴𝐶𝐴𝐷) ∧ (𝐶 ⊆ (𝐴 𝐵) ∧ 𝐷 ⊆ (𝐴 𝐵)))) ∧ ((𝐶𝐷) ⊆ 𝑅𝑅𝐷)) → 𝐴 ⊆ ((𝑅 𝐶) ∩ 𝐷))
15 ssin 4055 . . . . . . . . . 10 ((𝐴𝐶𝐴𝐷) ↔ 𝐴 ⊆ (𝐶𝐷))
16 mdslmd.4 . . . . . . . . . . . . 13 𝐷C
175, 16chincli 28891 . . . . . . . . . . . 12 (𝐶𝐷) ∈ C
1817, 6chub2i 28901 . . . . . . . . . . 11 (𝐶𝐷) ⊆ (𝑅 (𝐶𝐷))
19 sstr 3829 . . . . . . . . . . 11 ((𝐴 ⊆ (𝐶𝐷) ∧ (𝐶𝐷) ⊆ (𝑅 (𝐶𝐷))) → 𝐴 ⊆ (𝑅 (𝐶𝐷)))
2018, 19mpan2 681 . . . . . . . . . 10 (𝐴 ⊆ (𝐶𝐷) → 𝐴 ⊆ (𝑅 (𝐶𝐷)))
2115, 20sylbi 209 . . . . . . . . 9 ((𝐴𝐶𝐴𝐷) → 𝐴 ⊆ (𝑅 (𝐶𝐷)))
2221adantr 474 . . . . . . . 8 (((𝐴𝐶𝐴𝐷) ∧ (𝐶 ⊆ (𝐴 𝐵) ∧ 𝐷 ⊆ (𝐴 𝐵))) → 𝐴 ⊆ (𝑅 (𝐶𝐷)))
2322ad2antlr 717 . . . . . . 7 ((((𝐴 𝑀 𝐵𝐵 𝑀* 𝐴) ∧ ((𝐴𝐶𝐴𝐷) ∧ (𝐶 ⊆ (𝐴 𝐵) ∧ 𝐷 ⊆ (𝐴 𝐵)))) ∧ ((𝐶𝐷) ⊆ 𝑅𝑅𝐷)) → 𝐴 ⊆ (𝑅 (𝐶𝐷)))
2414, 23ssind 4057 . . . . . 6 ((((𝐴 𝑀 𝐵𝐵 𝑀* 𝐴) ∧ ((𝐴𝐶𝐴𝐷) ∧ (𝐶 ⊆ (𝐴 𝐵) ∧ 𝐷 ⊆ (𝐴 𝐵)))) ∧ ((𝐶𝐷) ⊆ 𝑅𝑅𝐷)) → 𝐴 ⊆ (((𝑅 𝐶) ∩ 𝐷) ∩ (𝑅 (𝐶𝐷))))
25 inss2 4054 . . . . . . . . . . 11 ((𝑅 𝐶) ∩ 𝐷) ⊆ 𝐷
26 sstr 3829 . . . . . . . . . . 11 ((((𝑅 𝐶) ∩ 𝐷) ⊆ 𝐷𝐷 ⊆ (𝐴 𝐵)) → ((𝑅 𝐶) ∩ 𝐷) ⊆ (𝐴 𝐵))
2725, 26mpan 680 . . . . . . . . . 10 (𝐷 ⊆ (𝐴 𝐵) → ((𝑅 𝐶) ∩ 𝐷) ⊆ (𝐴 𝐵))
2827ad2antll 719 . . . . . . . . 9 (((𝐴𝐶𝐴𝐷) ∧ (𝐶 ⊆ (𝐴 𝐵) ∧ 𝐷 ⊆ (𝐴 𝐵))) → ((𝑅 𝐶) ∩ 𝐷) ⊆ (𝐴 𝐵))
2928ad2antlr 717 . . . . . . . 8 ((((𝐴 𝑀 𝐵𝐵 𝑀* 𝐴) ∧ ((𝐴𝐶𝐴𝐷) ∧ (𝐶 ⊆ (𝐴 𝐵) ∧ 𝐷 ⊆ (𝐴 𝐵)))) ∧ ((𝐶𝐷) ⊆ 𝑅𝑅𝐷)) → ((𝑅 𝐶) ∩ 𝐷) ⊆ (𝐴 𝐵))
30 sstr 3829 . . . . . . . . . . . . . 14 ((𝑅𝐷𝐷 ⊆ (𝐴 𝐵)) → 𝑅 ⊆ (𝐴 𝐵))
3130ancoms 452 . . . . . . . . . . . . 13 ((𝐷 ⊆ (𝐴 𝐵) ∧ 𝑅𝐷) → 𝑅 ⊆ (𝐴 𝐵))
3231ad2ant2l 736 . . . . . . . . . . . 12 (((𝐶 ⊆ (𝐴 𝐵) ∧ 𝐷 ⊆ (𝐴 𝐵)) ∧ ((𝐶𝐷) ⊆ 𝑅𝑅𝐷)) → 𝑅 ⊆ (𝐴 𝐵))
3332adantll 704 . . . . . . . . . . 11 ((((𝐴𝐶𝐴𝐷) ∧ (𝐶 ⊆ (𝐴 𝐵) ∧ 𝐷 ⊆ (𝐴 𝐵))) ∧ ((𝐶𝐷) ⊆ 𝑅𝑅𝐷)) → 𝑅 ⊆ (𝐴 𝐵))
3433adantll 704 . . . . . . . . . 10 ((((𝐴 𝑀 𝐵𝐵 𝑀* 𝐴) ∧ ((𝐴𝐶𝐴𝐷) ∧ (𝐶 ⊆ (𝐴 𝐵) ∧ 𝐷 ⊆ (𝐴 𝐵)))) ∧ ((𝐶𝐷) ⊆ 𝑅𝑅𝐷)) → 𝑅 ⊆ (𝐴 𝐵))
35 ssinss1 4062 . . . . . . . . . . . 12 (𝐶 ⊆ (𝐴 𝐵) → (𝐶𝐷) ⊆ (𝐴 𝐵))
3635ad2antrl 718 . . . . . . . . . . 11 (((𝐴𝐶𝐴𝐷) ∧ (𝐶 ⊆ (𝐴 𝐵) ∧ 𝐷 ⊆ (𝐴 𝐵))) → (𝐶𝐷) ⊆ (𝐴 𝐵))
3736ad2antlr 717 . . . . . . . . . 10 ((((𝐴 𝑀 𝐵𝐵 𝑀* 𝐴) ∧ ((𝐴𝐶𝐴𝐷) ∧ (𝐶 ⊆ (𝐴 𝐵) ∧ 𝐷 ⊆ (𝐴 𝐵)))) ∧ ((𝐶𝐷) ⊆ 𝑅𝑅𝐷)) → (𝐶𝐷) ⊆ (𝐴 𝐵))
3834, 37jca 507 . . . . . . . . 9 ((((𝐴 𝑀 𝐵𝐵 𝑀* 𝐴) ∧ ((𝐴𝐶𝐴𝐷) ∧ (𝐶 ⊆ (𝐴 𝐵) ∧ 𝐷 ⊆ (𝐴 𝐵)))) ∧ ((𝐶𝐷) ⊆ 𝑅𝑅𝐷)) → (𝑅 ⊆ (𝐴 𝐵) ∧ (𝐶𝐷) ⊆ (𝐴 𝐵)))
39 mdslmd.1 . . . . . . . . . . 11 𝐴C
40 mdslmd.2 . . . . . . . . . . 11 𝐵C
4139, 40chjcli 28888 . . . . . . . . . 10 (𝐴 𝐵) ∈ C
426, 17, 41chlubi 28902 . . . . . . . . 9 ((𝑅 ⊆ (𝐴 𝐵) ∧ (𝐶𝐷) ⊆ (𝐴 𝐵)) ↔ (𝑅 (𝐶𝐷)) ⊆ (𝐴 𝐵))
4338, 42sylib 210 . . . . . . . 8 ((((𝐴 𝑀 𝐵𝐵 𝑀* 𝐴) ∧ ((𝐴𝐶𝐴𝐷) ∧ (𝐶 ⊆ (𝐴 𝐵) ∧ 𝐷 ⊆ (𝐴 𝐵)))) ∧ ((𝐶𝐷) ⊆ 𝑅𝑅𝐷)) → (𝑅 (𝐶𝐷)) ⊆ (𝐴 𝐵))
4429, 43jca 507 . . . . . . 7 ((((𝐴 𝑀 𝐵𝐵 𝑀* 𝐴) ∧ ((𝐴𝐶𝐴𝐷) ∧ (𝐶 ⊆ (𝐴 𝐵) ∧ 𝐷 ⊆ (𝐴 𝐵)))) ∧ ((𝐶𝐷) ⊆ 𝑅𝑅𝐷)) → (((𝑅 𝐶) ∩ 𝐷) ⊆ (𝐴 𝐵) ∧ (𝑅 (𝐶𝐷)) ⊆ (𝐴 𝐵)))
456, 5chjcli 28888 . . . . . . . . 9 (𝑅 𝐶) ∈ C
4645, 16chincli 28891 . . . . . . . 8 ((𝑅 𝐶) ∩ 𝐷) ∈ C
476, 17chjcli 28888 . . . . . . . 8 (𝑅 (𝐶𝐷)) ∈ C
4846, 47, 41chlubi 28902 . . . . . . 7 ((((𝑅 𝐶) ∩ 𝐷) ⊆ (𝐴 𝐵) ∧ (𝑅 (𝐶𝐷)) ⊆ (𝐴 𝐵)) ↔ (((𝑅 𝐶) ∩ 𝐷) ∨ (𝑅 (𝐶𝐷))) ⊆ (𝐴 𝐵))
4944, 48sylib 210 . . . . . 6 ((((𝐴 𝑀 𝐵𝐵 𝑀* 𝐴) ∧ ((𝐴𝐶𝐴𝐷) ∧ (𝐶 ⊆ (𝐴 𝐵) ∧ 𝐷 ⊆ (𝐴 𝐵)))) ∧ ((𝐶𝐷) ⊆ 𝑅𝑅𝐷)) → (((𝑅 𝐶) ∩ 𝐷) ∨ (𝑅 (𝐶𝐷))) ⊆ (𝐴 𝐵))
5039, 40, 46, 47mdslle1i 29748 . . . . . 6 ((𝐵 𝑀* 𝐴𝐴 ⊆ (((𝑅 𝐶) ∩ 𝐷) ∩ (𝑅 (𝐶𝐷))) ∧ (((𝑅 𝐶) ∩ 𝐷) ∨ (𝑅 (𝐶𝐷))) ⊆ (𝐴 𝐵)) → (((𝑅 𝐶) ∩ 𝐷) ⊆ (𝑅 (𝐶𝐷)) ↔ (((𝑅 𝐶) ∩ 𝐷) ∩ 𝐵) ⊆ ((𝑅 (𝐶𝐷)) ∩ 𝐵)))
514, 24, 49, 50syl3anc 1439 . . . . 5 ((((𝐴 𝑀 𝐵𝐵 𝑀* 𝐴) ∧ ((𝐴𝐶𝐴𝐷) ∧ (𝐶 ⊆ (𝐴 𝐵) ∧ 𝐷 ⊆ (𝐴 𝐵)))) ∧ ((𝐶𝐷) ⊆ 𝑅𝑅𝐷)) → (((𝑅 𝐶) ∩ 𝐷) ⊆ (𝑅 (𝐶𝐷)) ↔ (((𝑅 𝐶) ∩ 𝐷) ∩ 𝐵) ⊆ ((𝑅 (𝐶𝐷)) ∩ 𝐵)))
52 inindir 4052 . . . . . . 7 (((𝑅 𝐶) ∩ 𝐷) ∩ 𝐵) = (((𝑅 𝐶) ∩ 𝐵) ∩ (𝐷𝐵))
53 sstr 3829 . . . . . . . . . . . . . 14 ((𝐴 ⊆ (𝐶𝐷) ∧ (𝐶𝐷) ⊆ 𝑅) → 𝐴𝑅)
5415, 53sylanb 576 . . . . . . . . . . . . 13 (((𝐴𝐶𝐴𝐷) ∧ (𝐶𝐷) ⊆ 𝑅) → 𝐴𝑅)
5554ad2ant2r 737 . . . . . . . . . . . 12 ((((𝐴𝐶𝐴𝐷) ∧ (𝐶 ⊆ (𝐴 𝐵) ∧ 𝐷 ⊆ (𝐴 𝐵))) ∧ ((𝐶𝐷) ⊆ 𝑅𝑅𝐷)) → 𝐴𝑅)
56 simplll 765 . . . . . . . . . . . 12 ((((𝐴𝐶𝐴𝐷) ∧ (𝐶 ⊆ (𝐴 𝐵) ∧ 𝐷 ⊆ (𝐴 𝐵))) ∧ ((𝐶𝐷) ⊆ 𝑅𝑅𝐷)) → 𝐴𝐶)
5755, 56ssind 4057 . . . . . . . . . . 11 ((((𝐴𝐶𝐴𝐷) ∧ (𝐶 ⊆ (𝐴 𝐵) ∧ 𝐷 ⊆ (𝐴 𝐵))) ∧ ((𝐶𝐷) ⊆ 𝑅𝑅𝐷)) → 𝐴 ⊆ (𝑅𝐶))
58 simplrl 767 . . . . . . . . . . . . 13 ((((𝐴𝐶𝐴𝐷) ∧ (𝐶 ⊆ (𝐴 𝐵) ∧ 𝐷 ⊆ (𝐴 𝐵))) ∧ ((𝐶𝐷) ⊆ 𝑅𝑅𝐷)) → 𝐶 ⊆ (𝐴 𝐵))
5933, 58jca 507 . . . . . . . . . . . 12 ((((𝐴𝐶𝐴𝐷) ∧ (𝐶 ⊆ (𝐴 𝐵) ∧ 𝐷 ⊆ (𝐴 𝐵))) ∧ ((𝐶𝐷) ⊆ 𝑅𝑅𝐷)) → (𝑅 ⊆ (𝐴 𝐵) ∧ 𝐶 ⊆ (𝐴 𝐵)))
606, 5, 41chlubi 28902 . . . . . . . . . . . 12 ((𝑅 ⊆ (𝐴 𝐵) ∧ 𝐶 ⊆ (𝐴 𝐵)) ↔ (𝑅 𝐶) ⊆ (𝐴 𝐵))
6159, 60sylib 210 . . . . . . . . . . 11 ((((𝐴𝐶𝐴𝐷) ∧ (𝐶 ⊆ (𝐴 𝐵) ∧ 𝐷 ⊆ (𝐴 𝐵))) ∧ ((𝐶𝐷) ⊆ 𝑅𝑅𝐷)) → (𝑅 𝐶) ⊆ (𝐴 𝐵))
6257, 61jca 507 . . . . . . . . . 10 ((((𝐴𝐶𝐴𝐷) ∧ (𝐶 ⊆ (𝐴 𝐵) ∧ 𝐷 ⊆ (𝐴 𝐵))) ∧ ((𝐶𝐷) ⊆ 𝑅𝑅𝐷)) → (𝐴 ⊆ (𝑅𝐶) ∧ (𝑅 𝐶) ⊆ (𝐴 𝐵)))
6339, 40, 6, 5mdslj1i 29750 . . . . . . . . . 10 (((𝐴 𝑀 𝐵𝐵 𝑀* 𝐴) ∧ (𝐴 ⊆ (𝑅𝐶) ∧ (𝑅 𝐶) ⊆ (𝐴 𝐵))) → ((𝑅 𝐶) ∩ 𝐵) = ((𝑅𝐵) ∨ (𝐶𝐵)))
6462, 63sylan2 586 . . . . . . . . 9 (((𝐴 𝑀 𝐵𝐵 𝑀* 𝐴) ∧ (((𝐴𝐶𝐴𝐷) ∧ (𝐶 ⊆ (𝐴 𝐵) ∧ 𝐷 ⊆ (𝐴 𝐵))) ∧ ((𝐶𝐷) ⊆ 𝑅𝑅𝐷))) → ((𝑅 𝐶) ∩ 𝐵) = ((𝑅𝐵) ∨ (𝐶𝐵)))
6564anassrs 461 . . . . . . . 8 ((((𝐴 𝑀 𝐵𝐵 𝑀* 𝐴) ∧ ((𝐴𝐶𝐴𝐷) ∧ (𝐶 ⊆ (𝐴 𝐵) ∧ 𝐷 ⊆ (𝐴 𝐵)))) ∧ ((𝐶𝐷) ⊆ 𝑅𝑅𝐷)) → ((𝑅 𝐶) ∩ 𝐵) = ((𝑅𝐵) ∨ (𝐶𝐵)))
6665ineq1d 4036 . . . . . . 7 ((((𝐴 𝑀 𝐵𝐵 𝑀* 𝐴) ∧ ((𝐴𝐶𝐴𝐷) ∧ (𝐶 ⊆ (𝐴 𝐵) ∧ 𝐷 ⊆ (𝐴 𝐵)))) ∧ ((𝐶𝐷) ⊆ 𝑅𝑅𝐷)) → (((𝑅 𝐶) ∩ 𝐵) ∩ (𝐷𝐵)) = (((𝑅𝐵) ∨ (𝐶𝐵)) ∩ (𝐷𝐵)))
6752, 66syl5req 2827 . . . . . 6 ((((𝐴 𝑀 𝐵𝐵 𝑀* 𝐴) ∧ ((𝐴𝐶𝐴𝐷) ∧ (𝐶 ⊆ (𝐴 𝐵) ∧ 𝐷 ⊆ (𝐴 𝐵)))) ∧ ((𝐶𝐷) ⊆ 𝑅𝑅𝐷)) → (((𝑅𝐵) ∨ (𝐶𝐵)) ∩ (𝐷𝐵)) = (((𝑅 𝐶) ∩ 𝐷) ∩ 𝐵))
6815biimpi 208 . . . . . . . . . . . . 13 ((𝐴𝐶𝐴𝐷) → 𝐴 ⊆ (𝐶𝐷))
6968adantr 474 . . . . . . . . . . . 12 (((𝐴𝐶𝐴𝐷) ∧ (𝐶𝐷) ⊆ 𝑅) → 𝐴 ⊆ (𝐶𝐷))
7054, 69ssind 4057 . . . . . . . . . . 11 (((𝐴𝐶𝐴𝐷) ∧ (𝐶𝐷) ⊆ 𝑅) → 𝐴 ⊆ (𝑅 ∩ (𝐶𝐷)))
7131adantll 704 . . . . . . . . . . . . 13 (((𝐶 ⊆ (𝐴 𝐵) ∧ 𝐷 ⊆ (𝐴 𝐵)) ∧ 𝑅𝐷) → 𝑅 ⊆ (𝐴 𝐵))
7235ad2antrr 716 . . . . . . . . . . . . 13 (((𝐶 ⊆ (𝐴 𝐵) ∧ 𝐷 ⊆ (𝐴 𝐵)) ∧ 𝑅𝐷) → (𝐶𝐷) ⊆ (𝐴 𝐵))
7371, 72jca 507 . . . . . . . . . . . 12 (((𝐶 ⊆ (𝐴 𝐵) ∧ 𝐷 ⊆ (𝐴 𝐵)) ∧ 𝑅𝐷) → (𝑅 ⊆ (𝐴 𝐵) ∧ (𝐶𝐷) ⊆ (𝐴 𝐵)))
7473, 42sylib 210 . . . . . . . . . . 11 (((𝐶 ⊆ (𝐴 𝐵) ∧ 𝐷 ⊆ (𝐴 𝐵)) ∧ 𝑅𝐷) → (𝑅 (𝐶𝐷)) ⊆ (𝐴 𝐵))
7570, 74anim12i 606 . . . . . . . . . 10 ((((𝐴𝐶𝐴𝐷) ∧ (𝐶𝐷) ⊆ 𝑅) ∧ ((𝐶 ⊆ (𝐴 𝐵) ∧ 𝐷 ⊆ (𝐴 𝐵)) ∧ 𝑅𝐷)) → (𝐴 ⊆ (𝑅 ∩ (𝐶𝐷)) ∧ (𝑅 (𝐶𝐷)) ⊆ (𝐴 𝐵)))
7675an4s 650 . . . . . . . . 9 ((((𝐴𝐶𝐴𝐷) ∧ (𝐶 ⊆ (𝐴 𝐵) ∧ 𝐷 ⊆ (𝐴 𝐵))) ∧ ((𝐶𝐷) ⊆ 𝑅𝑅𝐷)) → (𝐴 ⊆ (𝑅 ∩ (𝐶𝐷)) ∧ (𝑅 (𝐶𝐷)) ⊆ (𝐴 𝐵)))
7739, 40, 6, 17mdslj1i 29750 . . . . . . . . 9 (((𝐴 𝑀 𝐵𝐵 𝑀* 𝐴) ∧ (𝐴 ⊆ (𝑅 ∩ (𝐶𝐷)) ∧ (𝑅 (𝐶𝐷)) ⊆ (𝐴 𝐵))) → ((𝑅 (𝐶𝐷)) ∩ 𝐵) = ((𝑅𝐵) ∨ ((𝐶𝐷) ∩ 𝐵)))
7876, 77sylan2 586 . . . . . . . 8 (((𝐴 𝑀 𝐵𝐵 𝑀* 𝐴) ∧ (((𝐴𝐶𝐴𝐷) ∧ (𝐶 ⊆ (𝐴 𝐵) ∧ 𝐷 ⊆ (𝐴 𝐵))) ∧ ((𝐶𝐷) ⊆ 𝑅𝑅𝐷))) → ((𝑅 (𝐶𝐷)) ∩ 𝐵) = ((𝑅𝐵) ∨ ((𝐶𝐷) ∩ 𝐵)))
7978anassrs 461 . . . . . . 7 ((((𝐴 𝑀 𝐵𝐵 𝑀* 𝐴) ∧ ((𝐴𝐶𝐴𝐷) ∧ (𝐶 ⊆ (𝐴 𝐵) ∧ 𝐷 ⊆ (𝐴 𝐵)))) ∧ ((𝐶𝐷) ⊆ 𝑅𝑅𝐷)) → ((𝑅 (𝐶𝐷)) ∩ 𝐵) = ((𝑅𝐵) ∨ ((𝐶𝐷) ∩ 𝐵)))
80 inindir 4052 . . . . . . . . 9 ((𝐶𝐷) ∩ 𝐵) = ((𝐶𝐵) ∩ (𝐷𝐵))
8180a1i 11 . . . . . . . 8 ((((𝐴 𝑀 𝐵𝐵 𝑀* 𝐴) ∧ ((𝐴𝐶𝐴𝐷) ∧ (𝐶 ⊆ (𝐴 𝐵) ∧ 𝐷 ⊆ (𝐴 𝐵)))) ∧ ((𝐶𝐷) ⊆ 𝑅𝑅𝐷)) → ((𝐶𝐷) ∩ 𝐵) = ((𝐶𝐵) ∩ (𝐷𝐵)))
8281oveq2d 6938 . . . . . . 7 ((((𝐴 𝑀 𝐵𝐵 𝑀* 𝐴) ∧ ((𝐴𝐶𝐴𝐷) ∧ (𝐶 ⊆ (𝐴 𝐵) ∧ 𝐷 ⊆ (𝐴 𝐵)))) ∧ ((𝐶𝐷) ⊆ 𝑅𝑅𝐷)) → ((𝑅𝐵) ∨ ((𝐶𝐷) ∩ 𝐵)) = ((𝑅𝐵) ∨ ((𝐶𝐵) ∩ (𝐷𝐵))))
8379, 82eqtr2d 2815 . . . . . 6 ((((𝐴 𝑀 𝐵𝐵 𝑀* 𝐴) ∧ ((𝐴𝐶𝐴𝐷) ∧ (𝐶 ⊆ (𝐴 𝐵) ∧ 𝐷 ⊆ (𝐴 𝐵)))) ∧ ((𝐶𝐷) ⊆ 𝑅𝑅𝐷)) → ((𝑅𝐵) ∨ ((𝐶𝐵) ∩ (𝐷𝐵))) = ((𝑅 (𝐶𝐷)) ∩ 𝐵))
8467, 83sseq12d 3853 . . . . 5 ((((𝐴 𝑀 𝐵𝐵 𝑀* 𝐴) ∧ ((𝐴𝐶𝐴𝐷) ∧ (𝐶 ⊆ (𝐴 𝐵) ∧ 𝐷 ⊆ (𝐴 𝐵)))) ∧ ((𝐶𝐷) ⊆ 𝑅𝑅𝐷)) → ((((𝑅𝐵) ∨ (𝐶𝐵)) ∩ (𝐷𝐵)) ⊆ ((𝑅𝐵) ∨ ((𝐶𝐵) ∩ (𝐷𝐵))) ↔ (((𝑅 𝐶) ∩ 𝐷) ∩ 𝐵) ⊆ ((𝑅 (𝐶𝐷)) ∩ 𝐵)))
8551, 84bitr4d 274 . . . 4 ((((𝐴 𝑀 𝐵𝐵 𝑀* 𝐴) ∧ ((𝐴𝐶𝐴𝐷) ∧ (𝐶 ⊆ (𝐴 𝐵) ∧ 𝐷 ⊆ (𝐴 𝐵)))) ∧ ((𝐶𝐷) ⊆ 𝑅𝑅𝐷)) → (((𝑅 𝐶) ∩ 𝐷) ⊆ (𝑅 (𝐶𝐷)) ↔ (((𝑅𝐵) ∨ (𝐶𝐵)) ∩ (𝐷𝐵)) ⊆ ((𝑅𝐵) ∨ ((𝐶𝐵) ∩ (𝐷𝐵)))))
8685exbiri 801 . . 3 (((𝐴 𝑀 𝐵𝐵 𝑀* 𝐴) ∧ ((𝐴𝐶𝐴𝐷) ∧ (𝐶 ⊆ (𝐴 𝐵) ∧ 𝐷 ⊆ (𝐴 𝐵)))) → (((𝐶𝐷) ⊆ 𝑅𝑅𝐷) → ((((𝑅𝐵) ∨ (𝐶𝐵)) ∩ (𝐷𝐵)) ⊆ ((𝑅𝐵) ∨ ((𝐶𝐵) ∩ (𝐷𝐵))) → ((𝑅 𝐶) ∩ 𝐷) ⊆ (𝑅 (𝐶𝐷)))))
8786a2d 29 . 2 (((𝐴 𝑀 𝐵𝐵 𝑀* 𝐴) ∧ ((𝐴𝐶𝐴𝐷) ∧ (𝐶 ⊆ (𝐴 𝐵) ∧ 𝐷 ⊆ (𝐴 𝐵)))) → ((((𝐶𝐷) ⊆ 𝑅𝑅𝐷) → (((𝑅𝐵) ∨ (𝐶𝐵)) ∩ (𝐷𝐵)) ⊆ ((𝑅𝐵) ∨ ((𝐶𝐵) ∩ (𝐷𝐵)))) → (((𝐶𝐷) ⊆ 𝑅𝑅𝐷) → ((𝑅 𝐶) ∩ 𝐷) ⊆ (𝑅 (𝐶𝐷)))))
883, 87syl5 34 1 (((𝐴 𝑀 𝐵𝐵 𝑀* 𝐴) ∧ ((𝐴𝐶𝐴𝐷) ∧ (𝐶 ⊆ (𝐴 𝐵) ∧ 𝐷 ⊆ (𝐴 𝐵)))) → (((𝑅𝐵) ⊆ (𝐷𝐵) → (((𝑅𝐵) ∨ (𝐶𝐵)) ∩ (𝐷𝐵)) ⊆ ((𝑅𝐵) ∨ ((𝐶𝐵) ∩ (𝐷𝐵)))) → (((𝐶𝐷) ⊆ 𝑅𝑅𝐷) → ((𝑅 𝐶) ∩ 𝐷) ⊆ (𝑅 (𝐶𝐷)))))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 198  wa 386   = wceq 1601  wcel 2107  cin 3791  wss 3792   class class class wbr 4886  (class class class)co 6922   C cch 28358   chj 28362   𝑀 cmd 28395   𝑀* cdmd 28396
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1839  ax-4 1853  ax-5 1953  ax-6 2021  ax-7 2055  ax-8 2109  ax-9 2116  ax-10 2135  ax-11 2150  ax-12 2163  ax-13 2334  ax-ext 2754  ax-rep 5006  ax-sep 5017  ax-nul 5025  ax-pow 5077  ax-pr 5138  ax-un 7226  ax-inf2 8835  ax-cc 9592  ax-cnex 10328  ax-resscn 10329  ax-1cn 10330  ax-icn 10331  ax-addcl 10332  ax-addrcl 10333  ax-mulcl 10334  ax-mulrcl 10335  ax-mulcom 10336  ax-addass 10337  ax-mulass 10338  ax-distr 10339  ax-i2m1 10340  ax-1ne0 10341  ax-1rid 10342  ax-rnegex 10343  ax-rrecex 10344  ax-cnre 10345  ax-pre-lttri 10346  ax-pre-lttrn 10347  ax-pre-ltadd 10348  ax-pre-mulgt0 10349  ax-pre-sup 10350  ax-addf 10351  ax-mulf 10352  ax-hilex 28428  ax-hfvadd 28429  ax-hvcom 28430  ax-hvass 28431  ax-hv0cl 28432  ax-hvaddid 28433  ax-hfvmul 28434  ax-hvmulid 28435  ax-hvmulass 28436  ax-hvdistr1 28437  ax-hvdistr2 28438  ax-hvmul0 28439  ax-hfi 28508  ax-his1 28511  ax-his2 28512  ax-his3 28513  ax-his4 28514  ax-hcompl 28631
This theorem depends on definitions:  df-bi 199  df-an 387  df-or 837  df-3or 1072  df-3an 1073  df-tru 1605  df-fal 1615  df-ex 1824  df-nf 1828  df-sb 2012  df-mo 2551  df-eu 2587  df-clab 2764  df-cleq 2770  df-clel 2774  df-nfc 2921  df-ne 2970  df-nel 3076  df-ral 3095  df-rex 3096  df-reu 3097  df-rmo 3098  df-rab 3099  df-v 3400  df-sbc 3653  df-csb 3752  df-dif 3795  df-un 3797  df-in 3799  df-ss 3806  df-pss 3808  df-nul 4142  df-if 4308  df-pw 4381  df-sn 4399  df-pr 4401  df-tp 4403  df-op 4405  df-uni 4672  df-int 4711  df-iun 4755  df-iin 4756  df-br 4887  df-opab 4949  df-mpt 4966  df-tr 4988  df-id 5261  df-eprel 5266  df-po 5274  df-so 5275  df-fr 5314  df-se 5315  df-we 5316  df-xp 5361  df-rel 5362  df-cnv 5363  df-co 5364  df-dm 5365  df-rn 5366  df-res 5367  df-ima 5368  df-pred 5933  df-ord 5979  df-on 5980  df-lim 5981  df-suc 5982  df-iota 6099  df-fun 6137  df-fn 6138  df-f 6139  df-f1 6140  df-fo 6141  df-f1o 6142  df-fv 6143  df-isom 6144  df-riota 6883  df-ov 6925  df-oprab 6926  df-mpt2 6927  df-of 7174  df-om 7344  df-1st 7445  df-2nd 7446  df-supp 7577  df-wrecs 7689  df-recs 7751  df-rdg 7789  df-1o 7843  df-2o 7844  df-oadd 7847  df-omul 7848  df-er 8026  df-map 8142  df-pm 8143  df-ixp 8195  df-en 8242  df-dom 8243  df-sdom 8244  df-fin 8245  df-fsupp 8564  df-fi 8605  df-sup 8636  df-inf 8637  df-oi 8704  df-card 9098  df-acn 9101  df-cda 9325  df-pnf 10413  df-mnf 10414  df-xr 10415  df-ltxr 10416  df-le 10417  df-sub 10608  df-neg 10609  df-div 11033  df-nn 11375  df-2 11438  df-3 11439  df-4 11440  df-5 11441  df-6 11442  df-7 11443  df-8 11444  df-9 11445  df-n0 11643  df-z 11729  df-dec 11846  df-uz 11993  df-q 12096  df-rp 12138  df-xneg 12257  df-xadd 12258  df-xmul 12259  df-ioo 12491  df-ico 12493  df-icc 12494  df-fz 12644  df-fzo 12785  df-fl 12912  df-seq 13120  df-exp 13179  df-hash 13436  df-cj 14246  df-re 14247  df-im 14248  df-sqrt 14382  df-abs 14383  df-clim 14627  df-rlim 14628  df-sum 14825  df-struct 16257  df-ndx 16258  df-slot 16259  df-base 16261  df-sets 16262  df-ress 16263  df-plusg 16351  df-mulr 16352  df-starv 16353  df-sca 16354  df-vsca 16355  df-ip 16356  df-tset 16357  df-ple 16358  df-ds 16360  df-unif 16361  df-hom 16362  df-cco 16363  df-rest 16469  df-topn 16470  df-0g 16488  df-gsum 16489  df-topgen 16490  df-pt 16491  df-prds 16494  df-xrs 16548  df-qtop 16553  df-imas 16554  df-xps 16556  df-mre 16632  df-mrc 16633  df-acs 16635  df-mgm 17628  df-sgrp 17670  df-mnd 17681  df-submnd 17722  df-mulg 17928  df-cntz 18133  df-cmn 18581  df-psmet 20134  df-xmet 20135  df-met 20136  df-bl 20137  df-mopn 20138  df-fbas 20139  df-fg 20140  df-cnfld 20143  df-top 21106  df-topon 21123  df-topsp 21145  df-bases 21158  df-cld 21231  df-ntr 21232  df-cls 21233  df-nei 21310  df-cn 21439  df-cnp 21440  df-lm 21441  df-haus 21527  df-tx 21774  df-hmeo 21967  df-fil 22058  df-fm 22150  df-flim 22151  df-flf 22152  df-xms 22533  df-ms 22534  df-tms 22535  df-cfil 23461  df-cau 23462  df-cmet 23463  df-grpo 27920  df-gid 27921  df-ginv 27922  df-gdiv 27923  df-ablo 27972  df-vc 27986  df-nv 28019  df-va 28022  df-ba 28023  df-sm 28024  df-0v 28025  df-vs 28026  df-nmcv 28027  df-ims 28028  df-dip 28128  df-ssp 28149  df-ph 28240  df-cbn 28291  df-hnorm 28397  df-hba 28398  df-hvsub 28400  df-hlim 28401  df-hcau 28402  df-sh 28636  df-ch 28650  df-oc 28681  df-ch0 28682  df-shs 28739  df-chj 28741  df-md 29711  df-dmd 29712
This theorem is referenced by:  mdslmd1lem4  29759
  Copyright terms: Public domain W3C validator