Metamath Proof Explorer


Theorem dochdmj1

Description: De Morgan-like law for subspace orthocomplement. (Contributed by NM, 5-Aug-2014)

Ref Expression
Hypotheses dochdmj1.h 𝐻 = ( LHyp ‘ 𝐾 )
dochdmj1.u 𝑈 = ( ( DVecH ‘ 𝐾 ) ‘ 𝑊 )
dochdmj1.v 𝑉 = ( Base ‘ 𝑈 )
dochdmj1.o = ( ( ocH ‘ 𝐾 ) ‘ 𝑊 )
Assertion dochdmj1 ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ 𝑋𝑉𝑌𝑉 ) → ( ‘ ( 𝑋𝑌 ) ) = ( ( 𝑋 ) ∩ ( 𝑌 ) ) )

Proof

Step Hyp Ref Expression
1 dochdmj1.h 𝐻 = ( LHyp ‘ 𝐾 )
2 dochdmj1.u 𝑈 = ( ( DVecH ‘ 𝐾 ) ‘ 𝑊 )
3 dochdmj1.v 𝑉 = ( Base ‘ 𝑈 )
4 dochdmj1.o = ( ( ocH ‘ 𝐾 ) ‘ 𝑊 )
5 simp1 ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ 𝑋𝑉𝑌𝑉 ) → ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) )
6 simp2 ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ 𝑋𝑉𝑌𝑉 ) → 𝑋𝑉 )
7 simp3 ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ 𝑋𝑉𝑌𝑉 ) → 𝑌𝑉 )
8 6 7 unssd ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ 𝑋𝑉𝑌𝑉 ) → ( 𝑋𝑌 ) ⊆ 𝑉 )
9 ssun1 𝑋 ⊆ ( 𝑋𝑌 )
10 9 a1i ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ 𝑋𝑉𝑌𝑉 ) → 𝑋 ⊆ ( 𝑋𝑌 ) )
11 1 2 3 4 dochss ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( 𝑋𝑌 ) ⊆ 𝑉𝑋 ⊆ ( 𝑋𝑌 ) ) → ( ‘ ( 𝑋𝑌 ) ) ⊆ ( 𝑋 ) )
12 5 8 10 11 syl3anc ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ 𝑋𝑉𝑌𝑉 ) → ( ‘ ( 𝑋𝑌 ) ) ⊆ ( 𝑋 ) )
13 ssun2 𝑌 ⊆ ( 𝑋𝑌 )
14 13 a1i ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ 𝑋𝑉𝑌𝑉 ) → 𝑌 ⊆ ( 𝑋𝑌 ) )
15 1 2 3 4 dochss ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( 𝑋𝑌 ) ⊆ 𝑉𝑌 ⊆ ( 𝑋𝑌 ) ) → ( ‘ ( 𝑋𝑌 ) ) ⊆ ( 𝑌 ) )
16 5 8 14 15 syl3anc ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ 𝑋𝑉𝑌𝑉 ) → ( ‘ ( 𝑋𝑌 ) ) ⊆ ( 𝑌 ) )
17 12 16 ssind ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ 𝑋𝑉𝑌𝑉 ) → ( ‘ ( 𝑋𝑌 ) ) ⊆ ( ( 𝑋 ) ∩ ( 𝑌 ) ) )
18 eqid ( ( DIsoH ‘ 𝐾 ) ‘ 𝑊 ) = ( ( DIsoH ‘ 𝐾 ) ‘ 𝑊 )
19 1 18 2 3 4 dochcl ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ 𝑋𝑉 ) → ( 𝑋 ) ∈ ran ( ( DIsoH ‘ 𝐾 ) ‘ 𝑊 ) )
20 19 3adant3 ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ 𝑋𝑉𝑌𝑉 ) → ( 𝑋 ) ∈ ran ( ( DIsoH ‘ 𝐾 ) ‘ 𝑊 ) )
21 1 18 2 3 4 dochcl ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ 𝑌𝑉 ) → ( 𝑌 ) ∈ ran ( ( DIsoH ‘ 𝐾 ) ‘ 𝑊 ) )
22 21 3adant2 ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ 𝑋𝑉𝑌𝑉 ) → ( 𝑌 ) ∈ ran ( ( DIsoH ‘ 𝐾 ) ‘ 𝑊 ) )
23 1 18 dihmeetcl ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( ( 𝑋 ) ∈ ran ( ( DIsoH ‘ 𝐾 ) ‘ 𝑊 ) ∧ ( 𝑌 ) ∈ ran ( ( DIsoH ‘ 𝐾 ) ‘ 𝑊 ) ) ) → ( ( 𝑋 ) ∩ ( 𝑌 ) ) ∈ ran ( ( DIsoH ‘ 𝐾 ) ‘ 𝑊 ) )
24 5 20 22 23 syl12anc ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ 𝑋𝑉𝑌𝑉 ) → ( ( 𝑋 ) ∩ ( 𝑌 ) ) ∈ ran ( ( DIsoH ‘ 𝐾 ) ‘ 𝑊 ) )
25 1 18 4 dochoc ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( ( 𝑋 ) ∩ ( 𝑌 ) ) ∈ ran ( ( DIsoH ‘ 𝐾 ) ‘ 𝑊 ) ) → ( ‘ ( ‘ ( ( 𝑋 ) ∩ ( 𝑌 ) ) ) ) = ( ( 𝑋 ) ∩ ( 𝑌 ) ) )
26 5 24 25 syl2anc ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ 𝑋𝑉𝑌𝑉 ) → ( ‘ ( ‘ ( ( 𝑋 ) ∩ ( 𝑌 ) ) ) ) = ( ( 𝑋 ) ∩ ( 𝑌 ) ) )
27 1 2 3 4 dochssv ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ 𝑋𝑉 ) → ( 𝑋 ) ⊆ 𝑉 )
28 27 3adant3 ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ 𝑋𝑉𝑌𝑉 ) → ( 𝑋 ) ⊆ 𝑉 )
29 ssinss1 ( ( 𝑋 ) ⊆ 𝑉 → ( ( 𝑋 ) ∩ ( 𝑌 ) ) ⊆ 𝑉 )
30 28 29 syl ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ 𝑋𝑉𝑌𝑉 ) → ( ( 𝑋 ) ∩ ( 𝑌 ) ) ⊆ 𝑉 )
31 1 2 3 4 dochssv ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( ( 𝑋 ) ∩ ( 𝑌 ) ) ⊆ 𝑉 ) → ( ‘ ( ( 𝑋 ) ∩ ( 𝑌 ) ) ) ⊆ 𝑉 )
32 5 30 31 syl2anc ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ 𝑋𝑉𝑌𝑉 ) → ( ‘ ( ( 𝑋 ) ∩ ( 𝑌 ) ) ) ⊆ 𝑉 )
33 1 2 3 4 dochocss ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ 𝑋𝑉 ) → 𝑋 ⊆ ( ‘ ( 𝑋 ) ) )
34 33 3adant3 ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ 𝑋𝑉𝑌𝑉 ) → 𝑋 ⊆ ( ‘ ( 𝑋 ) ) )
35 1 2 3 4 dochocss ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ 𝑌𝑉 ) → 𝑌 ⊆ ( ‘ ( 𝑌 ) ) )
36 35 3adant2 ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ 𝑋𝑉𝑌𝑉 ) → 𝑌 ⊆ ( ‘ ( 𝑌 ) ) )
37 unss12 ( ( 𝑋 ⊆ ( ‘ ( 𝑋 ) ) ∧ 𝑌 ⊆ ( ‘ ( 𝑌 ) ) ) → ( 𝑋𝑌 ) ⊆ ( ( ‘ ( 𝑋 ) ) ∪ ( ‘ ( 𝑌 ) ) ) )
38 34 36 37 syl2anc ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ 𝑋𝑉𝑌𝑉 ) → ( 𝑋𝑌 ) ⊆ ( ( ‘ ( 𝑋 ) ) ∪ ( ‘ ( 𝑌 ) ) ) )
39 inss1 ( ( 𝑋 ) ∩ ( 𝑌 ) ) ⊆ ( 𝑋 )
40 39 a1i ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ 𝑋𝑉𝑌𝑉 ) → ( ( 𝑋 ) ∩ ( 𝑌 ) ) ⊆ ( 𝑋 ) )
41 1 2 3 4 dochss ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( 𝑋 ) ⊆ 𝑉 ∧ ( ( 𝑋 ) ∩ ( 𝑌 ) ) ⊆ ( 𝑋 ) ) → ( ‘ ( 𝑋 ) ) ⊆ ( ‘ ( ( 𝑋 ) ∩ ( 𝑌 ) ) ) )
42 5 28 40 41 syl3anc ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ 𝑋𝑉𝑌𝑉 ) → ( ‘ ( 𝑋 ) ) ⊆ ( ‘ ( ( 𝑋 ) ∩ ( 𝑌 ) ) ) )
43 1 2 3 4 dochssv ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ 𝑌𝑉 ) → ( 𝑌 ) ⊆ 𝑉 )
44 43 3adant2 ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ 𝑋𝑉𝑌𝑉 ) → ( 𝑌 ) ⊆ 𝑉 )
45 inss2 ( ( 𝑋 ) ∩ ( 𝑌 ) ) ⊆ ( 𝑌 )
46 45 a1i ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ 𝑋𝑉𝑌𝑉 ) → ( ( 𝑋 ) ∩ ( 𝑌 ) ) ⊆ ( 𝑌 ) )
47 1 2 3 4 dochss ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( 𝑌 ) ⊆ 𝑉 ∧ ( ( 𝑋 ) ∩ ( 𝑌 ) ) ⊆ ( 𝑌 ) ) → ( ‘ ( 𝑌 ) ) ⊆ ( ‘ ( ( 𝑋 ) ∩ ( 𝑌 ) ) ) )
48 5 44 46 47 syl3anc ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ 𝑋𝑉𝑌𝑉 ) → ( ‘ ( 𝑌 ) ) ⊆ ( ‘ ( ( 𝑋 ) ∩ ( 𝑌 ) ) ) )
49 42 48 unssd ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ 𝑋𝑉𝑌𝑉 ) → ( ( ‘ ( 𝑋 ) ) ∪ ( ‘ ( 𝑌 ) ) ) ⊆ ( ‘ ( ( 𝑋 ) ∩ ( 𝑌 ) ) ) )
50 38 49 sstrd ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ 𝑋𝑉𝑌𝑉 ) → ( 𝑋𝑌 ) ⊆ ( ‘ ( ( 𝑋 ) ∩ ( 𝑌 ) ) ) )
51 1 2 3 4 dochss ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( ‘ ( ( 𝑋 ) ∩ ( 𝑌 ) ) ) ⊆ 𝑉 ∧ ( 𝑋𝑌 ) ⊆ ( ‘ ( ( 𝑋 ) ∩ ( 𝑌 ) ) ) ) → ( ‘ ( ‘ ( ( 𝑋 ) ∩ ( 𝑌 ) ) ) ) ⊆ ( ‘ ( 𝑋𝑌 ) ) )
52 5 32 50 51 syl3anc ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ 𝑋𝑉𝑌𝑉 ) → ( ‘ ( ‘ ( ( 𝑋 ) ∩ ( 𝑌 ) ) ) ) ⊆ ( ‘ ( 𝑋𝑌 ) ) )
53 26 52 eqsstrrd ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ 𝑋𝑉𝑌𝑉 ) → ( ( 𝑋 ) ∩ ( 𝑌 ) ) ⊆ ( ‘ ( 𝑋𝑌 ) ) )
54 17 53 eqssd ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ 𝑋𝑉𝑌𝑉 ) → ( ‘ ( 𝑋𝑌 ) ) = ( ( 𝑋 ) ∩ ( 𝑌 ) ) )