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 ⊢ ( 𝜑 → ( 𝐼 ‘ ( 𝑋 ∨ 𝑃 ) ) = ( ( 𝐼 ‘ 𝑋 ) ⊕ ( 𝐼 ‘ 𝑃 ) ) )