Metamath Proof Explorer


Theorem pjssge0i

Description: Theorem 4.5(iv)->(v) of Beran p. 112. (Contributed by NM, 26-Sep-2001) (New usage is discouraged.)

Ref Expression
Hypotheses pjco.1 G C
pjco.2 H C
Assertion pjssge0i A 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 pjco.1 G C
2 pjco.2 H C
3 fveq2 A = if A A 0 proj G A = proj G if A A 0
4 fveq2 A = if A A 0 proj H A = proj H if A A 0
5 3 4 oveq12d A = if A A 0 proj G A - proj H A = proj G if A A 0 - proj H if A A 0
6 fveq2 A = if A A 0 proj G H A = proj G H if A A 0
7 5 6 eqeq12d A = if A A 0 proj G A - proj H A = proj G H A proj G if A A 0 - proj H if A A 0 = proj G H if A A 0
8 id A = if A A 0 A = if A A 0
9 5 8 oveq12d A = if A A 0 proj G A - proj H A ih A = proj G if A A 0 - proj H if A A 0 ih if A A 0
10 9 breq2d A = if A A 0 0 proj G A - proj H A ih A 0 proj G if A A 0 - proj H if A A 0 ih if A A 0
11 7 10 imbi12d A = if A A 0 proj G A - proj H A = proj G H A 0 proj G A - proj H A ih A proj G if A A 0 - proj H if A A 0 = proj G H if A A 0 0 proj G if A A 0 - proj H if A A 0 ih if A A 0
12 ifhvhv0 if A A 0
13 2 12 1 pjssge0ii proj G if A A 0 - proj H if A A 0 = proj G H if A A 0 0 proj G if A A 0 - proj H if A A 0 ih if A A 0
14 11 13 dedth A proj G A - proj H A = proj G H A 0 proj G A - proj H A ih A