Metamath Proof Explorer


Theorem dih1dimb2

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

Ref Expression
Hypotheses dih1dimb2.b B = Base K
dih1dimb2.l ˙ = K
dih1dimb2.a A = Atoms K
dih1dimb2.h H = LHyp K
dih1dimb2.t T = LTrn K W
dih1dimb2.o O = h T I B
dih1dimb2.u U = DVecH K W
dih1dimb2.i I = DIsoH K W
dih1dimb2.n N = LSpan U
Assertion dih1dimb2 K HL W H Q A Q ˙ W f T f I B I Q = N f O

Proof

Step Hyp Ref Expression
1 dih1dimb2.b B = Base K
2 dih1dimb2.l ˙ = K
3 dih1dimb2.a A = Atoms K
4 dih1dimb2.h H = LHyp K
5 dih1dimb2.t T = LTrn K W
6 dih1dimb2.o O = h T I B
7 dih1dimb2.u U = DVecH K W
8 dih1dimb2.i I = DIsoH K W
9 dih1dimb2.n N = LSpan U
10 eqid trL K W = trL K W
11 2 3 4 5 10 cdlemf K HL W H Q A Q ˙ W f T trL K W f = Q
12 simp3 K HL W H Q A Q ˙ W f T trL K W f = Q trL K W f = Q
13 simp1rl K HL W H Q A Q ˙ W f T trL K W f = Q Q A
14 12 13 eqeltrd K HL W H Q A Q ˙ W f T trL K W f = Q trL K W f A
15 simp1l K HL W H Q A Q ˙ W f T trL K W f = Q K HL W H
16 simp2 K HL W H Q A Q ˙ W f T trL K W f = Q f T
17 1 3 4 5 10 trlnidatb K HL W H f T f I B trL K W f A
18 15 16 17 syl2anc K HL W H Q A Q ˙ W f T trL K W f = Q f I B trL K W f A
19 14 18 mpbird K HL W H Q A Q ˙ W f T trL K W f = Q f I B
20 12 fveq2d K HL W H Q A Q ˙ W f T trL K W f = Q I trL K W f = I Q
21 1 4 5 10 6 7 8 9 dih1dimb K HL W H f T I trL K W f = N f O
22 15 16 21 syl2anc K HL W H Q A Q ˙ W f T trL K W f = Q I trL K W f = N f O
23 20 22 eqtr3d K HL W H Q A Q ˙ W f T trL K W f = Q I Q = N f O
24 19 23 jca K HL W H Q A Q ˙ W f T trL K W f = Q f I B I Q = N f O
25 24 3expia K HL W H Q A Q ˙ W f T trL K W f = Q f I B I Q = N f O
26 25 reximdva K HL W H Q A Q ˙ W f T trL K W f = Q f T f I B I Q = N f O
27 11 26 mpd K HL W H Q A Q ˙ W f T f I B I Q = N f O