Metamath Proof Explorer

Theorem dih1dimc

Description: Isomorphism H at an atom not under W . (Contributed by NM, 27-Apr-2014)

Ref Expression
Hypotheses dih1dimc.l ⊢ ≤ ˙ = ≤ K
dih1dimc.a ⊢ A = Atoms ⁡ K
dih1dimc.h ⊢ H = LHyp ⁡ K
dih1dimc.p ⊢ P = oc ⁡ K ⁡ W
dih1dimc.t ⊢ T = LTrn ⁡ K ⁡ W
dih1dimc.i ⊢ I = DIsoH ⁡ K ⁡ W
dih1dimc.u ⊢ U = DVecH ⁡ K ⁡ W
dih1dimc.n ⊢ N = LSpan ⁡ U
dih1dimc.f ⊢ F = ι f ∈ T | f ⁡ P = Q
Assertion dih1dimc ⊢ K ∈ HL ∧ W ∈ H ∧ Q ∈ A ∧ ¬ Q ≤ ˙ W → I ⁡ Q = N ⁡ F I ↾ T

Proof

Step Hyp Ref Expression
1 dih1dimc.l ⊢ ≤ ˙ = ≤ K
2 dih1dimc.a ⊢ A = Atoms ⁡ K
3 dih1dimc.h ⊢ H = LHyp ⁡ K
4 dih1dimc.p ⊢ P = oc ⁡ K ⁡ W
5 dih1dimc.t ⊢ T = LTrn ⁡ K ⁡ W
6 dih1dimc.i ⊢ I = DIsoH ⁡ K ⁡ W
7 dih1dimc.u ⊢ U = DVecH ⁡ K ⁡ W
8 dih1dimc.n ⊢ N = LSpan ⁡ U
9 dih1dimc.f ⊢ F = ι f ∈ T | f ⁡ P = Q
10 eqid ⊢ DIsoC ⁡ K ⁡ W = DIsoC ⁡ K ⁡ W
11 1 2 3 10 6 dihvalcqat ⊢ K ∈ HL ∧ W ∈ H ∧ Q ∈ A ∧ ¬ Q ≤ ˙ W → I ⁡ Q = DIsoC ⁡ K ⁡ W ⁡ Q
12 1 2 3 4 5 10 7 8 9 diclspsn ⊢ K ∈ HL ∧ W ∈ H ∧ Q ∈ A ∧ ¬ Q ≤ ˙ W → DIsoC ⁡ K ⁡ W ⁡ Q = N ⁡ F I ↾ T
13 11 12 eqtrd ⊢ K ∈ HL ∧ W ∈ H ∧ Q ∈ A ∧ ¬ Q ≤ ˙ W → I ⁡ Q = N ⁡ F I ↾ T