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