Metamath Proof Explorer

Theorem dihf11lem

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

Ref Expression
Hypotheses dihf11.b ⊢ B = Base K
dihf11.h ⊢ H = LHyp ⁡ K
dihf11.i ⊢ I = DIsoH ⁡ K ⁡ W
dihf11.u ⊢ U = DVecH ⁡ K ⁡ W
dihf11.s ⊢ S = LSubSp ⁡ U
Assertion dihf11lem ⊢ K ∈ HL ∧ W ∈ H → I : B ⟶ S

Proof

Step Hyp Ref Expression
1 dihf11.b ⊢ B = Base K
2 dihf11.h ⊢ H = LHyp ⁡ K
3 dihf11.i ⊢ I = DIsoH ⁡ K ⁡ W
4 dihf11.u ⊢ U = DVecH ⁡ K ⁡ W
5 dihf11.s ⊢ S = LSubSp ⁡ U
6 fvex ⊢ DIsoB ⁡ K ⁡ W ⁡ x ∈ V
7 riotaex ⊢ ι u ∈ S | ∀ q ∈ Atoms ⁡ K ¬ q ≤ K W ∧ q join ⁡ K x meet ⁡ K W = x → u = DIsoC ⁡ K ⁡ W ⁡ q LSSum ⁡ U DIsoB ⁡ K ⁡ W ⁡ x meet ⁡ K W ∈ V
8 6 7 ifex ⊢ if x ≤ K W DIsoB ⁡ K ⁡ W ⁡ x ι u ∈ S | ∀ q ∈ Atoms ⁡ K ¬ q ≤ K W ∧ q join ⁡ K x meet ⁡ K W = x → u = DIsoC ⁡ K ⁡ W ⁡ q LSSum ⁡ U DIsoB ⁡ K ⁡ W ⁡ x meet ⁡ K W ∈ V
9 8 rgenw ⊢ ∀ x ∈ B if x ≤ K W DIsoB ⁡ K ⁡ W ⁡ x ι u ∈ S | ∀ q ∈ Atoms ⁡ K ¬ q ≤ K W ∧ q join ⁡ K x meet ⁡ K W = x → u = DIsoC ⁡ K ⁡ W ⁡ q LSSum ⁡ U DIsoB ⁡ K ⁡ W ⁡ x meet ⁡ K W ∈ V
10 9 a1i ⊢ K ∈ HL ∧ W ∈ H → ∀ x ∈ B if x ≤ K W DIsoB ⁡ K ⁡ W ⁡ x ι u ∈ S | ∀ q ∈ Atoms ⁡ K ¬ q ≤ K W ∧ q join ⁡ K x meet ⁡ K W = x → u = DIsoC ⁡ K ⁡ W ⁡ q LSSum ⁡ U DIsoB ⁡ K ⁡ W ⁡ x meet ⁡ K W ∈ V
11 eqid ⊢ x ∈ B ⟼ if x ≤ K W DIsoB ⁡ K ⁡ W ⁡ x ι u ∈ S | ∀ q ∈ Atoms ⁡ K ¬ q ≤ K W ∧ q join ⁡ K x meet ⁡ K W = x → u = DIsoC ⁡ K ⁡ W ⁡ q LSSum ⁡ U DIsoB ⁡ K ⁡ W ⁡ x meet ⁡ K W = x ∈ B ⟼ if x ≤ K W DIsoB ⁡ K ⁡ W ⁡ x ι u ∈ S | ∀ q ∈ Atoms ⁡ K ¬ q ≤ K W ∧ q join ⁡ K x meet ⁡ K W = x → u = DIsoC ⁡ K ⁡ W ⁡ q LSSum ⁡ U DIsoB ⁡ K ⁡ W ⁡ x meet ⁡ K W
12 11 mptfng ⊢ ∀ x ∈ B if x ≤ K W DIsoB ⁡ K ⁡ W ⁡ x ι u ∈ S | ∀ q ∈ Atoms ⁡ K ¬ q ≤ K W ∧ q join ⁡ K x meet ⁡ K W = x → u = DIsoC ⁡ K ⁡ W ⁡ q LSSum ⁡ U DIsoB ⁡ K ⁡ W ⁡ x meet ⁡ K W ∈ V ↔ x ∈ B ⟼ if x ≤ K W DIsoB ⁡ K ⁡ W ⁡ x ι u ∈ S | ∀ q ∈ Atoms ⁡ K ¬ q ≤ K W ∧ q join ⁡ K x meet ⁡ K W = x → u = DIsoC ⁡ K ⁡ W ⁡ q LSSum ⁡ U DIsoB ⁡ K ⁡ W ⁡ x meet ⁡ K W Fn B
13 10 12 sylib ⊢ K ∈ HL ∧ W ∈ H → x ∈ B ⟼ if x ≤ K W DIsoB ⁡ K ⁡ W ⁡ x ι u ∈ S | ∀ q ∈ Atoms ⁡ K ¬ q ≤ K W ∧ q join ⁡ K x meet ⁡ K W = x → u = DIsoC ⁡ K ⁡ W ⁡ q LSSum ⁡ U DIsoB ⁡ K ⁡ W ⁡ x meet ⁡ K W Fn B
14 eqid ⊢ ≤ K = ≤ K
15 eqid ⊢ join ⁡ K = join ⁡ K
16 eqid ⊢ meet ⁡ K = meet ⁡ K
17 eqid ⊢ Atoms ⁡ K = Atoms ⁡ K
18 eqid ⊢ DIsoB ⁡ K ⁡ W = DIsoB ⁡ K ⁡ W
19 eqid ⊢ DIsoC ⁡ K ⁡ W = DIsoC ⁡ K ⁡ W
20 eqid ⊢ LSSum ⁡ U = LSSum ⁡ U
21 1 14 15 16 17 2 3 18 19 4 5 20 dihfval ⊢ K ∈ HL ∧ W ∈ H → I = x ∈ B ⟼ if x ≤ K W DIsoB ⁡ K ⁡ W ⁡ x ι u ∈ S | ∀ q ∈ Atoms ⁡ K ¬ q ≤ K W ∧ q join ⁡ K x meet ⁡ K W = x → u = DIsoC ⁡ K ⁡ W ⁡ q LSSum ⁡ U DIsoB ⁡ K ⁡ W ⁡ x meet ⁡ K W
22 21 fneq1d ⊢ K ∈ HL ∧ W ∈ H → I Fn B ↔ x ∈ B ⟼ if x ≤ K W DIsoB ⁡ K ⁡ W ⁡ x ι u ∈ S | ∀ q ∈ Atoms ⁡ K ¬ q ≤ K W ∧ q join ⁡ K x meet ⁡ K W = x → u = DIsoC ⁡ K ⁡ W ⁡ q LSSum ⁡ U DIsoB ⁡ K ⁡ W ⁡ x meet ⁡ K W Fn B
23 13 22 mpbird ⊢ K ∈ HL ∧ W ∈ H → I Fn B
24 1 2 3 4 5 dihlss ⊢ K ∈ HL ∧ W ∈ H ∧ y ∈ B → I ⁡ y ∈ S
25 24 ralrimiva ⊢ K ∈ HL ∧ W ∈ H → ∀ y ∈ B I ⁡ y ∈ S
26 fnfvrnss ⊢ I Fn B ∧ ∀ y ∈ B I ⁡ y ∈ S → ran ⁡ I ⊆ S
27 23 25 26 syl2anc ⊢ K ∈ HL ∧ W ∈ H → ran ⁡ I ⊆ S
28 df-f ⊢ I : B ⟶ S ↔ I Fn B ∧ ran ⁡ I ⊆ S
29 23 27 28 sylanbrc ⊢ K ∈ HL ∧ W ∈ H → I : B ⟶ S