Metamath Proof Explorer


Theorem joinval2lem

Description: Lemma for joinval2 and joineu . (Contributed by NM, 12-Sep-2018) TODO: combine this through joineu into joinlem ?

Ref Expression
Hypotheses joinval2.b B=BaseK
joinval2.l ˙=K
joinval2.j ˙=joinK
joinval2.k φKV
joinval2.x φXB
joinval2.y φYB
Assertion joinval2lem XBYByXYy˙xzByXYy˙zx˙zX˙xY˙xzBX˙zY˙zx˙z

Proof

Step Hyp Ref Expression
1 joinval2.b B=BaseK
2 joinval2.l ˙=K
3 joinval2.j ˙=joinK
4 joinval2.k φKV
5 joinval2.x φXB
6 joinval2.y φYB
7 breq1 y=Xy˙xX˙x
8 breq1 y=Yy˙xY˙x
9 7 8 ralprg XBYByXYy˙xX˙xY˙x
10 breq1 y=Xy˙zX˙z
11 breq1 y=Yy˙zY˙z
12 10 11 ralprg XBYByXYy˙zX˙zY˙z
13 12 imbi1d XBYByXYy˙zx˙zX˙zY˙zx˙z
14 13 ralbidv XBYBzByXYy˙zx˙zzBX˙zY˙zx˙z
15 9 14 anbi12d XBYByXYy˙xzByXYy˙zx˙zX˙xY˙xzBX˙zY˙zx˙z