Theorem osumcllem1N

Description: Lemma for osumclN . (Contributed by NM, 25-Mar-2012) (New usage is discouraged.)

	Ref	Expression
Hypotheses	osumcllem.l	⊢ ≤ = ( le ‘ 𝐾 )
	osumcllem.j	⊢ ∨ = ( join ‘ 𝐾 )
	osumcllem.a	⊢ 𝐴 = ( Atoms ‘ 𝐾 )
	osumcllem.p	⊢ + = ( +𝑃 ‘ 𝐾 )
	osumcllem.o	⊢ ⊥ = ( ⊥𝑃 ‘ 𝐾 )
	osumcllem.c	⊢ 𝐶 = ( PSubCl ‘ 𝐾 )
	osumcllem.m	⊢ 𝑀 = ( 𝑋 + { 𝑝 } )
	osumcllem.u	⊢ 𝑈 = ( ⊥ ‘ ( ⊥ ‘ ( 𝑋 + 𝑌 ) ) )
Assertion	osumcllem1N	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑋 ⊆ 𝐴 ∧ 𝑌 ⊆ 𝐴 ) ∧ 𝑝 ∈ 𝑈 ) → ( 𝑈 ∩ 𝑀 ) = 𝑀 )

Proof

Step	Hyp	Ref	Expression
1		osumcllem.l	⊢ ≤ = ( le ‘ 𝐾 )
2		osumcllem.j	⊢ ∨ = ( join ‘ 𝐾 )
3		osumcllem.a	⊢ 𝐴 = ( Atoms ‘ 𝐾 )
4		osumcllem.p	⊢ + = ( +𝑃 ‘ 𝐾 )
5		osumcllem.o	⊢ ⊥ = ( ⊥𝑃 ‘ 𝐾 )
6		osumcllem.c	⊢ 𝐶 = ( PSubCl ‘ 𝐾 )
7		osumcllem.m	⊢ 𝑀 = ( 𝑋 + { 𝑝 } )
8		osumcllem.u	⊢ 𝑈 = ( ⊥ ‘ ( ⊥ ‘ ( 𝑋 + 𝑌 ) ) )
9	3 4	sspadd1	⊢ ( ( 𝐾 ∈ HL ∧ 𝑋 ⊆ 𝐴 ∧ 𝑌 ⊆ 𝐴 ) → 𝑋 ⊆ ( 𝑋 + 𝑌 ) )
10	9	adantr	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑋 ⊆ 𝐴 ∧ 𝑌 ⊆ 𝐴 ) ∧ 𝑝 ∈ 𝑈 ) → 𝑋 ⊆ ( 𝑋 + 𝑌 ) )
11		simpl1	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑋 ⊆ 𝐴 ∧ 𝑌 ⊆ 𝐴 ) ∧ 𝑝 ∈ 𝑈 ) → 𝐾 ∈ HL )
12	3 4	paddssat	⊢ ( ( 𝐾 ∈ HL ∧ 𝑋 ⊆ 𝐴 ∧ 𝑌 ⊆ 𝐴 ) → ( 𝑋 + 𝑌 ) ⊆ 𝐴 )
13	12	adantr	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑋 ⊆ 𝐴 ∧ 𝑌 ⊆ 𝐴 ) ∧ 𝑝 ∈ 𝑈 ) → ( 𝑋 + 𝑌 ) ⊆ 𝐴 )
14	3 5	2polssN	⊢ ( ( 𝐾 ∈ HL ∧ ( 𝑋 + 𝑌 ) ⊆ 𝐴 ) → ( 𝑋 + 𝑌 ) ⊆ ( ⊥ ‘ ( ⊥ ‘ ( 𝑋 + 𝑌 ) ) ) )
15	11 13 14	syl2anc	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑋 ⊆ 𝐴 ∧ 𝑌 ⊆ 𝐴 ) ∧ 𝑝 ∈ 𝑈 ) → ( 𝑋 + 𝑌 ) ⊆ ( ⊥ ‘ ( ⊥ ‘ ( 𝑋 + 𝑌 ) ) ) )
16	15 8	sseqtrrdi	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑋 ⊆ 𝐴 ∧ 𝑌 ⊆ 𝐴 ) ∧ 𝑝 ∈ 𝑈 ) → ( 𝑋 + 𝑌 ) ⊆ 𝑈 )
17	10 16	sstrd	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑋 ⊆ 𝐴 ∧ 𝑌 ⊆ 𝐴 ) ∧ 𝑝 ∈ 𝑈 ) → 𝑋 ⊆ 𝑈 )
18		simpr	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑋 ⊆ 𝐴 ∧ 𝑌 ⊆ 𝐴 ) ∧ 𝑝 ∈ 𝑈 ) → 𝑝 ∈ 𝑈 )
19	18	snssd	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑋 ⊆ 𝐴 ∧ 𝑌 ⊆ 𝐴 ) ∧ 𝑝 ∈ 𝑈 ) → { 𝑝 } ⊆ 𝑈 )
20		simpl2	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑋 ⊆ 𝐴 ∧ 𝑌 ⊆ 𝐴 ) ∧ 𝑝 ∈ 𝑈 ) → 𝑋 ⊆ 𝐴 )
21	3 5	polssatN	⊢ ( ( 𝐾 ∈ HL ∧ ( 𝑋 + 𝑌 ) ⊆ 𝐴 ) → ( ⊥ ‘ ( 𝑋 + 𝑌 ) ) ⊆ 𝐴 )
22	11 13 21	syl2anc	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑋 ⊆ 𝐴 ∧ 𝑌 ⊆ 𝐴 ) ∧ 𝑝 ∈ 𝑈 ) → ( ⊥ ‘ ( 𝑋 + 𝑌 ) ) ⊆ 𝐴 )
23	3 5	polssatN	⊢ ( ( 𝐾 ∈ HL ∧ ( ⊥ ‘ ( 𝑋 + 𝑌 ) ) ⊆ 𝐴 ) → ( ⊥ ‘ ( ⊥ ‘ ( 𝑋 + 𝑌 ) ) ) ⊆ 𝐴 )
24	11 22 23	syl2anc	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑋 ⊆ 𝐴 ∧ 𝑌 ⊆ 𝐴 ) ∧ 𝑝 ∈ 𝑈 ) → ( ⊥ ‘ ( ⊥ ‘ ( 𝑋 + 𝑌 ) ) ) ⊆ 𝐴 )
25	8 24	eqsstrid	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑋 ⊆ 𝐴 ∧ 𝑌 ⊆ 𝐴 ) ∧ 𝑝 ∈ 𝑈 ) → 𝑈 ⊆ 𝐴 )
26	19 25	sstrd	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑋 ⊆ 𝐴 ∧ 𝑌 ⊆ 𝐴 ) ∧ 𝑝 ∈ 𝑈 ) → { 𝑝 } ⊆ 𝐴 )
27		eqid	⊢ ( PSubSp ‘ 𝐾 ) = ( PSubSp ‘ 𝐾 )
28	3 27 5	polsubN	⊢ ( ( 𝐾 ∈ HL ∧ ( ⊥ ‘ ( 𝑋 + 𝑌 ) ) ⊆ 𝐴 ) → ( ⊥ ‘ ( ⊥ ‘ ( 𝑋 + 𝑌 ) ) ) ∈ ( PSubSp ‘ 𝐾 ) )
29	11 22 28	syl2anc	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑋 ⊆ 𝐴 ∧ 𝑌 ⊆ 𝐴 ) ∧ 𝑝 ∈ 𝑈 ) → ( ⊥ ‘ ( ⊥ ‘ ( 𝑋 + 𝑌 ) ) ) ∈ ( PSubSp ‘ 𝐾 ) )
30	8 29	eqeltrid	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑋 ⊆ 𝐴 ∧ 𝑌 ⊆ 𝐴 ) ∧ 𝑝 ∈ 𝑈 ) → 𝑈 ∈ ( PSubSp ‘ 𝐾 ) )
31	3 27 4	paddss	⊢ ( ( 𝐾 ∈ HL ∧ ( 𝑋 ⊆ 𝐴 ∧ { 𝑝 } ⊆ 𝐴 ∧ 𝑈 ∈ ( PSubSp ‘ 𝐾 ) ) ) → ( ( 𝑋 ⊆ 𝑈 ∧ { 𝑝 } ⊆ 𝑈 ) ↔ ( 𝑋 + { 𝑝 } ) ⊆ 𝑈 ) )
32	11 20 26 30 31	syl13anc	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑋 ⊆ 𝐴 ∧ 𝑌 ⊆ 𝐴 ) ∧ 𝑝 ∈ 𝑈 ) → ( ( 𝑋 ⊆ 𝑈 ∧ { 𝑝 } ⊆ 𝑈 ) ↔ ( 𝑋 + { 𝑝 } ) ⊆ 𝑈 ) )
33	17 19 32	mpbi2and	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑋 ⊆ 𝐴 ∧ 𝑌 ⊆ 𝐴 ) ∧ 𝑝 ∈ 𝑈 ) → ( 𝑋 + { 𝑝 } ) ⊆ 𝑈 )
34	7 33	eqsstrid	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑋 ⊆ 𝐴 ∧ 𝑌 ⊆ 𝐴 ) ∧ 𝑝 ∈ 𝑈 ) → 𝑀 ⊆ 𝑈 )
35		sseqin2	⊢ ( 𝑀 ⊆ 𝑈 ↔ ( 𝑈 ∩ 𝑀 ) = 𝑀 )
36	34 35	sylib	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑋 ⊆ 𝐴 ∧ 𝑌 ⊆ 𝐴 ) ∧ 𝑝 ∈ 𝑈 ) → ( 𝑈 ∩ 𝑀 ) = 𝑀 )