cdlemn11c - Mathbox for Norm Megill

	Mathbox for Norm Megill		< Previous Next > Nearby theorems
Mirrors > Home > MPE Home > Th. List > Mathboxes > cdlemn11c		Structured version Visualization version GIF version

Theorem cdlemn11c 38846

Description: Part of proof of Lemma N of [Crawley] p. 121 line 37. (Contributed by NM, 27-Feb-2014.)

**Hypotheses**
Ref	Expression
cdlemn11a.b	⊢ 𝐵 = (Base‘𝐾)
cdlemn11a.l	⊢ ≤ = (le‘𝐾)
cdlemn11a.j	⊢ ∨ = (join‘𝐾)
cdlemn11a.a	⊢ 𝐴 = (Atoms‘𝐾)
cdlemn11a.h	⊢ 𝐻 = (LHyp‘𝐾)
cdlemn11a.p	⊢ 𝑃 = ((oc‘𝐾)‘𝑊)
cdlemn11a.o	⊢ 𝑂 = (ℎ ∈ 𝑇 ↦ ( I ↾ 𝐵))
cdlemn11a.t	⊢ 𝑇 = ((LTrn‘𝐾)‘𝑊)
cdlemn11a.r	⊢ 𝑅 = ((trL‘𝐾)‘𝑊)
cdlemn11a.e	⊢ 𝐸 = ((TEndo‘𝐾)‘𝑊)
cdlemn11a.i	⊢ 𝐼 = ((DIsoB‘𝐾)‘𝑊)
cdlemn11a.J	⊢ 𝐽 = ((DIsoC‘𝐾)‘𝑊)
cdlemn11a.u	⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊)
cdlemn11a.d	⊢ + = (+_g‘𝑈)
cdlemn11a.s	⊢ ⊕ = (LSSum‘𝑈)
cdlemn11a.f	⊢ 𝐹 = (℩ℎ ∈ 𝑇 (ℎ‘𝑃) = 𝑄)
cdlemn11a.g	⊢ 𝐺 = (℩ℎ ∈ 𝑇 (ℎ‘𝑃) = 𝑁)

**Assertion**
Ref	Expression
cdlemn11c	⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ ((𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ (𝑁 ∈ 𝐴 ∧ ¬ 𝑁 ≤ 𝑊) ∧ (𝑋 ∈ 𝐵 ∧ 𝑋 ≤ 𝑊)) ∧ (𝐽‘𝑁) ⊆ ((𝐽‘𝑄) ⊕ (𝐼‘𝑋))) → ∃𝑦 ∈ (𝐽‘𝑄)∃𝑧 ∈ (𝐼‘𝑋)⟨𝐺, ( I ↾ 𝑇)⟩ = (𝑦 + 𝑧))

Distinct variable groups: 𝑦,𝑧, + 𝑦, ∨ ,𝑧 𝑦,ℎ,𝑧, ≤ 𝐴,ℎ,𝑦,𝑧 𝐵,ℎ,𝑦,𝑧 𝑦,𝐺,𝑧 𝑦,𝐼,𝑧 𝑦, ⊕ ,𝑧 ℎ,𝐻,𝑦,𝑧 ℎ,𝐾,𝑦,𝑧 ℎ,𝑁,𝑦,𝑧 𝑦,𝐽,𝑧 𝑃,ℎ 𝑄,ℎ,𝑦,𝑧 𝑇,ℎ,𝑦,𝑧 𝑦,𝑈,𝑧 ℎ,𝑊,𝑦,𝑧 𝑦,𝑋,𝑧 Allowed substitution hints: 𝑃(𝑦,𝑧) + (ℎ) ⊕ (ℎ) 𝑅(𝑦,𝑧,ℎ) 𝑈(ℎ) 𝐸(𝑦,𝑧,ℎ) 𝐹(𝑦,𝑧,ℎ) 𝐺(ℎ) 𝐼(ℎ) 𝐽(ℎ) ∨ (ℎ) 𝑂(𝑦,𝑧,ℎ) 𝑋(ℎ)

**Proof of Theorem cdlemn11c**
Step	Hyp	Ref	Expression
1		cdlemn11a.b	. . 3 ⊢ 𝐵 = (Base‘𝐾)
2		cdlemn11a.l	. . 3 ⊢ ≤ = (le‘𝐾)
3		cdlemn11a.j	. . 3 ⊢ ∨ = (join‘𝐾)
4		cdlemn11a.a	. . 3 ⊢ 𝐴 = (Atoms‘𝐾)
5		cdlemn11a.h	. . 3 ⊢ 𝐻 = (LHyp‘𝐾)
6		cdlemn11a.p	. . 3 ⊢ 𝑃 = ((oc‘𝐾)‘𝑊)
7		cdlemn11a.o	. . 3 ⊢ 𝑂 = (ℎ ∈ 𝑇 ↦ ( I ↾ 𝐵))
8		cdlemn11a.t	. . 3 ⊢ 𝑇 = ((LTrn‘𝐾)‘𝑊)
9		cdlemn11a.r	. . 3 ⊢ 𝑅 = ((trL‘𝐾)‘𝑊)
10		cdlemn11a.e	. . 3 ⊢ 𝐸 = ((TEndo‘𝐾)‘𝑊)
11		cdlemn11a.i	. . 3 ⊢ 𝐼 = ((DIsoB‘𝐾)‘𝑊)
12		cdlemn11a.J	. . 3 ⊢ 𝐽 = ((DIsoC‘𝐾)‘𝑊)
13		cdlemn11a.u	. . 3 ⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊)
14		cdlemn11a.d	. . 3 ⊢ + = (+_g‘𝑈)
15		cdlemn11a.s	. . 3 ⊢ ⊕ = (LSSum‘𝑈)
16		cdlemn11a.f	. . 3 ⊢ 𝐹 = (℩ℎ ∈ 𝑇 (ℎ‘𝑃) = 𝑄)
17		cdlemn11a.g	. . 3 ⊢ 𝐺 = (℩ℎ ∈ 𝑇 (ℎ‘𝑃) = 𝑁)
18	1, 2, 3, 4, 5, 6, 7, 8, 9, 10, 11, 12, 13, 14, 15, 16, 17	cdlemn11b 38845	. 2 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ ((𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ (𝑁 ∈ 𝐴 ∧ ¬ 𝑁 ≤ 𝑊) ∧ (𝑋 ∈ 𝐵 ∧ 𝑋 ≤ 𝑊)) ∧ (𝐽‘𝑁) ⊆ ((𝐽‘𝑄) ⊕ (𝐼‘𝑋))) → ⟨𝐺, ( I ↾ 𝑇)⟩ ∈ ((𝐽‘𝑄) ⊕ (𝐼‘𝑋)))
19		simp1 1137	. . . . . 6 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ ((𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ (𝑁 ∈ 𝐴 ∧ ¬ 𝑁 ≤ 𝑊) ∧ (𝑋 ∈ 𝐵 ∧ 𝑋 ≤ 𝑊)) ∧ (𝐽‘𝑁) ⊆ ((𝐽‘𝑄) ⊕ (𝐼‘𝑋))) → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻))
20	5, 13, 19	dvhlmod 38747	. . . . 5 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ ((𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ (𝑁 ∈ 𝐴 ∧ ¬ 𝑁 ≤ 𝑊) ∧ (𝑋 ∈ 𝐵 ∧ 𝑋 ≤ 𝑊)) ∧ (𝐽‘𝑁) ⊆ ((𝐽‘𝑄) ⊕ (𝐼‘𝑋))) → 𝑈 ∈ LMod)
21		eqid 2738	. . . . . 6 ⊢ (LSubSp‘𝑈) = (LSubSp‘𝑈)
22	21	lsssssubg 19849	. . . . 5 ⊢ (𝑈 ∈ LMod → (LSubSp‘𝑈) ⊆ (SubGrp‘𝑈))
23	20, 22	syl 17	. . . 4 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ ((𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ (𝑁 ∈ 𝐴 ∧ ¬ 𝑁 ≤ 𝑊) ∧ (𝑋 ∈ 𝐵 ∧ 𝑋 ≤ 𝑊)) ∧ (𝐽‘𝑁) ⊆ ((𝐽‘𝑄) ⊕ (𝐼‘𝑋))) → (LSubSp‘𝑈) ⊆ (SubGrp‘𝑈))
24		simp21 1207	. . . . 5 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ ((𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ (𝑁 ∈ 𝐴 ∧ ¬ 𝑁 ≤ 𝑊) ∧ (𝑋 ∈ 𝐵 ∧ 𝑋 ≤ 𝑊)) ∧ (𝐽‘𝑁) ⊆ ((𝐽‘𝑄) ⊕ (𝐼‘𝑋))) → (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊))
25	2, 4, 5, 13, 12, 21	diclss 38830	. . . . 5 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊)) → (𝐽‘𝑄) ∈ (LSubSp‘𝑈))
26	19, 24, 25	syl2anc 587	. . . 4 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ ((𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ (𝑁 ∈ 𝐴 ∧ ¬ 𝑁 ≤ 𝑊) ∧ (𝑋 ∈ 𝐵 ∧ 𝑋 ≤ 𝑊)) ∧ (𝐽‘𝑁) ⊆ ((𝐽‘𝑄) ⊕ (𝐼‘𝑋))) → (𝐽‘𝑄) ∈ (LSubSp‘𝑈))
27	23, 26	sseldd 3878	. . 3 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ ((𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ (𝑁 ∈ 𝐴 ∧ ¬ 𝑁 ≤ 𝑊) ∧ (𝑋 ∈ 𝐵 ∧ 𝑋 ≤ 𝑊)) ∧ (𝐽‘𝑁) ⊆ ((𝐽‘𝑄) ⊕ (𝐼‘𝑋))) → (𝐽‘𝑄) ∈ (SubGrp‘𝑈))
28		simp23l 1295	. . . . 5 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ ((𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ (𝑁 ∈ 𝐴 ∧ ¬ 𝑁 ≤ 𝑊) ∧ (𝑋 ∈ 𝐵 ∧ 𝑋 ≤ 𝑊)) ∧ (𝐽‘𝑁) ⊆ ((𝐽‘𝑄) ⊕ (𝐼‘𝑋))) → 𝑋 ∈ 𝐵)
29		simp23r 1296	. . . . 5 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ ((𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ (𝑁 ∈ 𝐴 ∧ ¬ 𝑁 ≤ 𝑊) ∧ (𝑋 ∈ 𝐵 ∧ 𝑋 ≤ 𝑊)) ∧ (𝐽‘𝑁) ⊆ ((𝐽‘𝑄) ⊕ (𝐼‘𝑋))) → 𝑋 ≤ 𝑊)
30	1, 2, 5, 13, 11, 21	diblss 38807	. . . . 5 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ 𝑋 ≤ 𝑊)) → (𝐼‘𝑋) ∈ (LSubSp‘𝑈))
31	19, 28, 29, 30	syl12anc 836	. . . 4 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ ((𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ (𝑁 ∈ 𝐴 ∧ ¬ 𝑁 ≤ 𝑊) ∧ (𝑋 ∈ 𝐵 ∧ 𝑋 ≤ 𝑊)) ∧ (𝐽‘𝑁) ⊆ ((𝐽‘𝑄) ⊕ (𝐼‘𝑋))) → (𝐼‘𝑋) ∈ (LSubSp‘𝑈))
32	23, 31	sseldd 3878	. . 3 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ ((𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ (𝑁 ∈ 𝐴 ∧ ¬ 𝑁 ≤ 𝑊) ∧ (𝑋 ∈ 𝐵 ∧ 𝑋 ≤ 𝑊)) ∧ (𝐽‘𝑁) ⊆ ((𝐽‘𝑄) ⊕ (𝐼‘𝑋))) → (𝐼‘𝑋) ∈ (SubGrp‘𝑈))
33	14, 15	lsmelval 18892	. . 3 ⊢ (((𝐽‘𝑄) ∈ (SubGrp‘𝑈) ∧ (𝐼‘𝑋) ∈ (SubGrp‘𝑈)) → (⟨𝐺, ( I ↾ 𝑇)⟩ ∈ ((𝐽‘𝑄) ⊕ (𝐼‘𝑋)) ↔ ∃𝑦 ∈ (𝐽‘𝑄)∃𝑧 ∈ (𝐼‘𝑋)⟨𝐺, ( I ↾ 𝑇)⟩ = (𝑦 + 𝑧)))
34	27, 32, 33	syl2anc 587	. 2 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ ((𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ (𝑁 ∈ 𝐴 ∧ ¬ 𝑁 ≤ 𝑊) ∧ (𝑋 ∈ 𝐵 ∧ 𝑋 ≤ 𝑊)) ∧ (𝐽‘𝑁) ⊆ ((𝐽‘𝑄) ⊕ (𝐼‘𝑋))) → (⟨𝐺, ( I ↾ 𝑇)⟩ ∈ ((𝐽‘𝑄) ⊕ (𝐼‘𝑋)) ↔ ∃𝑦 ∈ (𝐽‘𝑄)∃𝑧 ∈ (𝐼‘𝑋)⟨𝐺, ( I ↾ 𝑇)⟩ = (𝑦 + 𝑧)))
35	18, 34	mpbid 235	1 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ ((𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ (𝑁 ∈ 𝐴 ∧ ¬ 𝑁 ≤ 𝑊) ∧ (𝑋 ∈ 𝐵 ∧ 𝑋 ≤ 𝑊)) ∧ (𝐽‘𝑁) ⊆ ((𝐽‘𝑄) ⊕ (𝐼‘𝑋))) → ∃𝑦 ∈ (𝐽‘𝑄)∃𝑧 ∈ (𝐼‘𝑋)⟨𝐺, ( I ↾ 𝑇)⟩ = (𝑦 + 𝑧))

Colors of variables: wff setvar class

Syntax hints: ¬ wn 3 → wi 4 ↔ wb 209 ∧ wa 399 ∧ w3a 1088 = wceq 1542 ∈ wcel 2114 ∃wrex 3054 ⊆ wss 3843 ⟨cop 4522 class class class wbr 5030 ↦ cmpt 5110 I cid 5428 ↾ cres 5527 ‘cfv 6339 ℩crio 7126 (class class class)co 7170 Basecbs 16586 +_gcplusg 16668 lecple 16675 occoc 16676 joincjn 17670 SubGrpcsubg 18391 LSSumclsm 18877 LModclmod 19753 LSubSpclss 19822 Atomscatm 36900 HLchlt 36987 LHypclh 37621 LTrncltrn 37738 trLctrl 37795 TEndoctendo 38389 DVecHcdvh 38715 DIsoBcdib 38775 DIsoCcdic 38809

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 1975 ax-7 2020 ax-8 2116 ax-9 2124 ax-10 2145 ax-11 2162 ax-12 2179 ax-ext 2710 ax-rep 5154 ax-sep 5167 ax-nul 5174 ax-pow 5232 ax-pr 5296 ax-un 7479 ax-cnex 10671 ax-resscn 10672 ax-1cn 10673 ax-icn 10674 ax-addcl 10675 ax-addrcl 10676 ax-mulcl 10677 ax-mulrcl 10678 ax-mulcom 10679 ax-addass 10680 ax-mulass 10681 ax-distr 10682 ax-i2m1 10683 ax-1ne0 10684 ax-1rid 10685 ax-rnegex 10686 ax-rrecex 10687 ax-cnre 10688 ax-pre-lttri 10689 ax-pre-lttrn 10690 ax-pre-ltadd 10691 ax-pre-mulgt0 10692 ax-riotaBAD 36590

This theorem depends on definitions: df-bi 210 df-an 400 df-or 847 df-3or 1089 df-3an 1090 df-tru 1545 df-fal 1555 df-ex 1787 df-nf 1791 df-sb 2075 df-mo 2540 df-eu 2570 df-clab 2717 df-cleq 2730 df-clel 2811 df-nfc 2881 df-ne 2935 df-nel 3039 df-ral 3058 df-rex 3059 df-reu 3060 df-rmo 3061 df-rab 3062 df-v 3400 df-sbc 3681 df-csb 3791 df-dif 3846 df-un 3848 df-in 3850 df-ss 3860 df-pss 3862 df-nul 4212 df-if 4415 df-pw 4490 df-sn 4517 df-pr 4519 df-tp 4521 df-op 4523 df-uni 4797 df-iun 4883 df-iin 4884 df-br 5031 df-opab 5093 df-mpt 5111 df-tr 5137 df-id 5429 df-eprel 5434 df-po 5442 df-so 5443 df-fr 5483 df-we 5485 df-xp 5531 df-rel 5532 df-cnv 5533 df-co 5534 df-dm 5535 df-rn 5536 df-res 5537 df-ima 5538 df-pred 6129 df-ord 6175 df-on 6176 df-lim 6177 df-suc 6178 df-iota 6297 df-fun 6341 df-fn 6342 df-f 6343 df-f1 6344 df-fo 6345 df-f1o 6346 df-fv 6347 df-riota 7127 df-ov 7173 df-oprab 7174 df-mpo 7175 df-om 7600 df-1st 7714 df-2nd 7715 df-tpos 7921 df-undef 7968 df-wrecs 7976 df-recs 8037 df-rdg 8075 df-1o 8131 df-er 8320 df-map 8439 df-en 8556 df-dom 8557 df-sdom 8558 df-fin 8559 df-pnf 10755 df-mnf 10756 df-xr 10757 df-ltxr 10758 df-le 10759 df-sub 10950 df-neg 10951 df-nn 11717 df-2 11779 df-3 11780 df-4 11781 df-5 11782 df-6 11783 df-n0 11977 df-z 12063 df-uz 12325 df-fz 12982 df-struct 16588 df-ndx 16589 df-slot 16590 df-base 16592 df-sets 16593 df-ress 16594 df-plusg 16681 df-mulr 16682 df-sca 16684 df-vsca 16685 df-0g 16818 df-proset 17654 df-poset 17672 df-plt 17684 df-lub 17700 df-glb 17701 df-join 17702 df-meet 17703 df-p0 17765 df-p1 17766 df-lat 17772 df-clat 17834 df-mgm 17968 df-sgrp 18017 df-mnd 18028 df-grp 18222 df-minusg 18223 df-sbg 18224 df-subg 18394 df-lsm 18879 df-mgp 19359 df-ur 19371 df-ring 19418 df-oppr 19495 df-dvdsr 19513 df-unit 19514 df-invr 19544 df-dvr 19555 df-drng 19623 df-lmod 19755 df-lss 19823 df-lvec 19994 df-oposet 36813 df-ol 36815 df-oml 36816 df-covers 36903 df-ats 36904 df-atl 36935 df-cvlat 36959 df-hlat 36988 df-llines 37135 df-lplanes 37136 df-lvols 37137 df-lines 37138 df-psubsp 37140 df-pmap 37141 df-padd 37433 df-lhyp 37625 df-laut 37626 df-ldil 37741 df-ltrn 37742 df-trl 37796 df-tendo 38392 df-edring 38394 df-disoa 38666 df-dvech 38716 df-dib 38776 df-dic 38810

This theorem is referenced by: cdlemn11pre 38847

W3C validator