dihoml4

Description: Orthomodular law for constructed vector space H. Lemma 3.3(1) in Holland95 p. 215. ( poml4N analog.) (Contributed by NM, 15-Jan-2015)

	Ref	Expression
Hypotheses	dihoml4.h	⊢ 𝐻 = ( LHyp ‘ 𝐾 )
	dihoml4.u	⊢ 𝑈 = ( ( DVecH ‘ 𝐾 ) ‘ 𝑊 )
	dihoml4.s	⊢ 𝑆 = ( LSubSp ‘ 𝑈 )
	dihoml4.o	⊢ ⊥ = ( ( ocH ‘ 𝐾 ) ‘ 𝑊 )
	dihoml4.k	⊢ ( 𝜑 → ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) )
	dihoml4.x	⊢ ( 𝜑 → 𝑋 ∈ 𝑆 )
	dihoml4.y	⊢ ( 𝜑 → 𝑌 ∈ 𝑆 )
	dihoml4.c	⊢ ( 𝜑 → ( ⊥ ‘ ( ⊥ ‘ 𝑌 ) ) = 𝑌 )
	dihoml4.l	⊢ ( 𝜑 → 𝑋 ⊆ 𝑌 )
Assertion	dihoml4	⊢ ( 𝜑 → ( ( ⊥ ‘ ( ( ⊥ ‘ 𝑋 ) ∩ 𝑌 ) ) ∩ 𝑌 ) = ( ⊥ ‘ ( ⊥ ‘ 𝑋 ) ) )

Proof

Step	Hyp	Ref	Expression
1		dihoml4.h	⊢ 𝐻 = ( LHyp ‘ 𝐾 )
2		dihoml4.u	⊢ 𝑈 = ( ( DVecH ‘ 𝐾 ) ‘ 𝑊 )
3		dihoml4.s	⊢ 𝑆 = ( LSubSp ‘ 𝑈 )
4		dihoml4.o	⊢ ⊥ = ( ( ocH ‘ 𝐾 ) ‘ 𝑊 )
5		dihoml4.k	⊢ ( 𝜑 → ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) )
6		dihoml4.x	⊢ ( 𝜑 → 𝑋 ∈ 𝑆 )
7		dihoml4.y	⊢ ( 𝜑 → 𝑌 ∈ 𝑆 )
8		dihoml4.c	⊢ ( 𝜑 → ( ⊥ ‘ ( ⊥ ‘ 𝑌 ) ) = 𝑌 )
9		dihoml4.l	⊢ ( 𝜑 → 𝑋 ⊆ 𝑌 )
10		eqid	⊢ ( Base ‘ 𝑈 ) = ( Base ‘ 𝑈 )
11	10 3	lssss	⊢ ( 𝑋 ∈ 𝑆 → 𝑋 ⊆ ( Base ‘ 𝑈 ) )
12	6 11	syl	⊢ ( 𝜑 → 𝑋 ⊆ ( Base ‘ 𝑈 ) )
13		eqid	⊢ ( ( DIsoH ‘ 𝐾 ) ‘ 𝑊 ) = ( ( DIsoH ‘ 𝐾 ) ‘ 𝑊 )
14	1 13 2 10 4	dochcl	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝑋 ⊆ ( Base ‘ 𝑈 ) ) → ( ⊥ ‘ 𝑋 ) ∈ ran ( ( DIsoH ‘ 𝐾 ) ‘ 𝑊 ) )
15	5 12 14	syl2anc	⊢ ( 𝜑 → ( ⊥ ‘ 𝑋 ) ∈ ran ( ( DIsoH ‘ 𝐾 ) ‘ 𝑊 ) )
16	1 13 4	dochoc	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( ⊥ ‘ 𝑋 ) ∈ ran ( ( DIsoH ‘ 𝐾 ) ‘ 𝑊 ) ) → ( ⊥ ‘ ( ⊥ ‘ ( ⊥ ‘ 𝑋 ) ) ) = ( ⊥ ‘ 𝑋 ) )
17	5 15 16	syl2anc	⊢ ( 𝜑 → ( ⊥ ‘ ( ⊥ ‘ ( ⊥ ‘ 𝑋 ) ) ) = ( ⊥ ‘ 𝑋 ) )
18	17	ineq1d	⊢ ( 𝜑 → ( ( ⊥ ‘ ( ⊥ ‘ ( ⊥ ‘ 𝑋 ) ) ) ∩ 𝑌 ) = ( ( ⊥ ‘ 𝑋 ) ∩ 𝑌 ) )
19	18	fveq2d	⊢ ( 𝜑 → ( ⊥ ‘ ( ( ⊥ ‘ ( ⊥ ‘ ( ⊥ ‘ 𝑋 ) ) ) ∩ 𝑌 ) ) = ( ⊥ ‘ ( ( ⊥ ‘ 𝑋 ) ∩ 𝑌 ) ) )
20	19	ineq1d	⊢ ( 𝜑 → ( ( ⊥ ‘ ( ( ⊥ ‘ ( ⊥ ‘ ( ⊥ ‘ 𝑋 ) ) ) ∩ 𝑌 ) ) ∩ 𝑌 ) = ( ( ⊥ ‘ ( ( ⊥ ‘ 𝑋 ) ∩ 𝑌 ) ) ∩ 𝑌 ) )
21	1 2 10 4	dochssv	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝑋 ⊆ ( Base ‘ 𝑈 ) ) → ( ⊥ ‘ 𝑋 ) ⊆ ( Base ‘ 𝑈 ) )
22	5 12 21	syl2anc	⊢ ( 𝜑 → ( ⊥ ‘ 𝑋 ) ⊆ ( Base ‘ 𝑈 ) )
23	1 13 2 10 4	dochcl	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( ⊥ ‘ 𝑋 ) ⊆ ( Base ‘ 𝑈 ) ) → ( ⊥ ‘ ( ⊥ ‘ 𝑋 ) ) ∈ ran ( ( DIsoH ‘ 𝐾 ) ‘ 𝑊 ) )
24	5 22 23	syl2anc	⊢ ( 𝜑 → ( ⊥ ‘ ( ⊥ ‘ 𝑋 ) ) ∈ ran ( ( DIsoH ‘ 𝐾 ) ‘ 𝑊 ) )
25	10 3	lssss	⊢ ( 𝑌 ∈ 𝑆 → 𝑌 ⊆ ( Base ‘ 𝑈 ) )
26	7 25	syl	⊢ ( 𝜑 → 𝑌 ⊆ ( Base ‘ 𝑈 ) )
27	1 13 2 10 4 5 26	dochoccl	⊢ ( 𝜑 → ( 𝑌 ∈ ran ( ( DIsoH ‘ 𝐾 ) ‘ 𝑊 ) ↔ ( ⊥ ‘ ( ⊥ ‘ 𝑌 ) ) = 𝑌 ) )
28	8 27	mpbird	⊢ ( 𝜑 → 𝑌 ∈ ran ( ( DIsoH ‘ 𝐾 ) ‘ 𝑊 ) )
29	1 2 10 4	dochss	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝑌 ⊆ ( Base ‘ 𝑈 ) ∧ 𝑋 ⊆ 𝑌 ) → ( ⊥ ‘ 𝑌 ) ⊆ ( ⊥ ‘ 𝑋 ) )
30	5 26 9 29	syl3anc	⊢ ( 𝜑 → ( ⊥ ‘ 𝑌 ) ⊆ ( ⊥ ‘ 𝑋 ) )
31	1 2 10 4	dochss	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( ⊥ ‘ 𝑋 ) ⊆ ( Base ‘ 𝑈 ) ∧ ( ⊥ ‘ 𝑌 ) ⊆ ( ⊥ ‘ 𝑋 ) ) → ( ⊥ ‘ ( ⊥ ‘ 𝑋 ) ) ⊆ ( ⊥ ‘ ( ⊥ ‘ 𝑌 ) ) )
32	5 22 30 31	syl3anc	⊢ ( 𝜑 → ( ⊥ ‘ ( ⊥ ‘ 𝑋 ) ) ⊆ ( ⊥ ‘ ( ⊥ ‘ 𝑌 ) ) )
33	32 8	sseqtrd	⊢ ( 𝜑 → ( ⊥ ‘ ( ⊥ ‘ 𝑋 ) ) ⊆ 𝑌 )
34	1 13 4 5 24 28 33	dihoml4c	⊢ ( 𝜑 → ( ( ⊥ ‘ ( ( ⊥ ‘ ( ⊥ ‘ ( ⊥ ‘ 𝑋 ) ) ) ∩ 𝑌 ) ) ∩ 𝑌 ) = ( ⊥ ‘ ( ⊥ ‘ 𝑋 ) ) )
35	20 34	eqtr3d	⊢ ( 𝜑 → ( ( ⊥ ‘ ( ( ⊥ ‘ 𝑋 ) ∩ 𝑌 ) ) ∩ 𝑌 ) = ( ⊥ ‘ ( ⊥ ‘ 𝑋 ) ) )

Metamath Proof Explorer

Theorem dihoml4

Proof