Metamath Proof Explorer


Theorem dihjatc

Description: Isomorphism H of lattice join of an element under the fiducial hyperplane with atom not under it. (Contributed by NM, 26-Aug-2014)

Ref Expression
Hypotheses dihjatc.b 𝐵 = ( Base ‘ 𝐾 )
dihjatc.l = ( le ‘ 𝐾 )
dihjatc.h 𝐻 = ( LHyp ‘ 𝐾 )
dihjatc.j = ( join ‘ 𝐾 )
dihjatc.a 𝐴 = ( Atoms ‘ 𝐾 )
dihjatc.u 𝑈 = ( ( DVecH ‘ 𝐾 ) ‘ 𝑊 )
dihjatc.s = ( LSSum ‘ 𝑈 )
dihjatc.i 𝐼 = ( ( DIsoH ‘ 𝐾 ) ‘ 𝑊 )
dihjatc.k ( 𝜑 → ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) )
dihjatc.x ( 𝜑 → ( 𝑋𝐵𝑋 𝑊 ) )
dihjatc.p ( 𝜑 → ( 𝑃𝐴 ∧ ¬ 𝑃 𝑊 ) )
Assertion dihjatc ( 𝜑 → ( 𝐼 ‘ ( 𝑋 𝑃 ) ) = ( ( 𝐼𝑋 ) ( 𝐼𝑃 ) ) )

Proof

Step Hyp Ref Expression
1 dihjatc.b 𝐵 = ( Base ‘ 𝐾 )
2 dihjatc.l = ( le ‘ 𝐾 )
3 dihjatc.h 𝐻 = ( LHyp ‘ 𝐾 )
4 dihjatc.j = ( join ‘ 𝐾 )
5 dihjatc.a 𝐴 = ( Atoms ‘ 𝐾 )
6 dihjatc.u 𝑈 = ( ( DVecH ‘ 𝐾 ) ‘ 𝑊 )
7 dihjatc.s = ( LSSum ‘ 𝑈 )
8 dihjatc.i 𝐼 = ( ( DIsoH ‘ 𝐾 ) ‘ 𝑊 )
9 dihjatc.k ( 𝜑 → ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) )
10 dihjatc.x ( 𝜑 → ( 𝑋𝐵𝑋 𝑊 ) )
11 dihjatc.p ( 𝜑 → ( 𝑃𝐴 ∧ ¬ 𝑃 𝑊 ) )
12 9 simpld ( 𝜑𝐾 ∈ HL )
13 hlop ( 𝐾 ∈ HL → 𝐾 ∈ OP )
14 12 13 syl ( 𝜑𝐾 ∈ OP )
15 eqid ( 1. ‘ 𝐾 ) = ( 1. ‘ 𝐾 )
16 1 15 op1cl ( 𝐾 ∈ OP → ( 1. ‘ 𝐾 ) ∈ 𝐵 )
17 14 16 syl ( 𝜑 → ( 1. ‘ 𝐾 ) ∈ 𝐵 )
18 10 simpld ( 𝜑𝑋𝐵 )
19 11 simpld ( 𝜑𝑃𝐴 )
20 1 5 atbase ( 𝑃𝐴𝑃𝐵 )
21 19 20 syl ( 𝜑𝑃𝐵 )
22 1 2 15 ople1 ( ( 𝐾 ∈ OP ∧ 𝑃𝐵 ) → 𝑃 ( 1. ‘ 𝐾 ) )
23 14 21 22 syl2anc ( 𝜑𝑃 ( 1. ‘ 𝐾 ) )
24 hlol ( 𝐾 ∈ HL → 𝐾 ∈ OL )
25 12 24 syl ( 𝜑𝐾 ∈ OL )
26 eqid ( meet ‘ 𝐾 ) = ( meet ‘ 𝐾 )
27 1 26 15 olm12 ( ( 𝐾 ∈ OL ∧ 𝑋𝐵 ) → ( ( 1. ‘ 𝐾 ) ( meet ‘ 𝐾 ) 𝑋 ) = 𝑋 )
28 25 18 27 syl2anc ( 𝜑 → ( ( 1. ‘ 𝐾 ) ( meet ‘ 𝐾 ) 𝑋 ) = 𝑋 )
29 10 simprd ( 𝜑𝑋 𝑊 )
30 28 29 eqbrtrd ( 𝜑 → ( ( 1. ‘ 𝐾 ) ( meet ‘ 𝐾 ) 𝑋 ) 𝑊 )
31 1 2 3 4 26 5 6 7 8 dihjatc3 ( ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( 1. ‘ 𝐾 ) ∈ 𝐵𝑋𝐵 ) ∧ ( 𝑃𝐴 ∧ ¬ 𝑃 𝑊 ) ∧ ( 𝑃 ( 1. ‘ 𝐾 ) ∧ ( ( 1. ‘ 𝐾 ) ( meet ‘ 𝐾 ) 𝑋 ) 𝑊 ) ) → ( 𝐼 ‘ ( ( ( 1. ‘ 𝐾 ) ( meet ‘ 𝐾 ) 𝑋 ) 𝑃 ) ) = ( ( 𝐼 ‘ ( ( 1. ‘ 𝐾 ) ( meet ‘ 𝐾 ) 𝑋 ) ) ( 𝐼𝑃 ) ) )
32 9 17 18 11 23 30 31 syl312anc ( 𝜑 → ( 𝐼 ‘ ( ( ( 1. ‘ 𝐾 ) ( meet ‘ 𝐾 ) 𝑋 ) 𝑃 ) ) = ( ( 𝐼 ‘ ( ( 1. ‘ 𝐾 ) ( meet ‘ 𝐾 ) 𝑋 ) ) ( 𝐼𝑃 ) ) )
33 28 fvoveq1d ( 𝜑 → ( 𝐼 ‘ ( ( ( 1. ‘ 𝐾 ) ( meet ‘ 𝐾 ) 𝑋 ) 𝑃 ) ) = ( 𝐼 ‘ ( 𝑋 𝑃 ) ) )
34 28 fveq2d ( 𝜑 → ( 𝐼 ‘ ( ( 1. ‘ 𝐾 ) ( meet ‘ 𝐾 ) 𝑋 ) ) = ( 𝐼𝑋 ) )
35 34 oveq1d ( 𝜑 → ( ( 𝐼 ‘ ( ( 1. ‘ 𝐾 ) ( meet ‘ 𝐾 ) 𝑋 ) ) ( 𝐼𝑃 ) ) = ( ( 𝐼𝑋 ) ( 𝐼𝑃 ) ) )
36 32 33 35 3eqtr3d ( 𝜑 → ( 𝐼 ‘ ( 𝑋 𝑃 ) ) = ( ( 𝐼𝑋 ) ( 𝐼𝑃 ) ) )