Intuitionistic Logic Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  ILE Home  >  Th. List  >  recexprlemex GIF version

Theorem recexprlemex 6609
 Description: B is the reciprocal of A. Lemma for recexpr 6610. (Contributed by Jim Kingdon, 27-Dec-2019.)
Hypothesis
Ref Expression
recexpr.1 B = ⟨{xy(x <Q y (*Qy) (2ndA))}, {xy(y <Q x (*Qy) (1stA))}⟩
Assertion
Ref Expression
recexprlemex (A P → (A ·P B) = 1P)
Distinct variable groups:   x,y,A   x,B,y

Proof of Theorem recexprlemex
StepHypRef Expression
1 recexpr.1 . . . 4 B = ⟨{xy(x <Q y (*Qy) (2ndA))}, {xy(y <Q x (*Qy) (1stA))}⟩
21recexprlemss1l 6607 . . 3 (A P → (1st ‘(A ·P B)) ⊆ (1st ‘1P))
31recexprlem1ssl 6605 . . 3 (A P → (1st ‘1P) ⊆ (1st ‘(A ·P B)))
42, 3eqssd 2956 . 2 (A P → (1st ‘(A ·P B)) = (1st ‘1P))
51recexprlemss1u 6608 . . 3 (A P → (2nd ‘(A ·P B)) ⊆ (2nd ‘1P))
61recexprlem1ssu 6606 . . 3 (A P → (2nd ‘1P) ⊆ (2nd ‘(A ·P B)))
75, 6eqssd 2956 . 2 (A P → (2nd ‘(A ·P B)) = (2nd ‘1P))
81recexprlempr 6604 . . . 4 (A PB P)
9 mulclpr 6553 . . . 4 ((A P B P) → (A ·P B) P)
108, 9mpdan 398 . . 3 (A P → (A ·P B) P)
11 1pr 6535 . . 3 1P P
12 preqlu 6455 . . 3 (((A ·P B) P 1P P) → ((A ·P B) = 1P ↔ ((1st ‘(A ·P B)) = (1st ‘1P) (2nd ‘(A ·P B)) = (2nd ‘1P))))
1310, 11, 12sylancl 392 . 2 (A P → ((A ·P B) = 1P ↔ ((1st ‘(A ·P B)) = (1st ‘1P) (2nd ‘(A ·P B)) = (2nd ‘1P))))
144, 7, 13mpbir2and 850 1 (A P → (A ·P B) = 1P)
 Colors of variables: wff set class Syntax hints:   → wi 4   ∧ wa 97   ↔ wb 98   = wceq 1242  ∃wex 1378   ∈ wcel 1390  {cab 2023  ⟨cop 3370   class class class wbr 3755  ‘cfv 4845  (class class class)co 5455  1st c1st 5707  2nd c2nd 5708  *Qcrq 6268
 Copyright terms: Public domain W3C validator