Metamath Proof Explorer


Theorem pjssge0ii

Description: Theorem 4.5(iv)->(v) of Beran p. 112. (Contributed by NM, 13-Aug-2000) (New usage is discouraged.)

Ref Expression
Hypotheses pjidm.1 H C
pjidm.2 A
pjsslem.1 G C
Assertion pjssge0ii proj G A - proj H A = proj G H A 0 proj G A - proj H A ih A

Proof

Step Hyp Ref Expression
1 pjidm.1 H C
2 pjidm.2 A
3 pjsslem.1 G C
4 1 choccli H C
5 3 4 chincli G H C
6 5 2 pjhclii proj G H A
7 6 normcli norm proj G H A
8 7 sqge0i 0 norm proj G H A 2
9 oveq1 proj G A - proj H A = proj G H A proj G A - proj H A ih A = proj G H A ih A
10 5 2 pjinormii proj G H A ih A = norm proj G H A 2
11 9 10 eqtrdi proj G A - proj H A = proj G H A proj G A - proj H A ih A = norm proj G H A 2
12 8 11 breqtrrid proj G A - proj H A = proj G H A 0 proj G A - proj H A ih A