Metamath Proof Explorer

Definition df-dih

Description: Define isomorphism H. (Contributed by NM, 28-Jan-2014)

Ref Expression
Assertion df-dih DIsoH = ( 𝑘 ∈ V ↦ ( 𝑤 ∈ ( LHyp ‘ 𝑘 ) ↦ ( 𝑥 ∈ ( Base ‘ 𝑘 ) ↦ if ( 𝑥 ( le ‘ 𝑘 ) 𝑤 , ( ( ( DIsoB ‘ 𝑘 ) ‘ 𝑤 ) ‘ 𝑥 ) , ( ℩ 𝑢 ∈ ( LSubSp ‘ ( ( DVecH ‘ 𝑘 ) ‘ 𝑤 ) ) ∀ 𝑞 ∈ ( Atoms ‘ 𝑘 ) ( ( ¬ 𝑞 ( le ‘ 𝑘 ) 𝑤 ∧ ( 𝑞 ( join ‘ 𝑘 ) ( 𝑥 ( meet ‘ 𝑘 ) 𝑤 ) ) = 𝑥 ) → 𝑢 = ( ( ( ( DIsoC ‘ 𝑘 ) ‘ 𝑤 ) ‘ 𝑞 ) ( LSSum ‘ ( ( DVecH ‘ 𝑘 ) ‘ 𝑤 ) ) ( ( ( DIsoB ‘ 𝑘 ) ‘ 𝑤 ) ‘ ( 𝑥 ( meet ‘ 𝑘 ) 𝑤 ) ) ) ) ) ) ) ) )

Detailed syntax breakdown

Step Hyp Ref Expression
0 cdih ⊢ DIsoH
1 vk ⊢ 𝑘
2 cvv ⊢ V
3 vw ⊢ 𝑤
4 clh ⊢ LHyp
5 1 cv ⊢ 𝑘
6 5 4 cfv ⊢ ( LHyp ‘ 𝑘 )
7 vx ⊢ 𝑥
8 cbs ⊢ Base
9 5 8 cfv ⊢ ( Base ‘ 𝑘 )
10 7 cv ⊢ 𝑥
11 cple ⊢ le
12 5 11 cfv ⊢ ( le ‘ 𝑘 )
13 3 cv ⊢ 𝑤
14 10 13 12 wbr ⊢ 𝑥 ( le ‘ 𝑘 ) 𝑤
15 cdib ⊢ DIsoB
16 5 15 cfv ⊢ ( DIsoB ‘ 𝑘 )
17 13 16 cfv ⊢ ( ( DIsoB ‘ 𝑘 ) ‘ 𝑤 )
18 10 17 cfv ⊢ ( ( ( DIsoB ‘ 𝑘 ) ‘ 𝑤 ) ‘ 𝑥 )
19 vu ⊢ 𝑢
20 clss ⊢ LSubSp
21 cdvh ⊢ DVecH
22 5 21 cfv ⊢ ( DVecH ‘ 𝑘 )
23 13 22 cfv ⊢ ( ( DVecH ‘ 𝑘 ) ‘ 𝑤 )
24 23 20 cfv ⊢ ( LSubSp ‘ ( ( DVecH ‘ 𝑘 ) ‘ 𝑤 ) )
25 vq ⊢ 𝑞
26 catm ⊢ Atoms
27 5 26 cfv ⊢ ( Atoms ‘ 𝑘 )
28 25 cv ⊢ 𝑞
29 28 13 12 wbr ⊢ 𝑞 ( le ‘ 𝑘 ) 𝑤
30 29 wn ⊢ ¬ 𝑞 ( le ‘ 𝑘 ) 𝑤
31 cjn ⊢ join
32 5 31 cfv ⊢ ( join ‘ 𝑘 )
33 cmee ⊢ meet
34 5 33 cfv ⊢ ( meet ‘ 𝑘 )
35 10 13 34 co ⊢ ( 𝑥 ( meet ‘ 𝑘 ) 𝑤 )
36 28 35 32 co ⊢ ( 𝑞 ( join ‘ 𝑘 ) ( 𝑥 ( meet ‘ 𝑘 ) 𝑤 ) )
37 36 10 wceq ⊢ ( 𝑞 ( join ‘ 𝑘 ) ( 𝑥 ( meet ‘ 𝑘 ) 𝑤 ) ) = 𝑥
38 30 37 wa ⊢ ( ¬ 𝑞 ( le ‘ 𝑘 ) 𝑤 ∧ ( 𝑞 ( join ‘ 𝑘 ) ( 𝑥 ( meet ‘ 𝑘 ) 𝑤 ) ) = 𝑥 )
39 19 cv ⊢ 𝑢
40 cdic ⊢ DIsoC
41 5 40 cfv ⊢ ( DIsoC ‘ 𝑘 )
42 13 41 cfv ⊢ ( ( DIsoC ‘ 𝑘 ) ‘ 𝑤 )
43 28 42 cfv ⊢ ( ( ( DIsoC ‘ 𝑘 ) ‘ 𝑤 ) ‘ 𝑞 )
44 clsm ⊢ LSSum
45 23 44 cfv ⊢ ( LSSum ‘ ( ( DVecH ‘ 𝑘 ) ‘ 𝑤 ) )
46 35 17 cfv ⊢ ( ( ( DIsoB ‘ 𝑘 ) ‘ 𝑤 ) ‘ ( 𝑥 ( meet ‘ 𝑘 ) 𝑤 ) )
47 43 46 45 co ⊢ ( ( ( ( DIsoC ‘ 𝑘 ) ‘ 𝑤 ) ‘ 𝑞 ) ( LSSum ‘ ( ( DVecH ‘ 𝑘 ) ‘ 𝑤 ) ) ( ( ( DIsoB ‘ 𝑘 ) ‘ 𝑤 ) ‘ ( 𝑥 ( meet ‘ 𝑘 ) 𝑤 ) ) )
48 39 47 wceq ⊢ 𝑢 = ( ( ( ( DIsoC ‘ 𝑘 ) ‘ 𝑤 ) ‘ 𝑞 ) ( LSSum ‘ ( ( DVecH ‘ 𝑘 ) ‘ 𝑤 ) ) ( ( ( DIsoB ‘ 𝑘 ) ‘ 𝑤 ) ‘ ( 𝑥 ( meet ‘ 𝑘 ) 𝑤 ) ) )
49 38 48 wi ⊢ ( ( ¬ 𝑞 ( le ‘ 𝑘 ) 𝑤 ∧ ( 𝑞 ( join ‘ 𝑘 ) ( 𝑥 ( meet ‘ 𝑘 ) 𝑤 ) ) = 𝑥 ) → 𝑢 = ( ( ( ( DIsoC ‘ 𝑘 ) ‘ 𝑤 ) ‘ 𝑞 ) ( LSSum ‘ ( ( DVecH ‘ 𝑘 ) ‘ 𝑤 ) ) ( ( ( DIsoB ‘ 𝑘 ) ‘ 𝑤 ) ‘ ( 𝑥 ( meet ‘ 𝑘 ) 𝑤 ) ) ) )
50 49 25 27 wral ⊢ ∀ 𝑞 ∈ ( Atoms ‘ 𝑘 ) ( ( ¬ 𝑞 ( le ‘ 𝑘 ) 𝑤 ∧ ( 𝑞 ( join ‘ 𝑘 ) ( 𝑥 ( meet ‘ 𝑘 ) 𝑤 ) ) = 𝑥 ) → 𝑢 = ( ( ( ( DIsoC ‘ 𝑘 ) ‘ 𝑤 ) ‘ 𝑞 ) ( LSSum ‘ ( ( DVecH ‘ 𝑘 ) ‘ 𝑤 ) ) ( ( ( DIsoB ‘ 𝑘 ) ‘ 𝑤 ) ‘ ( 𝑥 ( meet ‘ 𝑘 ) 𝑤 ) ) ) )
51 50 19 24 crio ⊢ ( ℩ 𝑢 ∈ ( LSubSp ‘ ( ( DVecH ‘ 𝑘 ) ‘ 𝑤 ) ) ∀ 𝑞 ∈ ( Atoms ‘ 𝑘 ) ( ( ¬ 𝑞 ( le ‘ 𝑘 ) 𝑤 ∧ ( 𝑞 ( join ‘ 𝑘 ) ( 𝑥 ( meet ‘ 𝑘 ) 𝑤 ) ) = 𝑥 ) → 𝑢 = ( ( ( ( DIsoC ‘ 𝑘 ) ‘ 𝑤 ) ‘ 𝑞 ) ( LSSum ‘ ( ( DVecH ‘ 𝑘 ) ‘ 𝑤 ) ) ( ( ( DIsoB ‘ 𝑘 ) ‘ 𝑤 ) ‘ ( 𝑥 ( meet ‘ 𝑘 ) 𝑤 ) ) ) ) )
52 14 18 51 cif ⊢ if ( 𝑥 ( le ‘ 𝑘 ) 𝑤 , ( ( ( DIsoB ‘ 𝑘 ) ‘ 𝑤 ) ‘ 𝑥 ) , ( ℩ 𝑢 ∈ ( LSubSp ‘ ( ( DVecH ‘ 𝑘 ) ‘ 𝑤 ) ) ∀ 𝑞 ∈ ( Atoms ‘ 𝑘 ) ( ( ¬ 𝑞 ( le ‘ 𝑘 ) 𝑤 ∧ ( 𝑞 ( join ‘ 𝑘 ) ( 𝑥 ( meet ‘ 𝑘 ) 𝑤 ) ) = 𝑥 ) → 𝑢 = ( ( ( ( DIsoC ‘ 𝑘 ) ‘ 𝑤 ) ‘ 𝑞 ) ( LSSum ‘ ( ( DVecH ‘ 𝑘 ) ‘ 𝑤 ) ) ( ( ( DIsoB ‘ 𝑘 ) ‘ 𝑤 ) ‘ ( 𝑥 ( meet ‘ 𝑘 ) 𝑤 ) ) ) ) ) )
53 7 9 52 cmpt ⊢ ( 𝑥 ∈ ( Base ‘ 𝑘 ) ↦ if ( 𝑥 ( le ‘ 𝑘 ) 𝑤 , ( ( ( DIsoB ‘ 𝑘 ) ‘ 𝑤 ) ‘ 𝑥 ) , ( ℩ 𝑢 ∈ ( LSubSp ‘ ( ( DVecH ‘ 𝑘 ) ‘ 𝑤 ) ) ∀ 𝑞 ∈ ( Atoms ‘ 𝑘 ) ( ( ¬ 𝑞 ( le ‘ 𝑘 ) 𝑤 ∧ ( 𝑞 ( join ‘ 𝑘 ) ( 𝑥 ( meet ‘ 𝑘 ) 𝑤 ) ) = 𝑥 ) → 𝑢 = ( ( ( ( DIsoC ‘ 𝑘 ) ‘ 𝑤 ) ‘ 𝑞 ) ( LSSum ‘ ( ( DVecH ‘ 𝑘 ) ‘ 𝑤 ) ) ( ( ( DIsoB ‘ 𝑘 ) ‘ 𝑤 ) ‘ ( 𝑥 ( meet ‘ 𝑘 ) 𝑤 ) ) ) ) ) ) )
54 3 6 53 cmpt ⊢ ( 𝑤 ∈ ( LHyp ‘ 𝑘 ) ↦ ( 𝑥 ∈ ( Base ‘ 𝑘 ) ↦ if ( 𝑥 ( le ‘ 𝑘 ) 𝑤 , ( ( ( DIsoB ‘ 𝑘 ) ‘ 𝑤 ) ‘ 𝑥 ) , ( ℩ 𝑢 ∈ ( LSubSp ‘ ( ( DVecH ‘ 𝑘 ) ‘ 𝑤 ) ) ∀ 𝑞 ∈ ( Atoms ‘ 𝑘 ) ( ( ¬ 𝑞 ( le ‘ 𝑘 ) 𝑤 ∧ ( 𝑞 ( join ‘ 𝑘 ) ( 𝑥 ( meet ‘ 𝑘 ) 𝑤 ) ) = 𝑥 ) → 𝑢 = ( ( ( ( DIsoC ‘ 𝑘 ) ‘ 𝑤 ) ‘ 𝑞 ) ( LSSum ‘ ( ( DVecH ‘ 𝑘 ) ‘ 𝑤 ) ) ( ( ( DIsoB ‘ 𝑘 ) ‘ 𝑤 ) ‘ ( 𝑥 ( meet ‘ 𝑘 ) 𝑤 ) ) ) ) ) ) ) )
55 1 2 54 cmpt ⊢ ( 𝑘 ∈ V ↦ ( 𝑤 ∈ ( LHyp ‘ 𝑘 ) ↦ ( 𝑥 ∈ ( Base ‘ 𝑘 ) ↦ if ( 𝑥 ( le ‘ 𝑘 ) 𝑤 , ( ( ( DIsoB ‘ 𝑘 ) ‘ 𝑤 ) ‘ 𝑥 ) , ( ℩ 𝑢 ∈ ( LSubSp ‘ ( ( DVecH ‘ 𝑘 ) ‘ 𝑤 ) ) ∀ 𝑞 ∈ ( Atoms ‘ 𝑘 ) ( ( ¬ 𝑞 ( le ‘ 𝑘 ) 𝑤 ∧ ( 𝑞 ( join ‘ 𝑘 ) ( 𝑥 ( meet ‘ 𝑘 ) 𝑤 ) ) = 𝑥 ) → 𝑢 = ( ( ( ( DIsoC ‘ 𝑘 ) ‘ 𝑤 ) ‘ 𝑞 ) ( LSSum ‘ ( ( DVecH ‘ 𝑘 ) ‘ 𝑤 ) ) ( ( ( DIsoB ‘ 𝑘 ) ‘ 𝑤 ) ‘ ( 𝑥 ( meet ‘ 𝑘 ) 𝑤 ) ) ) ) ) ) ) ) )
56 0 55 wceq ⊢ DIsoH = ( 𝑘 ∈ V ↦ ( 𝑤 ∈ ( LHyp ‘ 𝑘 ) ↦ ( 𝑥 ∈ ( Base ‘ 𝑘 ) ↦ if ( 𝑥 ( le ‘ 𝑘 ) 𝑤 , ( ( ( DIsoB ‘ 𝑘 ) ‘ 𝑤 ) ‘ 𝑥 ) , ( ℩ 𝑢 ∈ ( LSubSp ‘ ( ( DVecH ‘ 𝑘 ) ‘ 𝑤 ) ) ∀ 𝑞 ∈ ( Atoms ‘ 𝑘 ) ( ( ¬ 𝑞 ( le ‘ 𝑘 ) 𝑤 ∧ ( 𝑞 ( join ‘ 𝑘 ) ( 𝑥 ( meet ‘ 𝑘 ) 𝑤 ) ) = 𝑥 ) → 𝑢 = ( ( ( ( DIsoC ‘ 𝑘 ) ‘ 𝑤 ) ‘ 𝑞 ) ( LSSum ‘ ( ( DVecH ‘ 𝑘 ) ‘ 𝑤 ) ) ( ( ( DIsoB ‘ 𝑘 ) ‘ 𝑤 ) ‘ ( 𝑥 ( meet ‘ 𝑘 ) 𝑤 ) ) ) ) ) ) ) ) )