This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem dihf11lem

Description: Functionality of the isomorphism H. (Contributed by NM, 6-Mar-2014)

Ref Expression
Hypotheses dihf11.b ⊢ 𝐵 = ( Base ‘ 𝐾 )
dihf11.h ⊢ 𝐻 = ( LHyp ‘ 𝐾 )
dihf11.i ⊢ 𝐼 = ( ( DIsoH ‘ 𝐾 ) ‘ 𝑊 )
dihf11.u ⊢ 𝑈 = ( ( DVecH ‘ 𝐾 ) ‘ 𝑊 )
dihf11.s ⊢ 𝑆 = ( LSubSp ‘ 𝑈 )
Assertion dihf11lem ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) → 𝐼 : 𝐵 ⟶ 𝑆 )

Proof

Step Hyp Ref Expression
1 dihf11.b ⊢ 𝐵 = ( Base ‘ 𝐾 )
2 dihf11.h ⊢ 𝐻 = ( LHyp ‘ 𝐾 )
3 dihf11.i ⊢ 𝐼 = ( ( DIsoH ‘ 𝐾 ) ‘ 𝑊 )
4 dihf11.u ⊢ 𝑈 = ( ( DVecH ‘ 𝐾 ) ‘ 𝑊 )
5 dihf11.s ⊢ 𝑆 = ( LSubSp ‘ 𝑈 )
6 fvex ⊢ ( ( ( DIsoB ‘ 𝐾 ) ‘ 𝑊 ) ‘ 𝑥 ) ∈ V
7 riotaex ⊢ ( ℩ 𝑢 ∈ 𝑆 ∀ 𝑞 ∈ ( Atoms ‘ 𝐾 ) ( ( ¬ 𝑞 ( le ‘ 𝐾 ) 𝑊 ∧ ( 𝑞 ( join ‘ 𝐾 ) ( 𝑥 ( meet ‘ 𝐾 ) 𝑊 ) ) = 𝑥 ) → 𝑢 = ( ( ( ( DIsoC ‘ 𝐾 ) ‘ 𝑊 ) ‘ 𝑞 ) ( LSSum ‘ 𝑈 ) ( ( ( DIsoB ‘ 𝐾 ) ‘ 𝑊 ) ‘ ( 𝑥 ( meet ‘ 𝐾 ) 𝑊 ) ) ) ) ) ∈ V
8 6 7 ifex ⊢ if ( 𝑥 ( le ‘ 𝐾 ) 𝑊 , ( ( ( DIsoB ‘ 𝐾 ) ‘ 𝑊 ) ‘ 𝑥 ) , ( ℩ 𝑢 ∈ 𝑆 ∀ 𝑞 ∈ ( Atoms ‘ 𝐾 ) ( ( ¬ 𝑞 ( le ‘ 𝐾 ) 𝑊 ∧ ( 𝑞 ( join ‘ 𝐾 ) ( 𝑥 ( meet ‘ 𝐾 ) 𝑊 ) ) = 𝑥 ) → 𝑢 = ( ( ( ( DIsoC ‘ 𝐾 ) ‘ 𝑊 ) ‘ 𝑞 ) ( LSSum ‘ 𝑈 ) ( ( ( DIsoB ‘ 𝐾 ) ‘ 𝑊 ) ‘ ( 𝑥 ( meet ‘ 𝐾 ) 𝑊 ) ) ) ) ) ) ∈ V
9 8 rgenw ⊢ ∀ 𝑥 ∈ 𝐵 if ( 𝑥 ( le ‘ 𝐾 ) 𝑊 , ( ( ( DIsoB ‘ 𝐾 ) ‘ 𝑊 ) ‘ 𝑥 ) , ( ℩ 𝑢 ∈ 𝑆 ∀ 𝑞 ∈ ( Atoms ‘ 𝐾 ) ( ( ¬ 𝑞 ( le ‘ 𝐾 ) 𝑊 ∧ ( 𝑞 ( join ‘ 𝐾 ) ( 𝑥 ( meet ‘ 𝐾 ) 𝑊 ) ) = 𝑥 ) → 𝑢 = ( ( ( ( DIsoC ‘ 𝐾 ) ‘ 𝑊 ) ‘ 𝑞 ) ( LSSum ‘ 𝑈 ) ( ( ( DIsoB ‘ 𝐾 ) ‘ 𝑊 ) ‘ ( 𝑥 ( meet ‘ 𝐾 ) 𝑊 ) ) ) ) ) ) ∈ V
10 9 a1i ⊢ ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) → ∀ 𝑥 ∈ 𝐵 if ( 𝑥 ( le ‘ 𝐾 ) 𝑊 , ( ( ( DIsoB ‘ 𝐾 ) ‘ 𝑊 ) ‘ 𝑥 ) , ( ℩ 𝑢 ∈ 𝑆 ∀ 𝑞 ∈ ( Atoms ‘ 𝐾 ) ( ( ¬ 𝑞 ( le ‘ 𝐾 ) 𝑊 ∧ ( 𝑞 ( join ‘ 𝐾 ) ( 𝑥 ( meet ‘ 𝐾 ) 𝑊 ) ) = 𝑥 ) → 𝑢 = ( ( ( ( DIsoC ‘ 𝐾 ) ‘ 𝑊 ) ‘ 𝑞 ) ( LSSum ‘ 𝑈 ) ( ( ( DIsoB ‘ 𝐾 ) ‘ 𝑊 ) ‘ ( 𝑥 ( meet ‘ 𝐾 ) 𝑊 ) ) ) ) ) ) ∈ V )
11 eqid ⊢ ( 𝑥 ∈ 𝐵 ↦ if ( 𝑥 ( le ‘ 𝐾 ) 𝑊 , ( ( ( DIsoB ‘ 𝐾 ) ‘ 𝑊 ) ‘ 𝑥 ) , ( ℩ 𝑢 ∈ 𝑆 ∀ 𝑞 ∈ ( Atoms ‘ 𝐾 ) ( ( ¬ 𝑞 ( le ‘ 𝐾 ) 𝑊 ∧ ( 𝑞 ( join ‘ 𝐾 ) ( 𝑥 ( meet ‘ 𝐾 ) 𝑊 ) ) = 𝑥 ) → 𝑢 = ( ( ( ( DIsoC ‘ 𝐾 ) ‘ 𝑊 ) ‘ 𝑞 ) ( LSSum ‘ 𝑈 ) ( ( ( DIsoB ‘ 𝐾 ) ‘ 𝑊 ) ‘ ( 𝑥 ( meet ‘ 𝐾 ) 𝑊 ) ) ) ) ) ) ) = ( 𝑥 ∈ 𝐵 ↦ if ( 𝑥 ( le ‘ 𝐾 ) 𝑊 , ( ( ( DIsoB ‘ 𝐾 ) ‘ 𝑊 ) ‘ 𝑥 ) , ( ℩ 𝑢 ∈ 𝑆 ∀ 𝑞 ∈ ( Atoms ‘ 𝐾 ) ( ( ¬ 𝑞 ( le ‘ 𝐾 ) 𝑊 ∧ ( 𝑞 ( join ‘ 𝐾 ) ( 𝑥 ( meet ‘ 𝐾 ) 𝑊 ) ) = 𝑥 ) → 𝑢 = ( ( ( ( DIsoC ‘ 𝐾 ) ‘ 𝑊 ) ‘ 𝑞 ) ( LSSum ‘ 𝑈 ) ( ( ( DIsoB ‘ 𝐾 ) ‘ 𝑊 ) ‘ ( 𝑥 ( meet ‘ 𝐾 ) 𝑊 ) ) ) ) ) ) )
12 11 mptfng ⊢ ( ∀ 𝑥 ∈ 𝐵 if ( 𝑥 ( le ‘ 𝐾 ) 𝑊 , ( ( ( DIsoB ‘ 𝐾 ) ‘ 𝑊 ) ‘ 𝑥 ) , ( ℩ 𝑢 ∈ 𝑆 ∀ 𝑞 ∈ ( Atoms ‘ 𝐾 ) ( ( ¬ 𝑞 ( le ‘ 𝐾 ) 𝑊 ∧ ( 𝑞 ( join ‘ 𝐾 ) ( 𝑥 ( meet ‘ 𝐾 ) 𝑊 ) ) = 𝑥 ) → 𝑢 = ( ( ( ( DIsoC ‘ 𝐾 ) ‘ 𝑊 ) ‘ 𝑞 ) ( LSSum ‘ 𝑈 ) ( ( ( DIsoB ‘ 𝐾 ) ‘ 𝑊 ) ‘ ( 𝑥 ( meet ‘ 𝐾 ) 𝑊 ) ) ) ) ) ) ∈ V ↔ ( 𝑥 ∈ 𝐵 ↦ if ( 𝑥 ( le ‘ 𝐾 ) 𝑊 , ( ( ( DIsoB ‘ 𝐾 ) ‘ 𝑊 ) ‘ 𝑥 ) , ( ℩ 𝑢 ∈ 𝑆 ∀ 𝑞 ∈ ( Atoms ‘ 𝐾 ) ( ( ¬ 𝑞 ( le ‘ 𝐾 ) 𝑊 ∧ ( 𝑞 ( join ‘ 𝐾 ) ( 𝑥 ( meet ‘ 𝐾 ) 𝑊 ) ) = 𝑥 ) → 𝑢 = ( ( ( ( DIsoC ‘ 𝐾 ) ‘ 𝑊 ) ‘ 𝑞 ) ( LSSum ‘ 𝑈 ) ( ( ( DIsoB ‘ 𝐾 ) ‘ 𝑊 ) ‘ ( 𝑥 ( meet ‘ 𝐾 ) 𝑊 ) ) ) ) ) ) ) Fn 𝐵 )
13 10 12 sylib ⊢ ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) → ( 𝑥 ∈ 𝐵 ↦ if ( 𝑥 ( le ‘ 𝐾 ) 𝑊 , ( ( ( DIsoB ‘ 𝐾 ) ‘ 𝑊 ) ‘ 𝑥 ) , ( ℩ 𝑢 ∈ 𝑆 ∀ 𝑞 ∈ ( Atoms ‘ 𝐾 ) ( ( ¬ 𝑞 ( le ‘ 𝐾 ) 𝑊 ∧ ( 𝑞 ( join ‘ 𝐾 ) ( 𝑥 ( meet ‘ 𝐾 ) 𝑊 ) ) = 𝑥 ) → 𝑢 = ( ( ( ( DIsoC ‘ 𝐾 ) ‘ 𝑊 ) ‘ 𝑞 ) ( LSSum ‘ 𝑈 ) ( ( ( DIsoB ‘ 𝐾 ) ‘ 𝑊 ) ‘ ( 𝑥 ( meet ‘ 𝐾 ) 𝑊 ) ) ) ) ) ) ) Fn 𝐵 )
14 eqid ⊢ ( le ‘ 𝐾 ) = ( le ‘ 𝐾 )
15 eqid ⊢ ( join ‘ 𝐾 ) = ( join ‘ 𝐾 )
16 eqid ⊢ ( meet ‘ 𝐾 ) = ( meet ‘ 𝐾 )
17 eqid ⊢ ( Atoms ‘ 𝐾 ) = ( Atoms ‘ 𝐾 )
18 eqid ⊢ ( ( DIsoB ‘ 𝐾 ) ‘ 𝑊 ) = ( ( DIsoB ‘ 𝐾 ) ‘ 𝑊 )
19 eqid ⊢ ( ( DIsoC ‘ 𝐾 ) ‘ 𝑊 ) = ( ( DIsoC ‘ 𝐾 ) ‘ 𝑊 )
20 eqid ⊢ ( LSSum ‘ 𝑈 ) = ( LSSum ‘ 𝑈 )
21 1 14 15 16 17 2 3 18 19 4 5 20 dihfval ⊢ ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) → 𝐼 = ( 𝑥 ∈ 𝐵 ↦ if ( 𝑥 ( le ‘ 𝐾 ) 𝑊 , ( ( ( DIsoB ‘ 𝐾 ) ‘ 𝑊 ) ‘ 𝑥 ) , ( ℩ 𝑢 ∈ 𝑆 ∀ 𝑞 ∈ ( Atoms ‘ 𝐾 ) ( ( ¬ 𝑞 ( le ‘ 𝐾 ) 𝑊 ∧ ( 𝑞 ( join ‘ 𝐾 ) ( 𝑥 ( meet ‘ 𝐾 ) 𝑊 ) ) = 𝑥 ) → 𝑢 = ( ( ( ( DIsoC ‘ 𝐾 ) ‘ 𝑊 ) ‘ 𝑞 ) ( LSSum ‘ 𝑈 ) ( ( ( DIsoB ‘ 𝐾 ) ‘ 𝑊 ) ‘ ( 𝑥 ( meet ‘ 𝐾 ) 𝑊 ) ) ) ) ) ) ) )
22 21 fneq1d ⊢ ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) → ( 𝐼 Fn 𝐵 ↔ ( 𝑥 ∈ 𝐵 ↦ if ( 𝑥 ( le ‘ 𝐾 ) 𝑊 , ( ( ( DIsoB ‘ 𝐾 ) ‘ 𝑊 ) ‘ 𝑥 ) , ( ℩ 𝑢 ∈ 𝑆 ∀ 𝑞 ∈ ( Atoms ‘ 𝐾 ) ( ( ¬ 𝑞 ( le ‘ 𝐾 ) 𝑊 ∧ ( 𝑞 ( join ‘ 𝐾 ) ( 𝑥 ( meet ‘ 𝐾 ) 𝑊 ) ) = 𝑥 ) → 𝑢 = ( ( ( ( DIsoC ‘ 𝐾 ) ‘ 𝑊 ) ‘ 𝑞 ) ( LSSum ‘ 𝑈 ) ( ( ( DIsoB ‘ 𝐾 ) ‘ 𝑊 ) ‘ ( 𝑥 ( meet ‘ 𝐾 ) 𝑊 ) ) ) ) ) ) ) Fn 𝐵 ) )
23 13 22 mpbird ⊢ ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) → 𝐼 Fn 𝐵 )
24 1 2 3 4 5 dihlss ⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝑦 ∈ 𝐵 ) → ( 𝐼 ‘ 𝑦 ) ∈ 𝑆 )
25 24 ralrimiva ⊢ ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) → ∀ 𝑦 ∈ 𝐵 ( 𝐼 ‘ 𝑦 ) ∈ 𝑆 )
26 fnfvrnss ⊢ ( ( 𝐼 Fn 𝐵 ∧ ∀ 𝑦 ∈ 𝐵 ( 𝐼 ‘ 𝑦 ) ∈ 𝑆 ) → ran 𝐼 ⊆ 𝑆 )
27 23 25 26 syl2anc ⊢ ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) → ran 𝐼 ⊆ 𝑆 )
28 df-f ⊢ ( 𝐼 : 𝐵 ⟶ 𝑆 ↔ ( 𝐼 Fn 𝐵 ∧ ran 𝐼 ⊆ 𝑆 ) )
29 23 27 28 sylanbrc ⊢ ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) → 𝐼 : 𝐵 ⟶ 𝑆 )