Metamath Proof Explorer

Theorem mapdrvallem3

Description: Lemma for mapdrval . (Contributed by NM, 2-Feb-2015)

Ref Expression
Hypotheses mapdrval.h ⊢ H = LHyp ⁡ K
mapdrval.o ⊢ O = ocH ⁡ K ⁡ W
mapdrval.m ⊢ M = mapd ⁡ K ⁡ W
mapdrval.u ⊢ U = DVecH ⁡ K ⁡ W
mapdrval.s ⊢ S = LSubSp ⁡ U
mapdrval.f ⊢ F = LFnl ⁡ U
mapdrval.l ⊢ L = LKer ⁡ U
mapdrval.d ⊢ D = LDual ⁡ U
mapdrval.t ⊢ T = LSubSp ⁡ D
mapdrval.c ⊢ C = g ∈ F | O ⁡ O ⁡ L ⁡ g = L ⁡ g
mapdrval.k ⊢ φ → K ∈ HL ∧ W ∈ H
mapdrval.r ⊢ φ → R ∈ T
mapdrval.e ⊢ φ → R ⊆ C
mapdrval.q ⊢ Q = ⋃ h ∈ R O ⁡ L ⁡ h
mapdrval.v ⊢ V = Base U
mapdrvallem2.a ⊢ A = LSAtoms ⁡ U
mapdrvallem2.n ⊢ N = LSpan ⁡ U
mapdrvallem2.z ⊢ 0 ˙ = 0 U
mapdrvallem2.y ⊢ Y = 0 D
Assertion mapdrvallem3 ⊢ φ → f ∈ C | O ⁡ L ⁡ f ⊆ Q = R

Proof

Step Hyp Ref Expression
1 mapdrval.h ⊢ H = LHyp ⁡ K
2 mapdrval.o ⊢ O = ocH ⁡ K ⁡ W
3 mapdrval.m ⊢ M = mapd ⁡ K ⁡ W
4 mapdrval.u ⊢ U = DVecH ⁡ K ⁡ W
5 mapdrval.s ⊢ S = LSubSp ⁡ U
6 mapdrval.f ⊢ F = LFnl ⁡ U
7 mapdrval.l ⊢ L = LKer ⁡ U
8 mapdrval.d ⊢ D = LDual ⁡ U
9 mapdrval.t ⊢ T = LSubSp ⁡ D
10 mapdrval.c ⊢ C = g ∈ F | O ⁡ O ⁡ L ⁡ g = L ⁡ g
11 mapdrval.k ⊢ φ → K ∈ HL ∧ W ∈ H
12 mapdrval.r ⊢ φ → R ∈ T
13 mapdrval.e ⊢ φ → R ⊆ C
14 mapdrval.q ⊢ Q = ⋃ h ∈ R O ⁡ L ⁡ h
15 mapdrval.v ⊢ V = Base U
16 mapdrvallem2.a ⊢ A = LSAtoms ⁡ U
17 mapdrvallem2.n ⊢ N = LSpan ⁡ U
18 mapdrvallem2.z ⊢ 0 ˙ = 0 U
19 mapdrvallem2.y ⊢ Y = 0 D
20 1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 mapdrvallem2 ⊢ φ → f ∈ C | O ⁡ L ⁡ f ⊆ Q ⊆ R
21 2fveq3 ⊢ h = f → O ⁡ L ⁡ h = O ⁡ L ⁡ f
22 21 ssiun2s ⊢ f ∈ R → O ⁡ L ⁡ f ⊆ ⋃ h ∈ R O ⁡ L ⁡ h
23 22 adantl ⊢ φ ∧ f ∈ R → O ⁡ L ⁡ f ⊆ ⋃ h ∈ R O ⁡ L ⁡ h
24 23 14 sseqtrrdi ⊢ φ ∧ f ∈ R → O ⁡ L ⁡ f ⊆ Q
25 13 24 ssrabdv ⊢ φ → R ⊆ f ∈ C | O ⁡ L ⁡ f ⊆ Q
26 20 25 eqssd ⊢ φ → f ∈ C | O ⁡ L ⁡ f ⊆ Q = R