This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem 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 ⊢ ( 𝜑 → ( ( ⊥ ‘ ( ( ⊥ ‘ 𝑋 ) ∩ 𝑌 ) ) ∩ 𝑌 ) = ( ⊥ ‘ ( ⊥ ‘ 𝑋 ) ) )