Metamath Proof Explorer


Theorem lhpmod2i2

Description: Modular law for hyperplanes analogous to atmod2i2 for atoms. (Contributed by NM, 9-Feb-2013)

Ref Expression
Hypotheses lhpmod.b 𝐵 = ( Base ‘ 𝐾 )
lhpmod.l = ( le ‘ 𝐾 )
lhpmod.j = ( join ‘ 𝐾 )
lhpmod.m = ( meet ‘ 𝐾 )
lhpmod.h 𝐻 = ( LHyp ‘ 𝐾 )
Assertion lhpmod2i2 ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( 𝑋𝐵𝑌𝐵 ) ∧ 𝑌 𝑋 ) → ( ( 𝑋 𝑊 ) 𝑌 ) = ( 𝑋 ( 𝑊 𝑌 ) ) )

Proof

Step Hyp Ref Expression
1 lhpmod.b 𝐵 = ( Base ‘ 𝐾 )
2 lhpmod.l = ( le ‘ 𝐾 )
3 lhpmod.j = ( join ‘ 𝐾 )
4 lhpmod.m = ( meet ‘ 𝐾 )
5 lhpmod.h 𝐻 = ( LHyp ‘ 𝐾 )
6 simp1l ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( 𝑋𝐵𝑌𝐵 ) ∧ 𝑌 𝑋 ) → 𝐾 ∈ HL )
7 simp1r ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( 𝑋𝐵𝑌𝐵 ) ∧ 𝑌 𝑋 ) → 𝑊𝐻 )
8 eqid ( oc ‘ 𝐾 ) = ( oc ‘ 𝐾 )
9 eqid ( Atoms ‘ 𝐾 ) = ( Atoms ‘ 𝐾 )
10 8 9 5 lhpocat ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) → ( ( oc ‘ 𝐾 ) ‘ 𝑊 ) ∈ ( Atoms ‘ 𝐾 ) )
11 6 7 10 syl2anc ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( 𝑋𝐵𝑌𝐵 ) ∧ 𝑌 𝑋 ) → ( ( oc ‘ 𝐾 ) ‘ 𝑊 ) ∈ ( Atoms ‘ 𝐾 ) )
12 hlop ( 𝐾 ∈ HL → 𝐾 ∈ OP )
13 6 12 syl ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( 𝑋𝐵𝑌𝐵 ) ∧ 𝑌 𝑋 ) → 𝐾 ∈ OP )
14 simp2l ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( 𝑋𝐵𝑌𝐵 ) ∧ 𝑌 𝑋 ) → 𝑋𝐵 )
15 1 8 opoccl ( ( 𝐾 ∈ OP ∧ 𝑋𝐵 ) → ( ( oc ‘ 𝐾 ) ‘ 𝑋 ) ∈ 𝐵 )
16 13 14 15 syl2anc ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( 𝑋𝐵𝑌𝐵 ) ∧ 𝑌 𝑋 ) → ( ( oc ‘ 𝐾 ) ‘ 𝑋 ) ∈ 𝐵 )
17 simp2r ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( 𝑋𝐵𝑌𝐵 ) ∧ 𝑌 𝑋 ) → 𝑌𝐵 )
18 1 8 opoccl ( ( 𝐾 ∈ OP ∧ 𝑌𝐵 ) → ( ( oc ‘ 𝐾 ) ‘ 𝑌 ) ∈ 𝐵 )
19 13 17 18 syl2anc ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( 𝑋𝐵𝑌𝐵 ) ∧ 𝑌 𝑋 ) → ( ( oc ‘ 𝐾 ) ‘ 𝑌 ) ∈ 𝐵 )
20 simp3 ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( 𝑋𝐵𝑌𝐵 ) ∧ 𝑌 𝑋 ) → 𝑌 𝑋 )
21 1 2 8 oplecon3b ( ( 𝐾 ∈ OP ∧ 𝑌𝐵𝑋𝐵 ) → ( 𝑌 𝑋 ↔ ( ( oc ‘ 𝐾 ) ‘ 𝑋 ) ( ( oc ‘ 𝐾 ) ‘ 𝑌 ) ) )
22 13 17 14 21 syl3anc ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( 𝑋𝐵𝑌𝐵 ) ∧ 𝑌 𝑋 ) → ( 𝑌 𝑋 ↔ ( ( oc ‘ 𝐾 ) ‘ 𝑋 ) ( ( oc ‘ 𝐾 ) ‘ 𝑌 ) ) )
23 20 22 mpbid ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( 𝑋𝐵𝑌𝐵 ) ∧ 𝑌 𝑋 ) → ( ( oc ‘ 𝐾 ) ‘ 𝑋 ) ( ( oc ‘ 𝐾 ) ‘ 𝑌 ) )
24 1 2 3 4 9 atmod1i2 ( ( 𝐾 ∈ HL ∧ ( ( ( oc ‘ 𝐾 ) ‘ 𝑊 ) ∈ ( Atoms ‘ 𝐾 ) ∧ ( ( oc ‘ 𝐾 ) ‘ 𝑋 ) ∈ 𝐵 ∧ ( ( oc ‘ 𝐾 ) ‘ 𝑌 ) ∈ 𝐵 ) ∧ ( ( oc ‘ 𝐾 ) ‘ 𝑋 ) ( ( oc ‘ 𝐾 ) ‘ 𝑌 ) ) → ( ( ( oc ‘ 𝐾 ) ‘ 𝑋 ) ( ( ( oc ‘ 𝐾 ) ‘ 𝑊 ) ( ( oc ‘ 𝐾 ) ‘ 𝑌 ) ) ) = ( ( ( ( oc ‘ 𝐾 ) ‘ 𝑋 ) ( ( oc ‘ 𝐾 ) ‘ 𝑊 ) ) ( ( oc ‘ 𝐾 ) ‘ 𝑌 ) ) )
25 6 11 16 19 23 24 syl131anc ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( 𝑋𝐵𝑌𝐵 ) ∧ 𝑌 𝑋 ) → ( ( ( oc ‘ 𝐾 ) ‘ 𝑋 ) ( ( ( oc ‘ 𝐾 ) ‘ 𝑊 ) ( ( oc ‘ 𝐾 ) ‘ 𝑌 ) ) ) = ( ( ( ( oc ‘ 𝐾 ) ‘ 𝑋 ) ( ( oc ‘ 𝐾 ) ‘ 𝑊 ) ) ( ( oc ‘ 𝐾 ) ‘ 𝑌 ) ) )
26 6 hllatd ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( 𝑋𝐵𝑌𝐵 ) ∧ 𝑌 𝑋 ) → 𝐾 ∈ Lat )
27 1 5 lhpbase ( 𝑊𝐻𝑊𝐵 )
28 7 27 syl ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( 𝑋𝐵𝑌𝐵 ) ∧ 𝑌 𝑋 ) → 𝑊𝐵 )
29 1 4 latmcl ( ( 𝐾 ∈ Lat ∧ 𝑋𝐵𝑊𝐵 ) → ( 𝑋 𝑊 ) ∈ 𝐵 )
30 26 14 28 29 syl3anc ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( 𝑋𝐵𝑌𝐵 ) ∧ 𝑌 𝑋 ) → ( 𝑋 𝑊 ) ∈ 𝐵 )
31 1 3 latjcl ( ( 𝐾 ∈ Lat ∧ ( 𝑋 𝑊 ) ∈ 𝐵𝑌𝐵 ) → ( ( 𝑋 𝑊 ) 𝑌 ) ∈ 𝐵 )
32 26 30 17 31 syl3anc ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( 𝑋𝐵𝑌𝐵 ) ∧ 𝑌 𝑋 ) → ( ( 𝑋 𝑊 ) 𝑌 ) ∈ 𝐵 )
33 1 3 latjcl ( ( 𝐾 ∈ Lat ∧ 𝑊𝐵𝑌𝐵 ) → ( 𝑊 𝑌 ) ∈ 𝐵 )
34 26 28 17 33 syl3anc ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( 𝑋𝐵𝑌𝐵 ) ∧ 𝑌 𝑋 ) → ( 𝑊 𝑌 ) ∈ 𝐵 )
35 1 4 latmcl ( ( 𝐾 ∈ Lat ∧ 𝑋𝐵 ∧ ( 𝑊 𝑌 ) ∈ 𝐵 ) → ( 𝑋 ( 𝑊 𝑌 ) ) ∈ 𝐵 )
36 26 14 34 35 syl3anc ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( 𝑋𝐵𝑌𝐵 ) ∧ 𝑌 𝑋 ) → ( 𝑋 ( 𝑊 𝑌 ) ) ∈ 𝐵 )
37 1 8 opcon3b ( ( 𝐾 ∈ OP ∧ ( ( 𝑋 𝑊 ) 𝑌 ) ∈ 𝐵 ∧ ( 𝑋 ( 𝑊 𝑌 ) ) ∈ 𝐵 ) → ( ( ( 𝑋 𝑊 ) 𝑌 ) = ( 𝑋 ( 𝑊 𝑌 ) ) ↔ ( ( oc ‘ 𝐾 ) ‘ ( 𝑋 ( 𝑊 𝑌 ) ) ) = ( ( oc ‘ 𝐾 ) ‘ ( ( 𝑋 𝑊 ) 𝑌 ) ) ) )
38 13 32 36 37 syl3anc ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( 𝑋𝐵𝑌𝐵 ) ∧ 𝑌 𝑋 ) → ( ( ( 𝑋 𝑊 ) 𝑌 ) = ( 𝑋 ( 𝑊 𝑌 ) ) ↔ ( ( oc ‘ 𝐾 ) ‘ ( 𝑋 ( 𝑊 𝑌 ) ) ) = ( ( oc ‘ 𝐾 ) ‘ ( ( 𝑋 𝑊 ) 𝑌 ) ) ) )
39 hlol ( 𝐾 ∈ HL → 𝐾 ∈ OL )
40 6 39 syl ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( 𝑋𝐵𝑌𝐵 ) ∧ 𝑌 𝑋 ) → 𝐾 ∈ OL )
41 1 3 4 8 oldmm1 ( ( 𝐾 ∈ OL ∧ 𝑋𝐵 ∧ ( 𝑊 𝑌 ) ∈ 𝐵 ) → ( ( oc ‘ 𝐾 ) ‘ ( 𝑋 ( 𝑊 𝑌 ) ) ) = ( ( ( oc ‘ 𝐾 ) ‘ 𝑋 ) ( ( oc ‘ 𝐾 ) ‘ ( 𝑊 𝑌 ) ) ) )
42 40 14 34 41 syl3anc ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( 𝑋𝐵𝑌𝐵 ) ∧ 𝑌 𝑋 ) → ( ( oc ‘ 𝐾 ) ‘ ( 𝑋 ( 𝑊 𝑌 ) ) ) = ( ( ( oc ‘ 𝐾 ) ‘ 𝑋 ) ( ( oc ‘ 𝐾 ) ‘ ( 𝑊 𝑌 ) ) ) )
43 1 3 4 8 oldmj1 ( ( 𝐾 ∈ OL ∧ 𝑊𝐵𝑌𝐵 ) → ( ( oc ‘ 𝐾 ) ‘ ( 𝑊 𝑌 ) ) = ( ( ( oc ‘ 𝐾 ) ‘ 𝑊 ) ( ( oc ‘ 𝐾 ) ‘ 𝑌 ) ) )
44 40 28 17 43 syl3anc ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( 𝑋𝐵𝑌𝐵 ) ∧ 𝑌 𝑋 ) → ( ( oc ‘ 𝐾 ) ‘ ( 𝑊 𝑌 ) ) = ( ( ( oc ‘ 𝐾 ) ‘ 𝑊 ) ( ( oc ‘ 𝐾 ) ‘ 𝑌 ) ) )
45 44 oveq2d ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( 𝑋𝐵𝑌𝐵 ) ∧ 𝑌 𝑋 ) → ( ( ( oc ‘ 𝐾 ) ‘ 𝑋 ) ( ( oc ‘ 𝐾 ) ‘ ( 𝑊 𝑌 ) ) ) = ( ( ( oc ‘ 𝐾 ) ‘ 𝑋 ) ( ( ( oc ‘ 𝐾 ) ‘ 𝑊 ) ( ( oc ‘ 𝐾 ) ‘ 𝑌 ) ) ) )
46 42 45 eqtrd ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( 𝑋𝐵𝑌𝐵 ) ∧ 𝑌 𝑋 ) → ( ( oc ‘ 𝐾 ) ‘ ( 𝑋 ( 𝑊 𝑌 ) ) ) = ( ( ( oc ‘ 𝐾 ) ‘ 𝑋 ) ( ( ( oc ‘ 𝐾 ) ‘ 𝑊 ) ( ( oc ‘ 𝐾 ) ‘ 𝑌 ) ) ) )
47 1 3 4 8 oldmj1 ( ( 𝐾 ∈ OL ∧ ( 𝑋 𝑊 ) ∈ 𝐵𝑌𝐵 ) → ( ( oc ‘ 𝐾 ) ‘ ( ( 𝑋 𝑊 ) 𝑌 ) ) = ( ( ( oc ‘ 𝐾 ) ‘ ( 𝑋 𝑊 ) ) ( ( oc ‘ 𝐾 ) ‘ 𝑌 ) ) )
48 40 30 17 47 syl3anc ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( 𝑋𝐵𝑌𝐵 ) ∧ 𝑌 𝑋 ) → ( ( oc ‘ 𝐾 ) ‘ ( ( 𝑋 𝑊 ) 𝑌 ) ) = ( ( ( oc ‘ 𝐾 ) ‘ ( 𝑋 𝑊 ) ) ( ( oc ‘ 𝐾 ) ‘ 𝑌 ) ) )
49 1 3 4 8 oldmm1 ( ( 𝐾 ∈ OL ∧ 𝑋𝐵𝑊𝐵 ) → ( ( oc ‘ 𝐾 ) ‘ ( 𝑋 𝑊 ) ) = ( ( ( oc ‘ 𝐾 ) ‘ 𝑋 ) ( ( oc ‘ 𝐾 ) ‘ 𝑊 ) ) )
50 40 14 28 49 syl3anc ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( 𝑋𝐵𝑌𝐵 ) ∧ 𝑌 𝑋 ) → ( ( oc ‘ 𝐾 ) ‘ ( 𝑋 𝑊 ) ) = ( ( ( oc ‘ 𝐾 ) ‘ 𝑋 ) ( ( oc ‘ 𝐾 ) ‘ 𝑊 ) ) )
51 50 oveq1d ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( 𝑋𝐵𝑌𝐵 ) ∧ 𝑌 𝑋 ) → ( ( ( oc ‘ 𝐾 ) ‘ ( 𝑋 𝑊 ) ) ( ( oc ‘ 𝐾 ) ‘ 𝑌 ) ) = ( ( ( ( oc ‘ 𝐾 ) ‘ 𝑋 ) ( ( oc ‘ 𝐾 ) ‘ 𝑊 ) ) ( ( oc ‘ 𝐾 ) ‘ 𝑌 ) ) )
52 48 51 eqtrd ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( 𝑋𝐵𝑌𝐵 ) ∧ 𝑌 𝑋 ) → ( ( oc ‘ 𝐾 ) ‘ ( ( 𝑋 𝑊 ) 𝑌 ) ) = ( ( ( ( oc ‘ 𝐾 ) ‘ 𝑋 ) ( ( oc ‘ 𝐾 ) ‘ 𝑊 ) ) ( ( oc ‘ 𝐾 ) ‘ 𝑌 ) ) )
53 46 52 eqeq12d ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( 𝑋𝐵𝑌𝐵 ) ∧ 𝑌 𝑋 ) → ( ( ( oc ‘ 𝐾 ) ‘ ( 𝑋 ( 𝑊 𝑌 ) ) ) = ( ( oc ‘ 𝐾 ) ‘ ( ( 𝑋 𝑊 ) 𝑌 ) ) ↔ ( ( ( oc ‘ 𝐾 ) ‘ 𝑋 ) ( ( ( oc ‘ 𝐾 ) ‘ 𝑊 ) ( ( oc ‘ 𝐾 ) ‘ 𝑌 ) ) ) = ( ( ( ( oc ‘ 𝐾 ) ‘ 𝑋 ) ( ( oc ‘ 𝐾 ) ‘ 𝑊 ) ) ( ( oc ‘ 𝐾 ) ‘ 𝑌 ) ) ) )
54 38 53 bitrd ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( 𝑋𝐵𝑌𝐵 ) ∧ 𝑌 𝑋 ) → ( ( ( 𝑋 𝑊 ) 𝑌 ) = ( 𝑋 ( 𝑊 𝑌 ) ) ↔ ( ( ( oc ‘ 𝐾 ) ‘ 𝑋 ) ( ( ( oc ‘ 𝐾 ) ‘ 𝑊 ) ( ( oc ‘ 𝐾 ) ‘ 𝑌 ) ) ) = ( ( ( ( oc ‘ 𝐾 ) ‘ 𝑋 ) ( ( oc ‘ 𝐾 ) ‘ 𝑊 ) ) ( ( oc ‘ 𝐾 ) ‘ 𝑌 ) ) ) )
55 25 54 mpbird ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( 𝑋𝐵𝑌𝐵 ) ∧ 𝑌 𝑋 ) → ( ( 𝑋 𝑊 ) 𝑌 ) = ( 𝑋 ( 𝑊 𝑌 ) ) )